Recurrence 2 lookup certificate: Scalar1Main coefficient convolution

This is a checked coefficient-lookup shard for the second pseudo-division recurrence in the order-seven certificate.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_92 : Polynomial.coeff recurrence2Scalar1Main 92 = -((10731471 * 10 ^ 70 + 1856810353665577160685631968543466694463253957773185317866778381432500) * 10 ^ 70 + 6493654293431976582051626071599203213417404334639153413974491856293640)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_93 : Polynomial.coeff recurrence2Scalar1Main 93 = (51191822 * 10 ^ 70 + 7166673637036075644816674261752030383044134915675895213753798907438448) * 10 ^ 70 + 3544512652535867281322657752241477634915202481413974565290821544413237

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_94 : Polynomial.coeff recurrence2Scalar1Main 94 = -((234267087 * 10 ^ 70 + 4604279687214216704789011459970790552105572081638343239363570995877236) * 10 ^ 70 + 9315317978467044810633037049545868650244231762809639500398476268818064)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_95 : Polynomial.coeff recurrence2Scalar1Main 95 = (1027486095 * 10 ^ 70 + 8918920795450915680346523572588735694943178697222094152243854406007098) * 10 ^ 70 + 7423608865412439300373381869565060857877913036465034129074146697381166

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_96 : Polynomial.coeff recurrence2Scalar1Main 96 = -((4312519436 * 10 ^ 70 + 6239196303075081988450281556458068186810766288191363259533803234526851) * 10 ^ 70 + 8293128866238623934959298653582088507719237023277676410248422022598899)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_97 : Polynomial.coeff recurrence2Scalar1Main 97 = (17273577964 * 10 ^ 70 + 7993220819682593672405558109419654319021680450334899647175953119901108) * 10 ^ 70 + 8355759436549071956655540279100544538582177773990373921024922685271362

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_98 : Polynomial.coeff recurrence2Scalar1Main 98 = -((65703164707 * 10 ^ 70 + 3416139851734796480838261734852187477430437885382885564726239196049334) * 10 ^ 70 + 3206583015900689152507504078661503314847770359099912437218943867900260)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_99 : Polynomial.coeff recurrence2Scalar1Main 99 = (235339118097 * 10 ^ 70 + 7852590937315181708953117276896949814396589744930025865628975474197765) * 10 ^ 70 + 5442253007795224104264516631116887343128474275072376127402186080591259

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_100 : Polynomial.coeff recurrence2Scalar1Main 100 = -((782974613221 * 10 ^ 70 + 5543151655984267129673722491708403505734783805028792566915387861154618) * 10 ^ 70 + 4541684287585951412338596714721527402287989203607649293134623549448620)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_101 : Polynomial.coeff recurrence2Scalar1Main 101 = (2365163282073 * 10 ^ 70 + 9324079229874143217428826286761138027953142167080153840654699548012863) * 10 ^ 70 + 7668088391966239381592521271296416005451107878027056274849815683560394

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_102 : Polynomial.coeff recurrence2Scalar1Main 102 = -((6214167069956 * 10 ^ 70 + 728833635196998973824098998146874544948506869637127558796601354724910) * 10 ^ 70 + 748081686393795668279453029366620313035708151089099896089388898418792)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_103 : Polynomial.coeff recurrence2Scalar1Main 103 = (12700246272995 * 10 ^ 70 + 1534025122411058120549363570349043170558372759056924403616567786485719) * 10 ^ 70 + 8193128328980994882613317458095337026010241284983969134112593067316698

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_104 : Polynomial.coeff recurrence2Scalar1Main 104 = -((10271187149706 * 10 ^ 70 + 4444573481185262517808436848298838706092804076408448139522541165384347) * 10 ^ 70 + 9906056155151228388227595235725383496487044092943953126668718375934896)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_105 : Polynomial.coeff recurrence2Scalar1Main 105 = -((81784636265101 * 10 ^ 70 + 6179275121540706910741528071201346406284886837921318473161942613023053) * 10 ^ 70 + 2362693393989791128785970114970904093743252546979998087436372921091884)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_106 : Polynomial.coeff recurrence2Scalar1Main 106 = (684112569228406 * 10 ^ 70 + 6946169941733797763068017188458203155840339143297899027161834811026210) * 10 ^ 70 + 7089092962800033617498233702436612251516705507720285461379489354389182

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_107 : Polynomial.coeff recurrence2Scalar1Main 107 = -((3791815016744393 * 10 ^ 70 + 9027874083333207977791536540952745637918250341648125036162610758210386) * 10 ^ 70 + 1542815825246194341290225174779715090892490147537258485018171587136798)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_108 : Polynomial.coeff recurrence2Scalar1Main 108 = (18149189000545066 * 10 ^ 70 + 6876173784555774379937764482156301321713175690971586610256075525448835) * 10 ^ 70 + 949104934343561910599284897537857959633689451967623741159161463680965

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_109 : Polynomial.coeff recurrence2Scalar1Main 109 = -((77430046986284092 * 10 ^ 70 + 2483010261119047706207494522276091247162740455750549871593492202392277) * 10 ^ 70 + 261120181888529329511977899607841258196521697285938525597106854077161)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_110 : Polynomial.coeff recurrence2Scalar1Main 110 = (285381092585964195 * 10 ^ 70 + 5745353418142751098427723275033906172547577925785961882960037569269538) * 10 ^ 70 + 8619427471595475877283219827469465710771058076332795633166288819390846

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_111 : Polynomial.coeff recurrence2Scalar1Main 111 = -((843012619050101703 * 10 ^ 70 + 5507143694233011828960381993517955580538651627782031450917760709007114) * 10 ^ 70 + 138694839253282500392698649114319089542498772375095007656722592993715)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_112 : Polynomial.coeff recurrence2Scalar1Main 112 = (1634923129271142020 * 10 ^ 70 + 4692971512686304794145886429047894295611254303879923673080061614585386) * 10 ^ 70 + 8357955778331405254286143033838997592550171036937874075003993407218500

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_113 : Polynomial.coeff recurrence2Scalar1Main 113 = (36958106278088612 * 10 ^ 70 + 9382603166933851485033406079825488336135636129248499468004437071442056) * 10 ^ 70 + 4005630148872088397280272306167780104119776054941725452916531705378172

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_114 : Polynomial.coeff recurrence2Scalar1Main 114 = -((13479486309068161321 * 10 ^ 70 + 6289557536648142308924330846127253588570323428511191578084877762266216) * 10 ^ 70 + 8415681934230598602781453194658577998013428763975758435791603961912098)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_115 : Polynomial.coeff recurrence2Scalar1Main 115 = (32696032444939579774 * 10 ^ 70 + 1551834032966531849869068423561287293381438871296528646048674267555963) * 10 ^ 70 + 7461966455383679153774120396589451513498689884791441237242082522605201

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_116 : Polynomial.coeff recurrence2Scalar1Main 116 = (176043765246138751468 * 10 ^ 70 + 2097548467551396803140190668455859407337849761622880047938667031305903) * 10 ^ 70 + 9359771604840230588107977683483715860864440579741883796171639118997679

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_117 : Polynomial.coeff recurrence2Scalar1Main 117 = -((1971590689037401119813 * 10 ^ 70 + 8845692204218908561967889097009644645426084185159132753435574857704993) * 10 ^ 70 + 4631716292040919133859064546373493250620622584375017645839599902501938)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_118 : Polynomial.coeff recurrence2Scalar1Main 118 = (9559080136386197342213 * 10 ^ 70 + 7357501426448694565801770445695468876812738981599651438271896561649543) * 10 ^ 70 + 7813254166081238683205172131534791009409424329274032770977072266548500

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_119 : Polynomial.coeff recurrence2Scalar1Main 119 = -((24978063997325642948342 * 10 ^ 70 + 6480692540201057370871064692768481551863408891475588183720107496646151) * 10 ^ 70 + 720885531136317650875671551288539841358943926230443046246505677133063)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_120 : Polynomial.coeff recurrence2Scalar1Main 120 = -((13476334784227916333273 * 10 ^ 70 + 6939459294120174620837733272399286612610468999696358137617935982130159) * 10 ^ 70 + 7223418516921953562945899293677869516377701900531321859300224305531850)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_121 : Polynomial.coeff recurrence2Scalar1Main 121 = (539648987071252207580516 * 10 ^ 70 + 1659825289990917721172634114512270788900248290021808102461935865499402) * 10 ^ 70 + 9360184951174080546399646113534709372203905414080020600193817673093757

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_122 : Polynomial.coeff recurrence2Scalar1Main 122 = -((3272146996989407869989383 * 10 ^ 70 + 700217447175821010448940334604202741212670236704823670362677589318110) * 10 ^ 70 + 5013729081855033299031620472212888655385382189269401905398171988757761)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_123 : Polynomial.coeff recurrence2Scalar1Main 123 = (11601705824115019753275959 * 10 ^ 70 + 1729308221309642818938172121669116080127535477974321485356002077718078) * 10 ^ 70 + 9751885817246970705651234920668516153380522474149941984671683295816513

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_124 : Polynomial.coeff recurrence2Scalar1Main 124 = -((16892830047939413030672339 * 10 ^ 70 + 2155847732662765798630441217304934540569189670295134038981633128314992) * 10 ^ 70 + 542364905592854890668395371686413498241552888434562085898332643432929)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_125 : Polynomial.coeff recurrence2Scalar1Main 125 = -((90525459306829139401543563 * 10 ^ 70 + 9109529101926874796042769762052198313884053533385687583782630097854467) * 10 ^ 70 + 9165817143237552673993623638747255370371471091947896050145029159094516)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_126 : Polynomial.coeff recurrence2Scalar1Main 126 = (804646943845235836578615762 * 10 ^ 70 + 185065299022055345158732760446382368659775946888677307819318140862433) * 10 ^ 70 + 1807288153785222098715004186781950234541427126558259423589689614197544

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_127 : Polynomial.coeff recurrence2Scalar1Main 127 = -((3170331576950677597861848094 * 10 ^ 70 + 3276354473890321330337760065296197767937521917804602826589704572279925) * 10 ^ 70 + 7806033702323266745653669136096475497611807122083758683730453579659630)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_128 : Polynomial.coeff recurrence2Scalar1Main 128 = (5744395883762065807813919700 * 10 ^ 70 + 7571540965043626024404311115640392203363915440417574113445876517578338) * 10 ^ 70 + 2180890391015636383295766120896928445408990791055322794796826483654754

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_129 : Polynomial.coeff recurrence2Scalar1Main 129 = (11039963888327238088018397412 * 10 ^ 70 + 1162839953819632251498099430434147397966992070700456490762658232280671) * 10 ^ 70 + 2736545162662905493711244397812036906687788509077603974997954917225762

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_130 : Polynomial.coeff recurrence2Scalar1Main 130 = -((116582918607836536405834183817 * 10 ^ 70 + 9282579004830389885570220764297370060931635395307968440884048178246914) * 10 ^ 70 + 6189418994491637307229489293178256083553190248567401022770530039724668)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_131 : Polynomial.coeff recurrence2Scalar1Main 131 = (416206874423288051483901303339 * 10 ^ 70 + 5149246722841989221712114322628761226920522273361582348375229241854623) * 10 ^ 70 + 1728083885435451360364496287072902876975175816421848081626602684339559

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_132 : Polynomial.coeff recurrence2Scalar1Main 132 = -((904082877353674543686837571511 * 10 ^ 70 + 3058711848019071563033903686538895524441474222226342358178726893387734) * 10 ^ 70 + 7789441769337962179231180694874212819845123583542785650808165819937947)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_133 : Polynomial.coeff recurrence2Scalar1Main 133 = (1849330295492066819513461760443 * 10 ^ 70 + 2569341552383987618282369685216505853476540398688075831462586221086995) * 10 ^ 70 + 4371744010637767698840284822139105176290677171204453176135867664242370

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_134 : Polynomial.coeff recurrence2Scalar1Main 134 = -((5949126831115369069666967829114 * 10 ^ 70 + 7408747193976264298984552272866514558466492587421380085062540723063999) * 10 ^ 70 + 5517251165108535855770806742551852235734437620137386980990483090904794)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_135 : Polynomial.coeff recurrence2Scalar1Main 135 = (4005954322203169196573587085004 * 10 ^ 70 + 7727041760493830319920706888579957900262418437468042123632865558480549) * 10 ^ 70 + 4950311534573460282741028393352118033513319478791236099804232882334575

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_136 : Polynomial.coeff recurrence2Scalar1Main 136 = (167223685638958151096032664278712 * 10 ^ 70 + 4004316717239780458209024361606073917438461853536637427143888482794321) * 10 ^ 70 + 6737973594729615260471592164804001009677818446674091002124284632777295

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_137 : Polynomial.coeff recurrence2Scalar1Main 137 = -((1216789077965758021165300266828345 * 10 ^ 70 + 9543440941521708051727625250802762379263759212197092531612735535047756) * 10 ^ 70 + 5741157387644601328102751411869379336491693943362035063874008491292621)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_138 : Polynomial.coeff recurrence2Scalar1Main 138 = (3688637869007011171291784547973441 * 10 ^ 70 + 9367085169896697160733909020703880616463434931831768092965802034768411) * 10 ^ 70 + 9168569455028637960302585327460152069057806707948839157692685704958237

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_139 : Polynomial.coeff recurrence2Scalar1Main 139 = (270097187605604057459603551127428 * 10 ^ 70 + 7671186865570062387533232054485230285527412489060120696887073875275979) * 10 ^ 70 + 2044991489071584350887854669229954076079892606248884882819136781698887

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_140 : Polynomial.coeff recurrence2Scalar1Main 140 = -((42962521717064744184471970526629704 * 10 ^ 70 + 2970086415021705772462825463288272343481406657872591304907908626021579) * 10 ^ 70 + 1618387387928014531435118700697657693620979439471450236718839598577544)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_141 : Polynomial.coeff recurrence2Scalar1Main 141 = (111629159922101474733107567060021922 * 10 ^ 70 + 4270098453837492673901113430347139915269054659931980238041288731495272) * 10 ^ 70 + 5683447221619276854213027117459347240483384284134272455925735501060886

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_142 : Polynomial.coeff recurrence2Scalar1Main 142 = (279433684704637464870835436373675670 * 10 ^ 70 + 5386658397212666811714357280529255043842496326977320569302918004305770) * 10 ^ 70 + 558260027122298708899623986028871335645015646564566094829534341794290

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_143 : Polynomial.coeff recurrence2Scalar1Main 143 = -((2172403115252479048440668743656115240 * 10 ^ 70 + 6854345939459646155989128393990975373455214492388547191763411355895643) * 10 ^ 70 + 6499358093292569435390899645345106176737674980371089462715794758946399)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_144 : Polynomial.coeff recurrence2Scalar1Main 144 = -((52061468172623598749029768012547226 * 10 ^ 70 + 220891477179171919603136357313372055971240271236481234834397239639704) * 10 ^ 70 + 9556667138060110968236703462992063884942188998887218513759259912269128)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_145 : Polynomial.coeff recurrence2Scalar1Main 145 = (46265950330538593681030765605334218429 * 10 ^ 70 + 379252062615447275403954844637289251986596101591850405163186620266867) * 10 ^ 70 + 2927075521216846983176858612828573528342906877955795752660105115653018

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_146 : Polynomial.coeff recurrence2Scalar1Main 146 = -((194519717332058516348006694550742989425 * 10 ^ 70 + 3168003669253456804814693094273892275040655966718105923221635767068905) * 10 ^ 70 + 4116947405892565901093857848077036441322938731447975585735787914484677)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_147 : Polynomial.coeff recurrence2Scalar1Main 147 = (20528936966179073171598445347335683061 * 10 ^ 70 + 4324814615342447914667146880406272496340548192037584876853830076307354) * 10 ^ 70 + 6842079181721422445248667388103978976841563769879905776040251843920753

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_148 : Polynomial.coeff recurrence2Scalar1Main 148 = (3053657466589775881965922374712468229430 * 10 ^ 70 + 7255295517125438093238980283165991268922372199920461905085929908651863) * 10 ^ 70 + 9973148666299095063884454134995844400753847994346173048821985401431260

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_149 : Polynomial.coeff recurrence2Scalar1Main 149 = -((12799280656841234636625720167165481863349 * 10 ^ 70 + 2030569730268318047711464707316863256601449611036009341028874508756674) * 10 ^ 70 + 1022665530029978952631536461126624129732394913207968026190318861293350)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_150 : Polynomial.coeff recurrence2Scalar1Main 150 = (6965198596987771507221429486441387910528 * 10 ^ 70 + 9673802682819035643945010941257649818349481046627446675787999865695479) * 10 ^ 70 + 7080709929682824070836818142531107502790750054507542345448511246022285

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_151 : Polynomial.coeff recurrence2Scalar1Main 151 = (151391492872235919044962281869157996303259 * 10 ^ 70 + 118464400924941510236739959530568489695339306314686819254575744509001) * 10 ^ 70 + 5710256580139561560124052953166560405713172190130738054175071626867669

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_152 : Polynomial.coeff recurrence2Scalar1Main 152 = -((680881598398747340193801825265564569311580 * 10 ^ 70 + 8689500674376875307918395429677936011832727663166490234192770720578059) * 10 ^ 70 + 2907557870276556561756284360541904724863338418531023524634721796041856)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_153 : Polynomial.coeff recurrence2Scalar1Main 153 = (610106624906183192535729130066824619310620 * 10 ^ 70 + 1142536235970873077706894338533922967682150629387306639637420240643811) * 10 ^ 70 + 8766225981729621250861654298852307249519237743091610100001576002669422