Recurrence 4 lookup certificate: Scalar1Left coefficient convolution

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

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_351 : Polynomial.coeff recurrence4Scalar1Left 351 = -((((120286399 * 10 ^ 70 + 795038765951331920897207116586230168831949434851944686391246222478535) * 10 ^ 70 + 3170646420601931149474393535555852897975475092641430907566193859481786) * 10 ^ 70 + 9931412122058466957116036521421166058537805424629585413411461700837005) * 10 ^ 70 + 4305759525204934575818925362936159859111166508380130147864848546677256)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_352 : Polynomial.coeff recurrence4Scalar1Left 352 = (((39750395 * 10 ^ 70 + 4895933724983486957291997673262798359616458752261978712710696761109721) * 10 ^ 70 + 9690490479356282465846809456540700770584571548990898758513610632271569) * 10 ^ 70 + 8000131154726115542605536590617349564753545793296735355571021421996366) * 10 ^ 70 + 7098130896101350151410972019116849254807403306547578922430607669640692

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_353 : Polynomial.coeff recurrence4Scalar1Left 353 = -((((12508380 * 10 ^ 70 + 3822864057199264277008250289671112121936538592286236274624506262232969) * 10 ^ 70 + 5211538758935952474923407541051599852913536618931787936836206180221562) * 10 ^ 70 + 7353066898691548108641884256060364851509696060621916698499939876936286) * 10 ^ 70 + 2729635835965326414801694891989242667758055331427046977876244108740500)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_354 : Polynomial.coeff recurrence4Scalar1Left 354 = (((3702217 * 10 ^ 70 + 6048683527745052234162796340102877244477409361896842778672857778717918) * 10 ^ 70 + 1378792908939720899282292590522060747821464216169142366910998601633874) * 10 ^ 70 + 4094045549776260302174692562376838102045154190706934251941268141948537) * 10 ^ 70 + 2025915748261855018581452350036285005549716742193880653700831481580424

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_355 : Polynomial.coeff recurrence4Scalar1Left 355 = -((((1008821 * 10 ^ 70 + 7078188887706410615125952080603839580566535273510190276019296667627549) * 10 ^ 70 + 6960559706073206808417326886987555289086788853897984522955492491276380) * 10 ^ 70 + 2463867411540786945414342065290589124853637392750252316664262986739641) * 10 ^ 70 + 9796620994238398601359577760997012736139317986644669469303511475087798)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_356 : Polynomial.coeff recurrence4Scalar1Left 356 = (((242040 * 10 ^ 70 + 2734782211184569437857577781202285894705612270552190508367122430379784) * 10 ^ 70 + 28154159435781260643288699911717190929129712933786682421754260334678) * 10 ^ 70 + 1676746829210537340907688805310085752698742612835737999207864014248562) * 10 ^ 70 + 2490027564600020418600592700262679685594937268070513437958773365609253

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_357 : Polynomial.coeff recurrence4Scalar1Left 357 = -((((45009 * 10 ^ 70 + 6429947153173596642186269220382339193702331069644871908110180211754309) * 10 ^ 70 + 5437867231745068921048131476961172457100290874897304264304708309123095) * 10 ^ 70 + 4084372780516176027991563013797734349523731932984732734297868879569307) * 10 ^ 70 + 6214594004021226323401238639367265695268880671683511417937432467036382)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_358 : Polynomial.coeff recurrence4Scalar1Left 358 = (((2522 * 10 ^ 70 + 5473627353250655218723292126653984080577593569814931331138311581748910) * 10 ^ 70 + 444941501286623502366299094756145390640184595435028412202557925316629) * 10 ^ 70 + 4934388009095920273739962114443318195907046866293496653586532263007504) * 10 ^ 70 + 3975382954877129045779227158368187865542959522070001823308692916198060

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_359 : Polynomial.coeff recurrence4Scalar1Left 359 = (((3285 * 10 ^ 70 + 4684946195347600780689717787337192974115760272326855531161497617592677) * 10 ^ 70 + 2657269964132117130598035816083669645967009490513332630595355675830421) * 10 ^ 70 + 4997378310377322136942044040915842153600781778704523429889560306326127) * 10 ^ 70 + 7924246084221425929490450624078068886351293727272941451913070811766492

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_360 : Polynomial.coeff recurrence4Scalar1Left 360 = -((((2439 * 10 ^ 70 + 7111159326811674972724991872578269905493061166865976424188110402557158) * 10 ^ 70 + 3074489799371091814897727583871586782218233510271723569857200208303280) * 10 ^ 70 + 3891078606433710878959895989243387948028255039710995342413589973639094) * 10 ^ 70 + 6170694491980429154087177133016560504498613421222209562296117700433462)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_361 : Polynomial.coeff recurrence4Scalar1Left 361 = (((1281 * 10 ^ 70 + 3026419537936591367750635730823830446013824065819929617539404729556377) * 10 ^ 70 + 7304228034957503374529507168804816981553333071287055169521268315195512) * 10 ^ 70 + 7748175043383812473894076592194591863238353949179435229586782521382848) * 10 ^ 70 + 2303240187442587373866573187221444245734640933006675074770160394215236

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_362 : Polynomial.coeff recurrence4Scalar1Left 362 = -((((618 * 10 ^ 70 + 3292519100409134695379961765047851174977949146156796973109956338415372) * 10 ^ 70 + 2534400982492667807980671999130790049404194875826922639465879359774619) * 10 ^ 70 + 3167358378072989183394801113263746305513584599206997751924099929364351) * 10 ^ 70 + 5578251181237359865942095772817200443247309388406649831480544131453476)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_363 : Polynomial.coeff recurrence4Scalar1Left 363 = (((299 * 10 ^ 70 + 998890255914638537770806959875256440834070846262967403238745649121076) * 10 ^ 70 + 9899227803492068755333069395650921599742571367950437779399482921441886) * 10 ^ 70 + 2453320011613009020037094819290724536292193682102333584060421844048833) * 10 ^ 70 + 4014332220827166327012822261110088958210302619303569366077173062668323

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_364 : Polynomial.coeff recurrence4Scalar1Left 364 = -((((149 * 10 ^ 70 + 2606646650913087244911236140376805647780768877393350541769153505836551) * 10 ^ 70 + 2135858228637600966357641320988686250058814036674464656472041011941957) * 10 ^ 70 + 5156535097862686436428054144577499623781145062512414108866966119449214) * 10 ^ 70 + 4876434431694021772123593735037298874877611465426583708012508290779253)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_365 : Polynomial.coeff recurrence4Scalar1Left 365 = (((76 * 10 ^ 70 + 3273487151685051300598831661791858694525140396988790013458473645254696) * 10 ^ 70 + 8723640428857386799950804889451816770789325948192003177053961344549762) * 10 ^ 70 + 4735118820421107204108316104921710323682788372439066977935644872503208) * 10 ^ 70 + 8391588697333888273031927034784870641324403565952339767078465772921561

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_366 : Polynomial.coeff recurrence4Scalar1Left 366 = -((((39 * 10 ^ 70 + 1468758905629910596849839831366868032581380920786593813955763412233008) * 10 ^ 70 + 1828221700820030429265598331883316203270814611207625271838883513311025) * 10 ^ 70 + 2547741186217554787974569181990505064485556528137173635268972292808932) * 10 ^ 70 + 9183851681381670201569228756034977831936617308229891764734093797797269)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_367 : Polynomial.coeff recurrence4Scalar1Left 367 = (((19 * 10 ^ 70 + 7336275690798807945599269190305428904004797835404189367305271988838503) * 10 ^ 70 + 8741989554930283786392657351603025519575230724431383274503286923079820) * 10 ^ 70 + 2802369499066589427466513298936511507868580259595788215871963328752084) * 10 ^ 70 + 644222007873088859592204207811773614894422035530570831033817477871954

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_368 : Polynomial.coeff recurrence4Scalar1Left 368 = -((((9 * 10 ^ 70 + 6465043000196833101638524330239864479766768207671266510395801052487523) * 10 ^ 70 + 3761360259714485838332306918138413099587472761014650766202639963005127) * 10 ^ 70 + 2838594862038518218738535975113015699004737080823063307020211020543760) * 10 ^ 70 + 370861328728594211005818480910128939754373468487102295575729516102141)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_369 : Polynomial.coeff recurrence4Scalar1Left 369 = (((4 * 10 ^ 70 + 5389401878868888227414780227184253382070741584795134157710049474816653) * 10 ^ 70 + 1928043833073265087657853752866389282218341066489388010794865675287128) * 10 ^ 70 + 2598793490802050409125458690862019509046199794408810721424568710058378) * 10 ^ 70 + 6618617878232280657264859288218716680842946654166920191159499713367884

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_370 : Polynomial.coeff recurrence4Scalar1Left 370 = -((((2 * 10 ^ 70 + 479733218762221458447180188128221889762229455988177374945681634988599) * 10 ^ 70 + 7343267896931898430714429283376078668804392859571180372040668848072189) * 10 ^ 70 + 2418620621461948136756500304630196610965698007171591761418423784788696) * 10 ^ 70 + 7370229509365208150520678304248380806224991048329319980559809676390267)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_371 : Polynomial.coeff recurrence4Scalar1Left 371 = ((8843006645530847008283591501381994255816421574603555224117913879215202 * 10 ^ 70 + 9636131120485547244753483961918262721168067547225524532880930659226610) * 10 ^ 70 + 8012860776328367651443428520480373108089372773896509990992763740177727) * 10 ^ 70 + 844914282464492881664292484368015765477574926469148255332622315101696

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_372 : Polynomial.coeff recurrence4Scalar1Left 372 = -(((3648382073412333222061561348652906840256521808867092491287770212749070 * 10 ^ 70 + 7240413498609567050821700023362432779178341824701445608935046649377637) * 10 ^ 70 + 5586701636989314276186645498549090123957202742767383381015591983536592) * 10 ^ 70 + 4891286175216737993559677057345066343741104546926511948948937144546611)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_373 : Polynomial.coeff recurrence4Scalar1Left 373 = ((1435361067908708978519196850778050859103179526633042196374572991383475 * 10 ^ 70 + 8470723994943814647364911403169693295245344660306176237253268604766895) * 10 ^ 70 + 3566002918688584564743675700297277429384642273002852269873417836730392) * 10 ^ 70 + 1314461527100605539055434015342209642703763886775615503848465719335187

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_374 : Polynomial.coeff recurrence4Scalar1Left 374 = -(((536784570330817203783269972957417230245697976627476645565931969367078 * 10 ^ 70 + 5350571527158693427593424886505071546125563152288390378816938253707857) * 10 ^ 70 + 1385460374595518709148559526998680397926687702365799340621817638895141) * 10 ^ 70 + 3826748285161867671589983929755363021271738758555721391840691888070940)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_375 : Polynomial.coeff recurrence4Scalar1Left 375 = ((189793332144890435190517802965787706757234988976009536977860560593633 * 10 ^ 70 + 8017998170692158779341176962781789707305335671078780376434657519894958) * 10 ^ 70 + 3486344398812608423256787257906251838188553179460854119967674293196670) * 10 ^ 70 + 8165234753002904511137324815335811951801777863260907092789586762632005

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_376 : Polynomial.coeff recurrence4Scalar1Left 376 = -(((62854138855448405342118671084633626610654951268749638312312524898154 * 10 ^ 70 + 7815946378458163527052963659437132901315476230760947871183191329877763) * 10 ^ 70 + 9376289580230863958256638946437135427206097973769861535385937327969902) * 10 ^ 70 + 2532164795404017709461322435853553916236266707364159162334449599573608)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_377 : Polynomial.coeff recurrence4Scalar1Left 377 = ((19160771257707081781073292680202174845763607484571715127607680662851 * 10 ^ 70 + 8157120390339633258717415796223669776706272047452964839076459144360447) * 10 ^ 70 + 5781648981856297595764885333483262565403136559220271211981661493914946) * 10 ^ 70 + 4649280921232186415501905639390271782096058074411047213253144588036517