Recurrence 2 lookup certificate: Scalar0Left 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.recurrence2Scalar0Left_coeff_93 :
Polynomial.coeff recurrence2Scalar0Left 93 = (12205612 * 10 ^ 70 + 9670116791929731697644254387109676019243663323458484580952181153422869) * 10 ^ 70 + 2293759075133267521865662239170739460100983797025184431244606819043458
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_94 :
Polynomial.coeff recurrence2Scalar0Left 94 = -((58629733 * 10 ^ 70 + 3358134333763208146658044306507251376159266989670700522597792510626056) * 10 ^ 70 + 6901007811280741545470829534595994603263016593136718167942944256873998)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_95 :
Polynomial.coeff recurrence2Scalar0Left 95 = (270312635 * 10 ^ 70 + 2264165363497700917953284815954672678838832622636013701188368159313175) * 10 ^ 70 + 9540582627490253677559352734172958384675179633105917547023915204870467
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_96 :
Polynomial.coeff recurrence2Scalar0Left 96 = -((1195326738 * 10 ^ 70 + 7960124760868854505978904808613554618262456280507439289108291209844993) * 10 ^ 70 + 6637891238379628558773654018766476231359186045676880324224062680056105)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_97 :
Polynomial.coeff recurrence2Scalar0Left 97 = (5063522450 * 10 ^ 70 + 4251204049483655335089796146860111511184132961658020673064632818449632) * 10 ^ 70 + 9238827016628107063856338641599786080221785304374189037209050854373190
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_98 :
Polynomial.coeff recurrence2Scalar0Left 98 = -((20500712943 * 10 ^ 70 + 1059218421732417412925294048872939816504219278021281875376587676875613) * 10 ^ 70 + 9089156305022978654962126252582617508223733851039475622874182515907099)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_99 :
Polynomial.coeff recurrence2Scalar0Left 99 = (78997526222 * 10 ^ 70 + 8804536151009119535187574173112778108596570864851383928390907192254144) * 10 ^ 70 + 480617534341330549576294131902654147031829999905588747619804659586850
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_100 :
Polynomial.coeff recurrence2Scalar0Left 100 = -((287693237043 * 10 ^ 70 + 1018584161841836342006634054484339791737540371353978942290011363934699) * 10 ^ 70 + 4553581973010770401288212502640948716837016765759833223602366714683498)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_101 :
Polynomial.coeff recurrence2Scalar0Left 101 = (979354473627 * 10 ^ 70 + 6253329224810187741184148352392264037602363838892939377475712303877635) * 10 ^ 70 + 4111629774550645668874325251930905699486578340371759264388327644827507
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_102 :
Polynomial.coeff recurrence2Scalar0Left 102 = -((3063945441958 * 10 ^ 70 + 7543961397064606793900702520373183533362528460453638626118540149890068) * 10 ^ 70 + 8359402432152104929111316440511569417711850284270761542505192134783216)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_103 :
Polynomial.coeff recurrence2Scalar0Left 103 = (8561653422442 * 10 ^ 70 + 8819692878683502327880187960040610580119269897721226569450509202431058) * 10 ^ 70 + 476343402256606209881297726780694363294071277024689107549252713349412
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_104 :
Polynomial.coeff recurrence2Scalar0Left 104 = -((20096920369312 * 10 ^ 70 + 2880642967156647296221169592193151937197761824455695546420795420679901) * 10 ^ 70 + 7635130905650339150271762261915731320333765037716710468860124331685828)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_105 :
Polynomial.coeff recurrence2Scalar0Left 105 = (31926469249669 * 10 ^ 70 + 6199920246413393775645870072186089323778267617765451890747003388410524) * 10 ^ 70 + 7333850355202506104911770358580409884544063440622988480780290711405019
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_106 :
Polynomial.coeff recurrence2Scalar0Left 106 = (23641315433917 * 10 ^ 70 + 7229667721130119065298212811259945643697650071083140264460078595182349) * 10 ^ 70 + 576700126731498751172734569602333006214073653170259031903563881081007
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_107 :
Polynomial.coeff recurrence2Scalar0Left 107 = -((544464799095724 * 10 ^ 70 + 3339359326782960119192408889148696863513974945725742993720569280675698) * 10 ^ 70 + 8977396977538399382018591712908122208488908536814710735415036859222271)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_108 :
Polynomial.coeff recurrence2Scalar0Left 108 = (3521790626057322 * 10 ^ 70 + 8912624823655654432058802260786918546061011351858159257778595719427703) * 10 ^ 70 + 9473564624575710431875031691648539079589847724331941973526663704079938
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_109 :
Polynomial.coeff recurrence2Scalar0Left 109 = -((18032217314329734 * 10 ^ 70 + 2312927873785201209387876132266132926116252789969325311988319721547848) * 10 ^ 70 + 1316873881957335286341487398431330662811243400853469939941798093779282)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_110 :
Polynomial.coeff recurrence2Scalar0Left 110 = (80626596571898484 * 10 ^ 70 + 7083887902105867934680467160022436312600685466600104570931838535858512) * 10 ^ 70 + 8105880420339933749265183982850314815507269807802901776685458338793550
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_111 :
Polynomial.coeff recurrence2Scalar0Left 111 = -((310749874428073668 * 10 ^ 70 + 6880145978239716911564230719005348049106369091317772893625601698678542) * 10 ^ 70 + 2584517826040188336505726745776581424502091382493502674863843838969079)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_112 :
Polynomial.coeff recurrence2Scalar0Left 112 = (961903079911194027 * 10 ^ 70 + 6559225285997392101474622009211143680656491286684995050500735999651157) * 10 ^ 70 + 3338459165444407666899947274915459986734235154452408597168889446700583
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_113 :
Polynomial.coeff recurrence2Scalar0Left 113 = -((1950796822556066330 * 10 ^ 70 + 7416540750194542578773170709175746519427091825432458876625818605954469) * 10 ^ 70 + 5976817068461706273123481064270982001169940423665133049050179921902341)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_114 :
Polynomial.coeff recurrence2Scalar0Left 114 = -((175101519447809920 * 10 ^ 70 + 9714814421780521237809429608205108226191001209058181764567741310200028) * 10 ^ 70 + 6717665724680457633457746823436717343707845643774902114599933212082216)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_115 :
Polynomial.coeff recurrence2Scalar0Left 115 = (19089177561245600513 * 10 ^ 70 + 2425715651570664856175407923722940849292717384232751991983193405251749) * 10 ^ 70 + 1211989410066549282519496059660383893112219933247886351849409189822603
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_116 :
Polynomial.coeff recurrence2Scalar0Left 116 = -((55995518839608095981 * 10 ^ 70 + 8920076610309924083669363656779340581534561979531393687959230238047207) * 10 ^ 70 + 5722844571194959952599303876979988540684555763838442879063668214044695)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_117 :
Polynomial.coeff recurrence2Scalar0Left 117 = -((172000269050581851638 * 10 ^ 70 + 2420211508507341729658738711600605769496873078618814042718043185957979) * 10 ^ 70 + 3816632384396901907350021867210977274008954060825053262965904409250869)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_118 :
Polynomial.coeff recurrence2Scalar0Left 118 = (2411368682396605374940 * 10 ^ 70 + 2750808452696358638945387534355574880786457489790359210818875653295612) * 10 ^ 70 + 7976364394935505149493924770214971560087343951616086766324819214876610
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_119 :
Polynomial.coeff recurrence2Scalar0Left 119 = -((11906375492587163228945 * 10 ^ 70 + 2927839752077313424294169782367526144767258980930089188416614331518979) * 10 ^ 70 + 3752853821249722792691756566880318098392099469280504845175469526851250)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_120 :
Polynomial.coeff recurrence2Scalar0Left 120 = (29023755539295809680208 * 10 ^ 70 + 7035312521184089149573299040414442385152865120275575477666420997271343) * 10 ^ 70 + 8408491130547892970504068786520937249136914566883549832108942630243976
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_121 :
Polynomial.coeff recurrence2Scalar0Left 121 = (32735886580857777333210 * 10 ^ 70 + 1291131480231658582277299473291356380781505205407253833276114425976334) * 10 ^ 70 + 6490804552105073993932003948134628864740478028859875426994770558159791
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_122 :
Polynomial.coeff recurrence2Scalar0Left 122 = -((690361182942019537518913 * 10 ^ 70 + 6078456201843886635409690433126064920883855041922534078443682214585936) * 10 ^ 70 + 5106572046658303594197359634607117306344700488302147838078784746890950)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_123 :
Polynomial.coeff recurrence2Scalar0Left 123 = (3635677248273860589860421 * 10 ^ 70 + 5068975055456440214461991595146012517457705070704365920330144227239350) * 10 ^ 70 + 7771636375514123589430826814372097633105889189230948715416707703139905
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_124 :
Polynomial.coeff recurrence2Scalar0Left 124 = -((10963563988105403197125207 * 10 ^ 70 + 8961615835475073147219121638240670692233359210070911869589995943608921) * 10 ^ 70 + 2718150306898755292609662817120812328488896778537777067083557117240764)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_125 :
Polynomial.coeff recurrence2Scalar0Left 125 = (10223523821411579015326509 * 10 ^ 70 + 7775678653997878895084668803390530757038061232798934187770702069073151) * 10 ^ 70 + 6787719378889122562198653487448131617809188530946024734824102516507610
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_126 :
Polynomial.coeff recurrence2Scalar0Left 126 = (96920631738774786120297494 * 10 ^ 70 + 742923250446499780023588566258275756944721941314162249345461879001644) * 10 ^ 70 + 6558325247642320033368289532623452451982805985462362796089520356264862
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_127 :
Polynomial.coeff recurrence2Scalar0Left 127 = -((676475743830521157972704149 * 10 ^ 70 + 6166331692824650768709541792216012353209090335246883807076207189043556) * 10 ^ 70 + 2406248411201034991959197572615408245139331983909783948107814171787160)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_128 :
Polynomial.coeff recurrence2Scalar0Left 128 = (2441033421095542009158826567 * 10 ^ 70 + 9268141714324754528475264329321349344922485994372689882789577419082890) * 10 ^ 70 + 1879567035567632581222362870148587148407021272581471012208928009791954
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_129 :
Polynomial.coeff recurrence2Scalar0Left 129 = -((5186795870966157144305992113 * 10 ^ 70 + 4512556563885258718648643324434833687955832739902492607233501888820423) * 10 ^ 70 + 580170430651579462166706993362626048771775892722013078258090138798964)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_130 :
Polynomial.coeff recurrence2Scalar0Left 130 = (3094281278228160721901721751 * 10 ^ 70 + 6787806247404286814947943000224064520808042589178029233013299008624117) * 10 ^ 70 + 1743903288612209439145146059401503456813205427884198733702559539987215
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_131 :
Polynomial.coeff recurrence2Scalar0Left 131 = (26630437085927772143151533043 * 10 ^ 70 + 3119808867885021342396966159972717758018691990821464714546142966591445) * 10 ^ 70 + 1569488287657471584030065327680019622027321215332750404432196843678556
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_132 :
Polynomial.coeff recurrence2Scalar0Left 132 = -((217007445332078232138566030180 * 10 ^ 70 + 7191849465185378658304958294481281991030828373430068241350126068813833) * 10 ^ 70 + 5980122877912020855650040812850904421593511745302439126927825653461074)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_133 :
Polynomial.coeff recurrence2Scalar0Left 133 = (1577541970728949194200773639164 * 10 ^ 70 + 949890431559400484167473184206735553950648937279617221698474815034820) * 10 ^ 70 + 5266471460836751297752342170782492365450151106481979752543860296462462
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_134 :
Polynomial.coeff recurrence2Scalar0Left 134 = -((8999193462075021127318099102459 * 10 ^ 70 + 7392112895285831969350812439244140982411416863984856611095081412562) * 10 ^ 70 + 8249787779902765938071880787633649099512548879522955559849259218581466)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_135 :
Polynomial.coeff recurrence2Scalar0Left 135 = (30707025648391110625678023819453 * 10 ^ 70 + 2180781788566585221402712985486164389104128941890517353806848173835899) * 10 ^ 70 + 697255331286531798160476062618700247659043439491248206536922678101004
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_136 :
Polynomial.coeff recurrence2Scalar0Left 136 = -((9333909619870777461352706707700 * 10 ^ 70 + 2801258067281038460816561931146416578858421544453009812040318648858421) * 10 ^ 70 + 5735077289654143213401329070022240312548074146985355114462795666135229)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_137 :
Polynomial.coeff recurrence2Scalar0Left 137 = -((527944035530545234814865235449552 * 10 ^ 70 + 6120836030555979406607549879829454826334470267932716510460823341034590) * 10 ^ 70 + 4800280830443109342896606475432735267907865448914519466250979014988236)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_138 :
Polynomial.coeff recurrence2Scalar0Left 138 = (2977474759272394788166797275488473 * 10 ^ 70 + 331311050880913562495679696963352094007967374278016925532177932481929) * 10 ^ 70 + 8705440620235975248036951674128648854342605876754601697338781924875443
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_139 :
Polynomial.coeff recurrence2Scalar0Left 139 = -((6484494930879142323639836493705713 * 10 ^ 70 + 6262588548186947603261275122603423560036252955176835928855778054315518) * 10 ^ 70 + 9523508447195933703508268392953465527091096429473336468312066759708261)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_140 :
Polynomial.coeff recurrence2Scalar0Left 140 = -((12399001518819038951116911447943331 * 10 ^ 70 + 5423637290590746212575002434204384302558959184244737317369448086960381) * 10 ^ 70 + 3272517007522258164825048308790096195064874716951719207080064362315291)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_141 :
Polynomial.coeff recurrence2Scalar0Left 141 = (133452302894542191610879553413638346 * 10 ^ 70 + 24241222561539122697732862275797466872666283435555417753413362725512) * 10 ^ 70 + 6631114002528863565461814107857030445596852716904912548542347568794305
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_142 :
Polynomial.coeff recurrence2Scalar0Left 142 = -((339058908489567814507253570903671457 * 10 ^ 70 + 5815187842960072397149045280837464935939313840844514707502352856139241) * 10 ^ 70 + 5533388301498163428540494628810982745492005741190259229327482580469890)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_143 :
Polynomial.coeff recurrence2Scalar0Left 143 = -((477575197657590189829384198623842990 * 10 ^ 70 + 3383952509297720533958650201559836145391957326736367842941792484789685) * 10 ^ 70 + 1912239191168239680218339509628372079516539935314550302640687018323592)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_144 :
Polynomial.coeff recurrence2Scalar0Left 144 = (5843831692139928351044593653277594690 * 10 ^ 70 + 9704053331288304180102261650384301529292331679321134504236320886146411) * 10 ^ 70 + 8582937731521692644192916364757085626950071595500690720346308875691466
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_145 :
Polynomial.coeff recurrence2Scalar0Left 145 = -((12945351499138117091221413881333513271 * 10 ^ 70 + 5200057910493800692412437921049342146630378380495684665096198857752932) * 10 ^ 70 + 2889852332887959814790309803608068860656172545565971307812915659240443)