Recurrence 4 lookup certificate: Scalar2Second 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.recurrence4Scalar2Second_coeff_324 :
Polynomial.coeff recurrence4Scalar2Second 324 = (((5595251916595250 * 10 ^ 70 + 6392472924244193114591568797391894523767428714520017310922666554081906) * 10 ^ 70 + 7197352551908097896614114060546634965438390275372483622717089744129929) * 10 ^ 70 + 1761747720407930790068065838958424522124251563810791063497154401678955) * 10 ^ 70 + 2488725130975693685424182028977377179721208114955341864084015555273971
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_325 :
Polynomial.coeff recurrence4Scalar2Second 325 = -((((4156731585505111 * 10 ^ 70 + 970253666082392256342218977380132493093444798588434074512824723672930) * 10 ^ 70 + 4376359596143995063804537043008226275727904968106846306671959502224468) * 10 ^ 70 + 1642015424850294992710028544215393162283384257709150610195914961481995) * 10 ^ 70 + 5424675727249958079266576704743375207518470133172749624090208067227094)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_326 :
Polynomial.coeff recurrence4Scalar2Second 326 = (((2768598458179420 * 10 ^ 70 + 6116890019114472411163901839975792339876007292106554661880813881137028) * 10 ^ 70 + 7546585397509119839203387384106060355418296463778465605403765288086440) * 10 ^ 70 + 5702463254480043670583978851749491238179900884225304450859609521810846) * 10 ^ 70 + 2120777962212007449913021967888781855184145029064747587217693397042240
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_327 :
Polynomial.coeff recurrence4Scalar2Second 327 = -((((1722236880824795 * 10 ^ 70 + 3363293753995463065839534859408644346350252724859190951397593218480547) * 10 ^ 70 + 9438714612599624797736226884928613397215550374644038579839203484209070) * 10 ^ 70 + 8139856384187547814256690730794153170912063780001992062741822095732873) * 10 ^ 70 + 2979818948404754324621133772744790122384612853209077592122442212065007)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_328 :
Polynomial.coeff recurrence4Scalar2Second 328 = (((1020124856907655 * 10 ^ 70 + 6861631587951893636812048182642098938271996472167830645235540279979161) * 10 ^ 70 + 8060084185777976210782033151297924746182065696167647170588224404536329) * 10 ^ 70 + 4251517843512103965539781760804130878028320286168998018353942585264825) * 10 ^ 70 + 5593653282556290767408172289978629180716447710909414782402816375976899
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_329 :
Polynomial.coeff recurrence4Scalar2Second 329 = -((((581529206173517 * 10 ^ 70 + 6676886006125744247710067395788723747874630597529604971862471837206173) * 10 ^ 70 + 6090090587204439184650061106234599839571724263221590993632246429260266) * 10 ^ 70 + 9003783868899086586794484934048429055285103564670962923902918777564211) * 10 ^ 70 + 2447848049009486565215051802975881272903357391230923327082340745287576)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_330 :
Polynomial.coeff recurrence4Scalar2Second 330 = (((321110475621484 * 10 ^ 70 + 6790727226620639350057560034133821121359388232442027827176683533103012) * 10 ^ 70 + 3024497010567570310149153825396166436314837780374766673904009222319771) * 10 ^ 70 + 5419198136539314686476377953957958062274178880330630015926334671791653) * 10 ^ 70 + 5253079958033371496288417148455176405555946734916099454721421299577586
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_331 :
Polynomial.coeff recurrence4Scalar2Second 331 = -((((172470827633458 * 10 ^ 70 + 6159431687405218503186130601316560823351750632773608782905144584915806) * 10 ^ 70 + 3512631755551514345808436700908190012732591891799515995586902131011530) * 10 ^ 70 + 4754912612024415739389040845472986889961405623245392715504924819435165) * 10 ^ 70 + 6430226599912141015256430030575792304816715476045047868797744036166948)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_332 :
Polynomial.coeff recurrence4Scalar2Second 332 = (((90360310814198 * 10 ^ 70 + 6875240617517991035165933512211510092242348133586292810900418302209145) * 10 ^ 70 + 3949034725514341787129713896197980084942972744488618131215547752126836) * 10 ^ 70 + 5691101346135580791307529402918234815711636305207631704570727480961995) * 10 ^ 70 + 4948546503268905536761849908959478306456855837972649359190664158814576
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_333 :
Polynomial.coeff recurrence4Scalar2Second 333 = -((((46268694131063 * 10 ^ 70 + 2519797250806601397543797261113626432701007898278811317299927683119417) * 10 ^ 70 + 1988935449960526514989483946008358288053527778820544047467337604538234) * 10 ^ 70 + 4866853804710560498825841812151087954459547059340715717968876091000926) * 10 ^ 70 + 5607684525848754477455864098587000735068331324300249158098902189289263)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_334 :
Polynomial.coeff recurrence4Scalar2Second 334 = (((23186629355552 * 10 ^ 70 + 5812557417184280824094622001268641253599551961637587735500204992439476) * 10 ^ 70 + 5972968574737526331139581988658382067752234425099794010360475854573424) * 10 ^ 70 + 6859695278425864328505996061394055040636635248512318126848175416435048) * 10 ^ 70 + 4338891958532632069276713687775650726035533072584883470601926133523601
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_335 :
Polynomial.coeff recurrence4Scalar2Second 335 = -((((11382651761788 * 10 ^ 70 + 2245172678443245556464113590417833848449832183134968523546318918721728) * 10 ^ 70 + 5274425652230567798229949502000918177165594212942156570150218885927870) * 10 ^ 70 + 2653507857219412079263794243330413864502627295099041114399844630774102) * 10 ^ 70 + 9839137043166353074145300641353290373807921735429922199549708573131829)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_336 :
Polynomial.coeff recurrence4Scalar2Second 336 = (((5477565124270 * 10 ^ 70 + 6496879069400333190084478268024758349383255560863375953509757950291366) * 10 ^ 70 + 4675101167263509894336911031872298198435094492656816524855545730979729) * 10 ^ 70 + 3272715467359010690104339190090805053766236797811296017133319886245927) * 10 ^ 70 + 3793796695669134151869616919504639223987136292531366349115532896918749
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_337 :
Polynomial.coeff recurrence4Scalar2Second 337 = -((((2584947581926 * 10 ^ 70 + 2582625123734056551677926253634530994012242229292428396061718138643725) * 10 ^ 70 + 8114996883835852667237486285383374945745333638631136135854964923185515) * 10 ^ 70 + 2932973208279986344313183377578199496704546472065483712355789071605783) * 10 ^ 70 + 5941739726874469822473819472562156682465085735604042092283423973210444)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_338 :
Polynomial.coeff recurrence4Scalar2Second 338 = (((1196568650862 * 10 ^ 70 + 5900561863070254171061476623682973801857333145957309698375705505889891) * 10 ^ 70 + 158731546974460113201550292635215677634011271414786529375673628499250) * 10 ^ 70 + 6451086638170848368141879696191207305855375020574439325972928244070291) * 10 ^ 70 + 6012682891783013202768999490234036022590192719334146639471111861969672
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_339 :
Polynomial.coeff recurrence4Scalar2Second 339 = -((((543351689906 * 10 ^ 70 + 8538872901866257146720660521458580117469326438244102834327199325541358) * 10 ^ 70 + 1226875175053064738059107214620301161928204807723377149894580846679447) * 10 ^ 70 + 7122869513465079038175098237401965983586571989032619823130166004324963) * 10 ^ 70 + 1590025655972753954200516639897351093364914957490930498437422852344092)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_340 :
Polynomial.coeff recurrence4Scalar2Second 340 = (((242026273074 * 10 ^ 70 + 3009798894316339677170195986593449759777812702914205845984154253956041) * 10 ^ 70 + 1685380310258465177411509479197929609316543620689190388083072104001897) * 10 ^ 70 + 3407968566081440467514013618699952552715905804422687526156575621675377) * 10 ^ 70 + 7283456543970652986800828857955370032984778611163276082526398166836597
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_341 :
Polynomial.coeff recurrence4Scalar2Second 341 = -((((105734237165 * 10 ^ 70 + 4932104279047487310638241469366502979021122106536757370289532207259530) * 10 ^ 70 + 9513854376337957955215593251883792232747955880081693536117336035610681) * 10 ^ 70 + 4551070844230898079338344965082234361423302890264935450358017234688266) * 10 ^ 70 + 9879314670433307177107504325919118902582120709542213959909686975712996)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_342 :
Polynomial.coeff recurrence4Scalar2Second 342 = (((45293342915 * 10 ^ 70 + 7489775298368620051075319712726131412309776985923125948355863673466763) * 10 ^ 70 + 913915087345498081336591625162490984265901932207994897465735030942417) * 10 ^ 70 + 5054912503997468850441678358530566579967287989851890103156939602364150) * 10 ^ 70 + 9274141736876094748613305319407641026120218439774986421961948587703720
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_343 :
Polynomial.coeff recurrence4Scalar2Second 343 = -((((19018728839 * 10 ^ 70 + 1728224512914311033458272709808048697688346478681894067479243582845166) * 10 ^ 70 + 1922730900779946930328541134088896649226995170219416157901064878754765) * 10 ^ 70 + 7962699913930496375975711248143138055363965349756472920743381672053987) * 10 ^ 70 + 6970245011752527749769568804098978818692428067649354228885608594187683)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_344 :
Polynomial.coeff recurrence4Scalar2Second 344 = (((7825280664 * 10 ^ 70 + 3601927449185696390679806274090941033311609301201279849700888526898690) * 10 ^ 70 + 8655231556114352027391178548269302392731592993022818757852300205608699) * 10 ^ 70 + 5847367997912043903191648830523614123284858172838655823150610337044830) * 10 ^ 70 + 384516725501317189722015883292579798822800023491855136876114363832
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_345 :
Polynomial.coeff recurrence4Scalar2Second 345 = -((((3153775571 * 10 ^ 70 + 5175018259208044073358800952617003476803299193388599938995936422084743) * 10 ^ 70 + 1062124240439967398100574011579200647401941210496145521711013218244006) * 10 ^ 70 + 9451988721880185813412702777976268725400210402421147171655459888103060) * 10 ^ 70 + 9923589573339730291410359655493698270351501282275060437543311870848220)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_346 :
Polynomial.coeff recurrence4Scalar2Second 346 = (((1244638939 * 10 ^ 70 + 8750968444097180972202644871257166464333978787052128469407151934660027) * 10 ^ 70 + 6372730067928450979777923215580221110421567233508896149485108010148284) * 10 ^ 70 + 6233899623429915100790013825950561274854338488386723571114300894450710) * 10 ^ 70 + 2485138620493522517203332505231646022979010198605240453911003623610155
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_347 :
Polynomial.coeff recurrence4Scalar2Second 347 = -((((480935323 * 10 ^ 70 + 4933997523408705300402501450059027675152270987694590835502000190535247) * 10 ^ 70 + 1810974227216773007819479178407334563030567176247510736198626359730646) * 10 ^ 70 + 9938490698937705446173852904634316056357540605041571224657608648321272) * 10 ^ 70 + 4785495004746658015391720857029202175412287719843591508891584669370362)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_348 :
Polynomial.coeff recurrence4Scalar2Second 348 = (((182002406 * 10 ^ 70 + 1630168182907375094134900624430087626989327369610045012152752344074886) * 10 ^ 70 + 9403239507436398376825994435314036295416875639782408611009690121588644) * 10 ^ 70 + 3600327461243456088540846895836530478391740337774216498296770979802416) * 10 ^ 70 + 8964888521776926176789275756765351224605585227693955653424383948354235
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_349 :
Polynomial.coeff recurrence4Scalar2Second 349 = -((((67522175 * 10 ^ 70 + 6548553165996147796359318420241182642909162653012511439409975528428854) * 10 ^ 70 + 3173439040820977356800628958931524092261658073173465749482455265224077) * 10 ^ 70 + 2785543980651926621986154592519065717978591737074766143745273855800991) * 10 ^ 70 + 5566800927337579014821243884690319683232259276949763257978817861764878)