Recurrence 4 lookup certificate: Scalar1First 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.recurrence4Scalar1First_coeff_384 : Polynomial.coeff recurrence4Scalar1First 384 = ((12204900858576666694737154951476219397819654870536717293851060741 * 10 ^ 70 + 6881646411325071197957329876219835063819754664723132719285796063202065) * 10 ^ 70 + 9527548674390232702346411693234258242982057431921552045833874266965061) * 10 ^ 70 + 4255087695874362596061739889810834105226769509754870429124356215542834

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_385 : Polynomial.coeff recurrence4Scalar1First 385 = -(((4499223418280417864160162119776585281656740311017334447491356044 * 10 ^ 70 + 4362737174375632248945310625381846738621049383497936909318814057023309) * 10 ^ 70 + 8291776068588762896816709313009856621092985181588158077938983838165387) * 10 ^ 70 + 1276772140421004618803539750058967870610496793166151012463552268310455)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_386 : Polynomial.coeff recurrence4Scalar1First 386 = ((1532548927771914364350050273420006236771027678498183469871711301 * 10 ^ 70 + 1292111233981291570804998055921240969567063578235352908817717752860451) * 10 ^ 70 + 3046420367942403368007097513521918803752606228720354431846601218806237) * 10 ^ 70 + 1292721351874295988864120794611272123628269050577044224014448741572249

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_387 : Polynomial.coeff recurrence4Scalar1First 387 = -(((483099392062704180343136605588131793160929468766700743940463613 * 10 ^ 70 + 3558098855630453231452442663869838858692089419522180092586570707641297) * 10 ^ 70 + 2936685130161567294503835031168176938763185433399481699192142752743693) * 10 ^ 70 + 8867927834814581868215665912495478882487819286960384485488159210659513)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_388 : Polynomial.coeff recurrence4Scalar1First 388 = ((139572627525093435548583520225923792810861683427608001650673873 * 10 ^ 70 + 7500081173575775768783051800676363596675511433727936830525474737982392) * 10 ^ 70 + 1053152500505410089353057756323355428818928388896097095887791428883558) * 10 ^ 70 + 7243781450096924080845656252154848500462072231803800371151442144265923

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_389 : Polynomial.coeff recurrence4Scalar1First 389 = -(((35923614105550759581598517760005949077534492713720341466932895 * 10 ^ 70 + 5786307847260609024483200931157424414495072997436058503160878046580582) * 10 ^ 70 + 1638153196688318731777644825194126638762818936475405673957130679798981) * 10 ^ 70 + 6369946816543268957795304431159008500505864652715187531210426544520824)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_390 : Polynomial.coeff recurrence4Scalar1First 390 = ((7602986761551684239757185977805075163748858620729669162437853 * 10 ^ 70 + 7905209683270755349055864186170230280140182657289112947246668778369527) * 10 ^ 70 + 1970072689583188178903915197592874272992858140404025914575149847815615) * 10 ^ 70 + 1290657597637193789283437350283383386859091341662993540469270972992936

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_391 : Polynomial.coeff recurrence4Scalar1First 391 = -(((921424972767487075453386005621359223165351457758210733394408 * 10 ^ 70 + 1215679436247451422953473907405534334868215793941579797295682893051913) * 10 ^ 70 + 4798497727618112862698648028492107313031912129402209959272843405033477) * 10 ^ 70 + 5966568975637369551282784261821270594931796776211914109119859625268631)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_392 : Polynomial.coeff recurrence4Scalar1First 392 = -(((240288852949163725845436687784898501433570010968313113766330 * 10 ^ 70 + 4374200957909788394994343205794167801401365582451470880965526743557946) * 10 ^ 70 + 642020357812775836959858628079778725055552597971323109648165135033114) * 10 ^ 70 + 348969679367361502496730899629825368392844126562547557742671374632647)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_393 : Polynomial.coeff recurrence4Scalar1First 393 = ((253384362893700793159340416274100552998192038688220713719702 * 10 ^ 70 + 7612957151719692375089356932687730460970009109898350794793547438055999) * 10 ^ 70 + 4572878041743270051399647388806988988994844840010216571525909534648242) * 10 ^ 70 + 3007051754591920895358632784616513511488713485067186748085132287197962

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_394 : Polynomial.coeff recurrence4Scalar1First 394 = -(((136037646539690565497043103647399562389398443151899500840474 * 10 ^ 70 + 2938070383197165619170766742590892414262748701135558648264373287194681) * 10 ^ 70 + 4865397364908982488527260176067621035193971051774000047329596190339477) * 10 ^ 70 + 3010243773347162526773707144606282629473829787378414498850519215585817)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_395 : Polynomial.coeff recurrence4Scalar1First 395 = ((59868053132371243435650693997577469416931415015996133529573 * 10 ^ 70 + 9083196518053629317408625371452427087800011209456566936178748223034043) * 10 ^ 70 + 5556315776349109958629075050149529043331272936167880084930376375832317) * 10 ^ 70 + 9367619048274364506499611554510170354481266726475326763006602392500008

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_396 : Polynomial.coeff recurrence4Scalar1First 396 = -(((23847436307716200588026251666996068403504758619446519421303 * 10 ^ 70 + 1220091653244842449583184898083685429297726192991542808162446080650758) * 10 ^ 70 + 4258620590754922290076891433320541483601972115683624563679710970882408) * 10 ^ 70 + 5854340270202101347829971697514414234482023382630253387495686985289960)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_397 : Polynomial.coeff recurrence4Scalar1First 397 = ((8947107138823702432002772981394590344945355944788697747223 * 10 ^ 70 + 7844095535791731296710140331683487960966144887182251238501308942824938) * 10 ^ 70 + 6754257398441178524741015724065530252151551655616459610298142379697800) * 10 ^ 70 + 7169466261701266894199714491723999696112907623713519267491873298054019

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_398 : Polynomial.coeff recurrence4Scalar1First 398 = -(((3227328677516584126420021757434369295218821030095435190569 * 10 ^ 70 + 8920602194745796819194006771742096724212531109018668266314800721949658) * 10 ^ 70 + 7859632260945548485902251955750605797589035624882853312487172164141358) * 10 ^ 70 + 6761327024524279629275135629074222934146800181333903582405114646190232)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_399 : Polynomial.coeff recurrence4Scalar1First 399 = ((1131995939189880608631948282698584141125431535993822011547 * 10 ^ 70 + 8864052363242655984073310343612141083170919957506548035882463312950696) * 10 ^ 70 + 3413216870247539925992706923069916660745463810426913785605321489579387) * 10 ^ 70 + 1889739814147164555620896271291001130792292111070139530583448020740487

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_400 : Polynomial.coeff recurrence4Scalar1First 400 = -(((388145498434093369312851364133658550900020402970864321649 * 10 ^ 70 + 7822138527263511545590238640020127461778341549127349545746254945596142) * 10 ^ 70 + 8006948097354716267837779000810388985555709350668572917346302306831757) * 10 ^ 70 + 2324877907631799846754320915935357767493774694074872891717040190546778)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_401 : Polynomial.coeff recurrence4Scalar1First 401 = ((130181584754645246680306352054577559646363044682260577636 * 10 ^ 70 + 2635220551912088632344896090302244988910924993202079586007622076990383) * 10 ^ 70 + 3878799517523248650609721466856966029208576776022724742990548486868328) * 10 ^ 70 + 5851234307197813391966741905867942031838254411986049860290723226432025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_402 : Polynomial.coeff recurrence4Scalar1First 402 = -(((42566862319890955177280898597346430305921129461327201423 * 10 ^ 70 + 3680695732861283931247205292399748186731725310989498284878224418815414) * 10 ^ 70 + 3224604189000073991459318733031865288379447051124065705317393299229317) * 10 ^ 70 + 5056371324699818531480013142565826878725632292944066996043945954907065)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_403 : Polynomial.coeff recurrence4Scalar1First 403 = ((13479491447253963470567951215560672626926432419154161397 * 10 ^ 70 + 2556464843042046134001547369330073207759830569792592303617521594630204) * 10 ^ 70 + 3562160870291514794184362583404019522346231876152682315306207913244312) * 10 ^ 70 + 7698687787352524527161459595903261082647432452936598447852792709657628

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_404 : Polynomial.coeff recurrence4Scalar1First 404 = -(((4092656204421569061614864142198881440423639989426437246 * 10 ^ 70 + 347902007175323113449875892232398434444074802741906257191660294021949) * 10 ^ 70 + 927607673198291705479288226954199778251265145368090914132169952580750) * 10 ^ 70 + 5899434468497932066638968565131939823438458653781305275935215068180244)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_405 : Polynomial.coeff recurrence4Scalar1First 405 = ((1173826241651622832615576570713860203862874943232834223 * 10 ^ 70 + 849619705468965439891400611410237787085396111301836427016167389466612) * 10 ^ 70 + 4331282801285834863448460485247240466712152998277920295753520325289842) * 10 ^ 70 + 7949431728819978443103109829550116023450022920784835336381393480943626

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_406 : Polynomial.coeff recurrence4Scalar1First 406 = -(((310192905256873961392066397237511988185410028819908267 * 10 ^ 70 + 227620716647283687328095068577816011803292493913815317394406326918721) * 10 ^ 70 + 9386761854886530729883321673982009335981838607273086269917313997233620) * 10 ^ 70 + 7316193516319007330970346438348446028936727167238488781641606909505859)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_407 : Polynomial.coeff recurrence4Scalar1First 407 = ((71667534006198999390806729955123774173709766185027814 * 10 ^ 70 + 6602450656779896079845692783626376661551071701748046480739342418711009) * 10 ^ 70 + 3741156098936704247851375851585787129811100064110279735093017344538483) * 10 ^ 70 + 9827395365369670073880213559599275240092163379357609364196157129259423