Recurrence 2 lookup certificate: Scalar0Main 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.recurrence2Scalar0Main_coeff_236 : Polynomial.coeff recurrence2Scalar0Main 236 = ((6930 * 10 ^ 70 + 4173725646603797473254053903337855014328521726276667926506144738042480) * 10 ^ 70 + 261597618626137237027825898765539348803040420961858141675165436495988) * 10 ^ 70 + 2161621584991166214931842165229757456195800137678119857082984446870423

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_237 : Polynomial.coeff recurrence2Scalar0Main 237 = -(((7619 * 10 ^ 70 + 3156750023892765688144604067308306393571625781424435887575872033335083) * 10 ^ 70 + 380227255685731935058463380600560564375412634350746944930333525735479) * 10 ^ 70 + 8809339239421559738695576304680460790891655866777909319028446899056378)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_238 : Polynomial.coeff recurrence2Scalar0Main 238 = ((7968 * 10 ^ 70 + 1880087459132719470155006619622305556673073026250372214050783947347104) * 10 ^ 70 + 2795596537291931758881408380795090400916155550175630695995584856213274) * 10 ^ 70 + 6167811604499954049612869901762535271531559503508705230144591121640961

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_239 : Polynomial.coeff recurrence2Scalar0Main 239 = -(((7914 * 10 ^ 70 + 4579601491421491845612576889622525597284493388979719681324151278063194) * 10 ^ 70 + 2357499583185049656476576565085460431877762347024784216805954032000630) * 10 ^ 70 + 5362474073128633898477271944250402107623691286067142386596644765164605)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_240 : Polynomial.coeff recurrence2Scalar0Main 240 = ((7440 * 10 ^ 70 + 1531600139951903538509441922659576795050022122103119648540303282699869) * 10 ^ 70 + 6678482031576215818742232434168640586332079389224546757853774491006555) * 10 ^ 70 + 274715935087210440186302607891306575906370741026629183398205006848082

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_241 : Polynomial.coeff recurrence2Scalar0Main 241 = -(((6576 * 10 ^ 70 + 5596743071976759773457506446192051248786633232856597780233529694433647) * 10 ^ 70 + 9812341014331789970856273942157838973041122893131841483086154355186579) * 10 ^ 70 + 130939094921074041375348156527929423086197236170808345119376646746407)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_242 : Polynomial.coeff recurrence2Scalar0Main 242 = ((5400 * 10 ^ 70 + 3974574836992087256506124201275508576291482999505494580579791369663393) * 10 ^ 70 + 5600686745333201705002935382481279641840939553033631250232525220693823) * 10 ^ 70 + 1993593984935747379167775633504905205183541593861443992022257825969538

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_243 : Polynomial.coeff recurrence2Scalar0Main 243 = -(((4022 * 10 ^ 70 + 2649343519442198979984486010068818792191653108467592470861464355087849) * 10 ^ 70 + 8681613700458990931207219267896563928313572217653034365647482520783886) * 10 ^ 70 + 745336323865454300550937151289972752658136003185768328258006555353802)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_244 : Polynomial.coeff recurrence2Scalar0Main 244 = ((2569 * 10 ^ 70 + 7987712086180369948316724940080851392770792323999870470045082390433937) * 10 ^ 70 + 7648631805947750884962294416707810596549661470862666611733859096299246) * 10 ^ 70 + 1860398975354197665865371350055320548780873370006803119756667569968091

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_245 : Polynomial.coeff recurrence2Scalar0Main 245 = -(((1169 * 10 ^ 70 + 326239843254896254871808187778903353386946620907224072206790142694907) * 10 ^ 70 + 947603733774240118374451954562626571883403082982547627049083640645567) * 10 ^ 70 + 2700957872219631582103876106748600210200555698825685054605344357216177)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_246 : Polynomial.coeff recurrence2Scalar0Main 246 = -(((72 * 10 ^ 70 + 4224285428941169421833560974855257537318054234501373359734180053932856) * 10 ^ 70 + 4029621916973183571071067322358568828063212616695652205023256033574550) * 10 ^ 70 + 2512528940683795681222694948535655648394918187956741889282757895731069)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_247 : Polynomial.coeff recurrence2Scalar0Main 247 = ((1077 * 10 ^ 70 + 4765492552769213787518229423080879484774750685389368142299355973746280) * 10 ^ 70 + 7247210074646100976514875627683655671845995441314870034661797188640770) * 10 ^ 70 + 1438070689768734477331893242973919986576021544238137738825166264397121

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_248 : Polynomial.coeff recurrence2Scalar0Main 248 = -(((1805 * 10 ^ 70 + 3499657765891824996657390294486409613979806712609974219874949869062020) * 10 ^ 70 + 9594571344416073950102379064061173183623618773797762763298326985963927) * 10 ^ 70 + 9504272120638955006365313455956561201923931968116930341604165913114344)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_249 : Polynomial.coeff recurrence2Scalar0Main 249 = ((2250 * 10 ^ 70 + 9556144096366509951776069611593669937614307764257391231146000044316658) * 10 ^ 70 + 6776126144505827876102302973369111718803250974849206758111878967985377) * 10 ^ 70 + 1530551859894547637756348667609614220115542097437386676437485290038262

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_250 : Polynomial.coeff recurrence2Scalar0Main 250 = -(((2439 * 10 ^ 70 + 586590698317517180393411672059877482100576975246455418729265844941807) * 10 ^ 70 + 98879937594713696767026423434361424267408935688601033574756426779860) * 10 ^ 70 + 1453721206125613628869620271960395629398868601261679361238014587997259)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_251 : Polynomial.coeff recurrence2Scalar0Main 251 = ((2415 * 10 ^ 70 + 1895545828719948640176410700200783116164203182015841867261747438127542) * 10 ^ 70 + 9822662418643417196980666603358896865814188262223636025502427665131257) * 10 ^ 70 + 5961596323899507759734718060744916650059963805224559573604749037973492

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_252 : Polynomial.coeff recurrence2Scalar0Main 252 = -(((2235 * 10 ^ 70 + 5013111489289747142972665394356346263706976439932039657184221756906441) * 10 ^ 70 + 1718556939761761673699716856801551341630699235565350326892718315303572) * 10 ^ 70 + 2917233268183608088882802682042637114603943271241508349406210828965238)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_253 : Polynomial.coeff recurrence2Scalar0Main 253 = ((1957 * 10 ^ 70 + 4707689098842591460122309542485292618108447954895595102743829734250992) * 10 ^ 70 + 8636301841410299376422764735323001603553527379248008183573626967751154) * 10 ^ 70 + 5055410917214927237295275921009399914346730485537717693653009075939413

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_254 : Polynomial.coeff recurrence2Scalar0Main 254 = -(((1632 * 10 ^ 70 + 7327214547658620851019538196447443115845704417385194904778584554843269) * 10 ^ 70 + 4485451947123551689120657945625607814066413634546869057669625820902802) * 10 ^ 70 + 6516925752065930364641278346550054434737637247030835725264394246245631)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_255 : Polynomial.coeff recurrence2Scalar0Main 255 = ((1302 * 10 ^ 70 + 6221107580814209379408944936091550827741855536084996253911502754069284) * 10 ^ 70 + 5553989100268914634386650772554421749355877920676675464875558540840404) * 10 ^ 70 + 9931614462846199713936376875279561894763795974369657801339161035566274

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_256 : Polynomial.coeff recurrence2Scalar0Main 256 = -(((996 * 10 ^ 70 + 3669867699707652819923308332994514435957761479325091817128479025088409) * 10 ^ 70 + 7391641521222783544937939168878609140927902875812956524797266749392030) * 10 ^ 70 + 9509310263475723889671825945474112563873184313230710880500337310295497)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_257 : Polynomial.coeff recurrence2Scalar0Main 257 = ((731 * 10 ^ 70 + 4353295244741773701314552988276226343683349416412442170101917335041903) * 10 ^ 70 + 4166357604701949963728592862687669718247881947310319877812817126767473) * 10 ^ 70 + 2790187316605408247945192952840703292347502048110999955210771994684912

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_258 : Polynomial.coeff recurrence2Scalar0Main 258 = -(((515 * 10 ^ 70 + 3255426890082479172223423067384686394059149099188246217698336759735016) * 10 ^ 70 + 891416181089077170049821059297517765451274674953009223804292794848639) * 10 ^ 70 + 9922961524557434114633366719361487371451228586311961285144112067203852)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_259 : Polynomial.coeff recurrence2Scalar0Main 259 = ((348 * 10 ^ 70 + 752519827901344953807036629314212442858951569027251522490359929808017) * 10 ^ 70 + 2621865392886168239178960829025250289804009167828796912613114313017846) * 10 ^ 70 + 6592708199487670800889881525730113695761946990612909412961254308776297

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_260 : Polynomial.coeff recurrence2Scalar0Main 260 = -(((224 * 10 ^ 70 + 8837573986826452946142288473299342780682778748213584638659528606354279) * 10 ^ 70 + 2248843825181015145913252775425893639089414108020283032779560288345585) * 10 ^ 70 + 7300656080042793830518651698560898189010595643757307788072736887791318)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_261 : Polynomial.coeff recurrence2Scalar0Main 261 = ((138 * 10 ^ 70 + 4303759736970617650222105071407614121758233134213052532888294699736463) * 10 ^ 70 + 7759676370247741706941702258867872979135163224956940315154388516088513) * 10 ^ 70 + 2057447979530230374919504268329524400879540624516043919074550031734839

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_262 : Polynomial.coeff recurrence2Scalar0Main 262 = -(((80 * 10 ^ 70 + 6653269756217030035592055576109107398724674575182937569175636954753022) * 10 ^ 70 + 6739843509570528223273160928782804419090373516906946035554777795791610) * 10 ^ 70 + 4986726526360584634965942668492816987029462256185831389705319661611950)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_263 : Polynomial.coeff recurrence2Scalar0Main 263 = ((44 * 10 ^ 70 + 129453667092275411785688931244639006969715975267122005072936471121913) * 10 ^ 70 + 3621889650466577444270792162588302733338277872481045424250024314837659) * 10 ^ 70 + 4229947597000601211874356144820842123324029375537131457403410882859890

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_264 : Polynomial.coeff recurrence2Scalar0Main 264 = -(((22 * 10 ^ 70 + 405844279578020409713525305739374335207800623986062875164551037694727) * 10 ^ 70 + 3579532304966288459325161934529402807312341081570730226232331172772663) * 10 ^ 70 + 811115471689136805633962261935442610756557198546560505236514144873718)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_265 : Polynomial.coeff recurrence2Scalar0Main 265 = ((9 * 10 ^ 70 + 7086748920823271808442767326247396780913584213007099657764283933304324) * 10 ^ 70 + 212534257943814552278589011587837766224992548951489283924398748878732) * 10 ^ 70 + 6658068052703452924796171834538547727269365237428088348010289490151214

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_266 : Polynomial.coeff recurrence2Scalar0Main 266 = -(((3 * 10 ^ 70 + 3365331324918413777634279786813613192211982954695808994312322066887094) * 10 ^ 70 + 9681597096124210757327594668232510173627228642794394884370591728720595) * 10 ^ 70 + 5906520247245691495050509605290402783810510020598640339960467377505731)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_267 : Polynomial.coeff recurrence2Scalar0Main 267 = (4078525747702871333145303949838237101513457577788508175297879326527292 * 10 ^ 70 + 2716983098387136730991074443700323417514126375179897402368615111359321) * 10 ^ 70 + 2177956376441422322843736295989455559173808937697208614071978048450404