Recurrence 4 lookup certificate: Scalar2Left 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.recurrence4Scalar2Left_coeff_461 : Polynomial.coeff recurrence4Scalar2Left 461 = ((5195607978155525 * 10 ^ 70 + 1115686689755348376488765462736583726060817322447838325517073931072244) * 10 ^ 70 + 9706682681766049225422222989774677397076587876528587056052527436775876) * 10 ^ 70 + 3005657153257176903289678679673683456621311789168205347462013499676219

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_462 : Polynomial.coeff recurrence4Scalar2Left 462 = -(((220008892151241 * 10 ^ 70 + 3682252781606533405608460848958090980692664227037300306461036746637019) * 10 ^ 70 + 1598749936477585752158543302787586566814493309008958970559397467669939) * 10 ^ 70 + 3073424134178405428614393375409822593660882910821668830120179835141901)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_463 : Polynomial.coeff recurrence4Scalar2Left 463 = -(((2093933168459 * 10 ^ 70 + 463548787277066927091121703227192536546525204912623648253547345314005) * 10 ^ 70 + 9263493028689754277452226204033781602850804546618780263520770344207633) * 10 ^ 70 + 2622440234664817116967594798680265385202527650803530557590222442506276)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_464 : Polynomial.coeff recurrence4Scalar2Left 464 = ((1448358195719 * 10 ^ 70 + 6265161717375611422444443048465833713884451788913641411820446337987227) * 10 ^ 70 + 5111192096065166187684265999815913763956174964309671741441938547679122) * 10 ^ 70 + 8863077471433670316338827256469748386932601201831298860372492890417549

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_465 : Polynomial.coeff recurrence4Scalar2Left 465 = -(((157748363291 * 10 ^ 70 + 8668388000560056056755387707024857196724165942921887216587342957858312) * 10 ^ 70 + 9734360932773449006269935023379684538649744349634474100324752416711835) * 10 ^ 70 + 3738963567129152054585146642105398112936775190003009662499399400941186)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_466 : Polynomial.coeff recurrence4Scalar2Left 466 = ((10853732806 * 10 ^ 70 + 7407686281001423564229402725439533494956840695246416475813449768978414) * 10 ^ 70 + 2759949388684503722234699338429039953156920131777605572251016225266201) * 10 ^ 70 + 5748793474163765269535013085670153369641063058454116062251021693014826

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_467 : Polynomial.coeff recurrence4Scalar2Left 467 = -(((500626312 * 10 ^ 70 + 3267248047145218034908499201438536676302291317719267479358664151170783) * 10 ^ 70 + 9148551876918932187243550323040570736016177582336149248895471910776479) * 10 ^ 70 + 5444431168886479986934375699145942652763374659115014695726818561170924)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_468 : Polynomial.coeff recurrence4Scalar2Left 468 = ((11867582 * 10 ^ 70 + 9117661176534081674763275798157958790168108314436521009730407823907604) * 10 ^ 70 + 2019776349614608166121663713723710167367771481084011369530201945081523) * 10 ^ 70 + 5842316290367601097185086375599408190085531872651300528852578982666058

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_469 : Polynomial.coeff recurrence4Scalar2Left 469 = ((287611 * 10 ^ 70 + 8986643804276758840844885382323679502345448547216666376451423113612481) * 10 ^ 70 + 2386208315364040796971280344711788089417188813849556108691543656031095) * 10 ^ 70 + 3313716920897508994742701709412919614319677588887024923914018015128856

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_470 : Polynomial.coeff recurrence4Scalar2Left 470 = -(((42271 * 10 ^ 70 + 2318096464655900051741985977104130975130557484011306981148346996705264) * 10 ^ 70 + 1884418204947317711112442684094437871398835661332951655529749140737918) * 10 ^ 70 + 1573176683270643636443725197223804722475125539134060704630528461889627)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_471 : Polynomial.coeff recurrence4Scalar2Left 471 = ((1965 * 10 ^ 70 + 942842719379591015446233432835756162722398437529475348097077644526388) * 10 ^ 70 + 3697990625985723752040611813670937034607239540694773522777537529159655) * 10 ^ 70 + 4032810863231593449906780291735808413516298966780435581537944905559139

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_472 : Polynomial.coeff recurrence4Scalar2Left 472 = -(((41 * 10 ^ 70 + 4063950631997650183619748014208974689836162760819708306993773204079504) * 10 ^ 70 + 4424940604634429333393880390841422196461907900382266437156600375674293) * 10 ^ 70 + 2625460216692103642070203372850676902189568193682627144542931608177552)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_473 : Polynomial.coeff recurrence4Scalar2Left 473 = -((3257370312778615221637997911683363945732684975818138050994339139669967 * 10 ^ 70 + 5718978700098846206273920479426890123762828282822440878102089351759746) * 10 ^ 70 + 3058732578885438914066017280840909473710652696306259020865145761623549)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_474 : Polynomial.coeff recurrence4Scalar2Left 474 = (431893996961065423838969530126388799143570221474810941615871833340405 * 10 ^ 70 + 1175244326083672993911367896102873074123859464384144751136565502873944) * 10 ^ 70 + 7403644277616772445160791468659945310180830732110067076826524102246178

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_475 : Polynomial.coeff recurrence4Scalar2Left 475 = -((8699007739552546716773914844575482911973880650356219984911599949583 * 10 ^ 70 + 9717589189579512712727907215664553824326780495407513115372202251490368) * 10 ^ 70 + 1750954718780492753594285365479824266506275819703600883447971668424658)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_476 : Polynomial.coeff recurrence4Scalar2Left 476 = -((43090521349718311476840999464135472531102986075675437387778590315 * 10 ^ 70 + 4139630417587685544526017393639477469425998806068286960598707430847046) * 10 ^ 70 + 5643206625841609829236166929827905713366344679722430135258674711843075)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_477 : Polynomial.coeff recurrence4Scalar2Left 477 = (3478309230957860055769347664465270141071000530602651891560797338 * 10 ^ 70 + 4096932541269642489146414493641107081076941431290888525954521302979223) * 10 ^ 70 + 4653337311040322110592667262136755159767994408044882497091176754514823

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_478 : Polynomial.coeff recurrence4Scalar2Left 478 = -((11964092151908318507467355459023430140265648979050666500985359 * 10 ^ 70 + 1157203503759777372697495905262293950095049118074638842627411469396652) * 10 ^ 70 + 9571631071560808495564513915125704021090022573444653669078288444807122)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_479 : Polynomial.coeff recurrence4Scalar2Left 479 = -((591154847903726400970581097772845468356311306891257492979599 * 10 ^ 70 + 7121416335022721217315660687714754026843513381858239447984243282780603) * 10 ^ 70 + 333545887363300287081538622297944187451933802179137991776440947206106)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_480 : Polynomial.coeff recurrence4Scalar2Left 480 = (1781095777866350687961040615594806070683105911959588402274 * 10 ^ 70 + 8741995260596668973887530424074950142510999010441415242594531746446597) * 10 ^ 70 + 184723804486900687290946172567554599130687082263360529941496347872189

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_481 : Polynomial.coeff recurrence4Scalar2Left 481 = (56572847228842456422901581309817646297546672565303143020 * 10 ^ 70 + 550796713726972265643794801062954257279693657998352508757284173396778) * 10 ^ 70 + 7947628094738616448801252836552719542279024294462160352143318194918554

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_482 : Polynomial.coeff recurrence4Scalar2Left 482 = -((6588901554284596095313409911562086382678291906772608 * 10 ^ 70 + 612876722517431218939320648748024687213198946863808635475294365139078) * 10 ^ 70 + 4854904984526101383585291631810185385557849169831095635250159732878517)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_483 : Polynomial.coeff recurrence4Scalar2Left 483 = -((2520182549979306304800161997611555400712833889054990 * 10 ^ 70 + 2216869425917039980051856065829162313612661487281851639059642346258029) * 10 ^ 70 + 9900417695066921270629748296671857661988554547080060114841941618907128)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_484 : Polynomial.coeff recurrence4Scalar2Left 484 = -((3912281446394025715272358044769956793288684803911 * 10 ^ 70 + 7727045559420187113063068116668930825226361308877282836232074329842583) * 10 ^ 70 + 3607160358500002621202673682330178657165709118459880545808939903318356)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_485 : Polynomial.coeff recurrence4Scalar2Left 485 = (54487697609868225671193490158449120376303932174 * 10 ^ 70 + 868668314413640865242061637170767552454091990806606569638200581533683) * 10 ^ 70 + 5898712846485633074574990837474846923762809734543318547680597342567054

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_486 : Polynomial.coeff recurrence4Scalar2Left 486 = (130423936972181799823155727158036309805411957 * 10 ^ 70 + 3522164028348769194978832941963273108868265985605399590722072845832753) * 10 ^ 70 + 4086855687195610557863247886776221913553032651573747656186860585921841

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_487 : Polynomial.coeff recurrence4Scalar2Left 487 = -((613921033389389689195702609686329740987955 * 10 ^ 70 + 5787013660001316049795138328307803938527586851767728088245080528734508) * 10 ^ 70 + 3497634860184175763000353512830903977507147696859078026761761944961626)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_488 : Polynomial.coeff recurrence4Scalar2Left 488 = -((1636155860588797259421959362477917188912 * 10 ^ 70 + 5634790556342186593503950344113590472487818580661768952956045624354495) * 10 ^ 70 + 696047250892501296519936402924211456138138612471888279849842649986596)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_489 : Polynomial.coeff recurrence4Scalar2Left 489 = (4303643889618364186628810103902607322 * 10 ^ 70 + 6188227881682108922270161984457506827058224204553290401464284443521589) * 10 ^ 70 + 2362096371610240721251475565445769736853305068055657376371915217310365