Recurrence 5 lookup certificate: Scalar0Left coefficient convolution

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

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_356 : Polynomial.coeff recurrence5Scalar0Left 356 = -((((1540805000385634063514866021003986082829947 * 10 ^ 70 + 5769698562360845862891265260205034811630965111386726890651981444748062) * 10 ^ 70 + 9024911722705909388964166392219002201485308165525054962864639458789309) * 10 ^ 70 + 6307565048600901341773878861860693456687624207250513671711170341423641) * 10 ^ 70 + 5477707783068228115391762757669961051036782520311692382705099940590495)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_357 : Polynomial.coeff recurrence5Scalar0Left 357 = -((((1815659278641657925979496664888516034959822 * 10 ^ 70 + 6922891205772452812215337310339373462000792750247270416892886564400351) * 10 ^ 70 + 8197293676793398149661697699006069413036383379457620671973146264396874) * 10 ^ 70 + 6282777633121359946872032473639233807315036960117889413715878597713297) * 10 ^ 70 + 5748794193717905466699402675048502265878850121775146612964150775031266)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_358 : Polynomial.coeff recurrence5Scalar0Left 358 = (((1353463885365118436181181340611623211730901 * 10 ^ 70 + 8445681008002356764927026732466218474790323652951415715174719730034413) * 10 ^ 70 + 6319387368213279900002891536859820933224833385654770562253596253486120) * 10 ^ 70 + 8218388519048539723324346786155295277280825126545508998342209218867123) * 10 ^ 70 + 5612004119566806972878147891711226334795678422765502185531552302181401

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_359 : Polynomial.coeff recurrence5Scalar0Left 359 = -((((688957574088480514798097237898299403684682 * 10 ^ 70 + 786850383103898675153804509683026307599372004585536010962315759195390) * 10 ^ 70 + 8487590425748486787333853808475891432393738260344582364564129550249428) * 10 ^ 70 + 4231019296520805224288545535361961624331486883451219615824245983404155) * 10 ^ 70 + 5596812229731986938493815507775818533297879280300147264581752672761205)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_360 : Polynomial.coeff recurrence5Scalar0Left 360 = (((304861209917412323380202766367609967398767 * 10 ^ 70 + 3360032716290459012196691552182336306909643687761054912822204711378375) * 10 ^ 70 + 9736351556111163703300499968197670523150617888741346555711972043849675) * 10 ^ 70 + 6481771524423060087377039104549923075754323751958283636051570134378767) * 10 ^ 70 + 3475541938104324216817797468736083985861593664109186357650559841574226

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_361 : Polynomial.coeff recurrence5Scalar0Left 361 = -((((125384011508318965194911409329421733644556 * 10 ^ 70 + 9681187899355391983617118850811744120422710520222271749149690911419036) * 10 ^ 70 + 4269590583058933752323941048095468408345390008444302182655136012379027) * 10 ^ 70 + 9085535673640153891680038706317597276084493919281588412671276630401079) * 10 ^ 70 + 3618782539317198578159902238758041339190310500140642060420814020062636)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_362 : Polynomial.coeff recurrence5Scalar0Left 362 = (((49301602442385354758878125412915429111898 * 10 ^ 70 + 947749081165005302227580450564811433733025824098344125318765809006612) * 10 ^ 70 + 9498926771442028679421548575571410497683593547745151854526157439803664) * 10 ^ 70 + 3286225026931803841246461970504995763322677716798234376351892206387525) * 10 ^ 70 + 2517087693557430553846491096163652604073168062990395055302783168767568

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_363 : Polynomial.coeff recurrence5Scalar0Left 363 = -((((18796240410947086937009001690393122921761 * 10 ^ 70 + 4342864175560321263702963180221265505196529201973034575589458956566462) * 10 ^ 70 + 1192002598173603473148838153485729780536211499142120670725243846202838) * 10 ^ 70 + 8289595289923507215959235885448587630410141837213016249822066339270356) * 10 ^ 70 + 3052750723509992155935253370329022700489095547538648762171293869687037)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_364 : Polynomial.coeff recurrence5Scalar0Left 364 = (((6999758519941657003841478668693695403784 * 10 ^ 70 + 832052995576606264424302464084996118000529511304910850897218801366304) * 10 ^ 70 + 1953342949087557615511772697719042337781074996263502321659193999716854) * 10 ^ 70 + 1137797574431814525130564765630290490564804541933010920500590445206936) * 10 ^ 70 + 1297129174384139820446169966405114514647712103577395175087272144484545

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_365 : Polynomial.coeff recurrence5Scalar0Left 365 = -((((2555703711345631944565105102646743830850 * 10 ^ 70 + 9019215782530339257724468291845265949104124921383053216692344545162691) * 10 ^ 70 + 8417953286428150592781663219115747757839880524030809200637270908799173) * 10 ^ 70 + 6765421924411510026550536240071265910319420462425608942293663690316848) * 10 ^ 70 + 8981444347175130307048927206171180587574133372634388888116448948734711)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_366 : Polynomial.coeff recurrence5Scalar0Left 366 = (((916268039671982135327736237853599521555 * 10 ^ 70 + 3974595625527336198829563159948055968240450084901342670933032837940972) * 10 ^ 70 + 109177612618527831330970431410247738496705290570095870284283875663694) * 10 ^ 70 + 8984701516394193145725140203868353019935674796407899535127391052620804) * 10 ^ 70 + 4049169590200072284853805672133683051931090653793880440736519159085392

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_367 : Polynomial.coeff recurrence5Scalar0Left 367 = -((((322650203016041235605492692294041759782 * 10 ^ 70 + 6958061809402831351682456658873835372929403357875358791612856257721546) * 10 ^ 70 + 7667605735750473047229489922049298054342655893340378735096849966733979) * 10 ^ 70 + 7443283695973359262465317228371184967821765660892834346018738644233571) * 10 ^ 70 + 7480632409700889179511939363996446982748504147689124428869252252080700)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_368 : Polynomial.coeff recurrence5Scalar0Left 368 = (((111544252854418804869496462172290678172 * 10 ^ 70 + 9962909084071730969888234667350686736008897136625307838705004716501566) * 10 ^ 70 + 3102222967802615629378359374547483558057801680322751995695587198017142) * 10 ^ 70 + 56949665383758278923073876286221192092153652740161772359248136615043) * 10 ^ 70 + 572934276984121498687690422914471157970304025336670296846673174045991

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_369 : Polynomial.coeff recurrence5Scalar0Left 369 = -((((37830211956728386190155804106291151918 * 10 ^ 70 + 9285990887931121650285128873579845918875139336032750907414150635789852) * 10 ^ 70 + 5148767103837095794100854495866221440918707608096530066177494897441443) * 10 ^ 70 + 1197091374032649320801780930259206063723024526695337188708434962528775) * 10 ^ 70 + 3975305150992574117857345394562939403985057350297006007116477256348324)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_370 : Polynomial.coeff recurrence5Scalar0Left 370 = (((12576020506645054277759381390511515136 * 10 ^ 70 + 707577018621267247633738711544527930140714007570545382020783151419167) * 10 ^ 70 + 5233262699408719879068508785692198733060281336825113903567719709906998) * 10 ^ 70 + 4437128005564921255034763445454857240093996979111607992952812588055624) * 10 ^ 70 + 1449044246201732699854356911630101074730324376370765404068850163093397

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_371 : Polynomial.coeff recurrence5Scalar0Left 371 = -((((4094688112130149294089409108340039914 * 10 ^ 70 + 3000228117507362016264581612473238807716404872424573838906237695236816) * 10 ^ 70 + 9270704708500755004758865093804501432579843004408471349710340970316801) * 10 ^ 70 + 2429336179273091667343442926860968954883361103173182862556546785118829) * 10 ^ 70 + 9291551344463701125018465112358642611742850998959031623802783430284528)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_372 : Polynomial.coeff recurrence5Scalar0Left 372 = (((1304905552068871030691527782729345242 * 10 ^ 70 + 2562800783549824240946450561605809427644344251992582846819780365224987) * 10 ^ 70 + 3258789484641439266535842946284750072963065946331884459803173422029406) * 10 ^ 70 + 344321652693923917441464237403849247672017928930857234405427553610409) * 10 ^ 70 + 6717909606506025563443908633457886355245710667341232474993589861588044

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_373 : Polynomial.coeff recurrence5Scalar0Left 373 = -((((406792395880018581147310759672761348 * 10 ^ 70 + 6326785862264079560842391180700326955163246087933253110373106628395636) * 10 ^ 70 + 9531328773122642864906511647371788058313031667499291476308889356907233) * 10 ^ 70 + 8784292188355688138401658653087732016826891977149017148879421096902266) * 10 ^ 70 + 6661782610747927865364273661173138114589477238223837153254527399851976)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_374 : Polynomial.coeff recurrence5Scalar0Left 374 = (((123990612484345002914266670012796284 * 10 ^ 70 + 8337124523116711629603163620578431205427758479076063782990472341915087) * 10 ^ 70 + 2971820321109237766245941363121958287505100465778726086349827606446463) * 10 ^ 70 + 7099863673226697399657636937398751610841598019080636432622738827964103) * 10 ^ 70 + 459871310805153393956604725114197911159432622510048370349187125469983

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_375 : Polynomial.coeff recurrence5Scalar0Left 375 = -((((36933550703999210446091307621164827 * 10 ^ 70 + 5185906630983483220923996856682426204272669761486319069344258398783900) * 10 ^ 70 + 1139507559637086823123328834865047293468756932070058993117278850258863) * 10 ^ 70 + 8343736630818686709044902357698590196022506978194461824302324089584149) * 10 ^ 70 + 5484806662828600055891742810638032977184080251887772510215353700020287)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_376 : Polynomial.coeff recurrence5Scalar0Left 376 = (((10745876239378985830643536806465516 * 10 ^ 70 + 2134384043575172718157409254288376233960382882632998925999263023032382) * 10 ^ 70 + 2935409116803395641063024023493733372854264871876539870432585916784838) * 10 ^ 70 + 619029709772504298192014776347717264866833666077181419436567023817673) * 10 ^ 70 + 1720496167145368795915769253109017533785651916825665923020913761907232

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_377 : Polynomial.coeff recurrence5Scalar0Left 377 = -((((3051907623375107533111087486654951 * 10 ^ 70 + 5917938187679537901901081682496314989012693560784996833386203457832890) * 10 ^ 70 + 3285259651412148601511709950975291001448202281840086717297382135566493) * 10 ^ 70 + 2866028164290380684407327757356110986568552197543486224495053965928218) * 10 ^ 70 + 5703569318543869435345358480013222864408635262566202738303417050683344)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_378 : Polynomial.coeff recurrence5Scalar0Left 378 = (((845374394577836549228254283439225 * 10 ^ 70 + 7911904506057124378891306304879731089077208539243904363728967824692276) * 10 ^ 70 + 6455672359819513938927519577552395000074305610262600591908674136903803) * 10 ^ 70 + 431343834956702676143060860504448062116427393110502655626178125540425) * 10 ^ 70 + 5232858873639978203614811034548006470578528394199881001893442302391560

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_379 : Polynomial.coeff recurrence5Scalar0Left 379 = -((((228142720466314975797491721477142 * 10 ^ 70 + 6201295798164487451179886368772127387274582877673707721731348280345127) * 10 ^ 70 + 7104016260937621696488908253376428737368077163725619184330705423890709) * 10 ^ 70 + 5721523814554652725320567744252773908098422383151839644141882216250981) * 10 ^ 70 + 2640908117124440321085835197838112498620047630436237259053363569524394)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_380 : Polynomial.coeff recurrence5Scalar0Left 380 = (((59902024412164280868922745051441 * 10 ^ 70 + 1043860657117500888296550021811726229524199808003364098365222492867778) * 10 ^ 70 + 4483067369672147789882477283400248817838928351153682072044371682489146) * 10 ^ 70 + 5232391705977502388568669965568443352742908764866237575811637469708271) * 10 ^ 70 + 7329024649237506271961914248819774374335217353917884938809546196660085

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_381 : Polynomial.coeff recurrence5Scalar0Left 381 = -((((15275153434852621059394750948168 * 10 ^ 70 + 2976172684299868832639589034404625291372975950170696496864754186177981) * 10 ^ 70 + 3377967190559636281510240833039043308887843982836983679960306435417777) * 10 ^ 70 + 1854616879425067165186679068258027622912855238777946261298652713038276) * 10 ^ 70 + 9296857692426916351307567819062166772453082051107088503231895081570326)