Recurrence 4 lookup certificate: Scalar0Exceptional 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.recurrence4Scalar0Exceptional_coeff_431 :
Polynomial.coeff recurrence4Scalar0Exceptional 431 = ((1010896728865668191979546892499962542504482 * 10 ^ 70 + 3735850537170494337350446598611342198052282179943191118299247713610462) * 10 ^ 70 + 6804081925447386553013921449326053493557207375020268018233171533758874) * 10 ^ 70 + 4351327340339493723580493781402150965043689449115204274955116662740637
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_432 :
Polynomial.coeff recurrence4Scalar0Exceptional 432 = -(((341473744337158437367946794527974772208814 * 10 ^ 70 + 2651104280617289418171515694223740664139859318285804561594454324553307) * 10 ^ 70 + 8623202943592106874154509545149547568708328212601806031655820197392819) * 10 ^ 70 + 1137171995776457336990896506292105804374462420136132161451049813068375)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_433 :
Polynomial.coeff recurrence4Scalar0Exceptional 433 = ((76040621674297571714011341063741366988449 * 10 ^ 70 + 2432700909966596535159298189332276481449388898185516054127743692176746) * 10 ^ 70 + 2125027964302946153596980763878381317398180672197686918124280321800420) * 10 ^ 70 + 9045902879858398559355970019605952541460812509072503675739971176882660
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_434 :
Polynomial.coeff recurrence4Scalar0Exceptional 434 = -(((10334621263128917168373270903825324738060 * 10 ^ 70 + 626394402478028609294184881949568079399309317522624773879861478484686) * 10 ^ 70 + 6722410223132649687482033164201199036363367530043820081223350734152870) * 10 ^ 70 + 8961242513725903166799591384926978581175819667078898290895198010405411)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_435 :
Polynomial.coeff recurrence4Scalar0Exceptional 435 = -(((380576595200404339169099367472476598682 * 10 ^ 70 + 7264781448711213782213113085220257360292890901951727730866190108158274) * 10 ^ 70 + 2029386984325533873665498570689395120506633446540254658888708624177015) * 10 ^ 70 + 9212009137892315400233811313883414660975581319147231518683797472966854)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_436 :
Polynomial.coeff recurrence4Scalar0Exceptional 436 = ((803307473787058504660627045104409358132 * 10 ^ 70 + 3372891065337004547090636509066761923909199363679856038663210745466138) * 10 ^ 70 + 6945111480520393784453392703923843249507149949995605695941735732094875) * 10 ^ 70 + 9301524299771822887950423248820393859845140078628385246765661557943425
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_437 :
Polynomial.coeff recurrence4Scalar0Exceptional 437 = -(((321990930105059303121527959021152242442 * 10 ^ 70 + 6471886577675099764565183117935476460043938648751016286090902185331926) * 10 ^ 70 + 7660755369749955497984015921313751199054427505782555261237679907942426) * 10 ^ 70 + 9040555878594965859395204701101831022982816315523513474615376418977003)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_438 :
Polynomial.coeff recurrence4Scalar0Exceptional 438 = ((90879991361692918823411900265092268101 * 10 ^ 70 + 4695294349615868527029121919247214451976981759340502166702722943428991) * 10 ^ 70 + 34889839085139498103760094851773403819272520837882271071966792082061) * 10 ^ 70 + 7045071118127124302470741446595939053470676233379508541641365884277573
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_439 :
Polynomial.coeff recurrence4Scalar0Exceptional 439 = -(((20581679753009221524671363547728245848 * 10 ^ 70 + 4529635916391907629828913193733769916415926372819012272277301778330690) * 10 ^ 70 + 5285137458549522659509323049501044408312532024228648276847565517527804) * 10 ^ 70 + 2568281275203679899150670463748760786581827544557598246111240222611019)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_440 :
Polynomial.coeff recurrence4Scalar0Exceptional 440 = ((3820399604410282246951866410884743359 * 10 ^ 70 + 1351654698466901918785924346804202549108764919777357690870988058430494) * 10 ^ 70 + 1571357540896864528446426547875544866135926151493925433322484657455065) * 10 ^ 70 + 1407738802877950761481523647972370821235114896147712005004796550392274
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_441 :
Polynomial.coeff recurrence4Scalar0Exceptional 441 = -(((558170838316779481597228461029394928 * 10 ^ 70 + 6019365562369104634352303388938556650425885878783315051771913230223656) * 10 ^ 70 + 2874745751419333142248437137743573863000444601957489664028378062521660) * 10 ^ 70 + 9457408767066838297212841489518339688782789700383636803085221070995219)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_442 :
Polynomial.coeff recurrence4Scalar0Exceptional 442 = ((52624100406827810439617102082628524 * 10 ^ 70 + 8533015929326885706186267055583624498167585487630800798182964391949737) * 10 ^ 70 + 7161302478571228395334523997960618385127454106922517522887067115676610) * 10 ^ 70 + 8798807967547002194679878349673822855772614013696347010163400394268194