Recurrence 4 lookup certificate: Scalar0Left 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.recurrence4Scalar0Left_coeff_41 :
Polynomial.coeff recurrence4Scalar0Left 41 = (38001 * 10 ^ 70 + 5281154893136255016670484768814372122353520153118030782931967139550779) * 10 ^ 70 + 1149150433381571411427574049261753981101940435694595870813860770556192
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_42 :
Polynomial.coeff recurrence4Scalar0Left 42 = -((4558517 * 10 ^ 70 + 4260162740111173661251142196996193155541469239280333940658676694824779) * 10 ^ 70 + 9869163515079238264490496138039070297498702919421614501463058117983600)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_43 :
Polynomial.coeff recurrence4Scalar0Left 43 = (443190844 * 10 ^ 70 + 6694123409281301221569022275883461789472928056782417762011888047430581) * 10 ^ 70 + 6543614874964110480550307228085215688886057389110851282461568763032344
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_44 :
Polynomial.coeff recurrence4Scalar0Left 44 = -((34527517776 * 10 ^ 70 + 2533904207089532906223147920152272953564480188397780369275393043113081) * 10 ^ 70 + 2576623312912762317353579325972093152850924712443762909387893598217976)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_45 :
Polynomial.coeff recurrence4Scalar0Left 45 = (1910832277761 * 10 ^ 70 + 4785779100988140419101845934704381011308919785663287383054648242595294) * 10 ^ 70 + 6987449279366145714819692895908604429702891253175307895454957028895547
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_46 :
Polynomial.coeff recurrence4Scalar0Left 46 = -((22781767535167 * 10 ^ 70 + 6023402979944987577577754790006636691779656473697242080076937979870708) * 10 ^ 70 + 9052427899566584058026022566736773443004634521464786416647159816462937)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_47 :
Polynomial.coeff recurrence4Scalar0Left 47 = -((12028918499149839 * 10 ^ 70 + 1846144379037361221944721551379118233937550354177136922437781808997868) * 10 ^ 70 + 2093810432418136430729156431220034479096616075020536689716959542656287)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_48 :
Polynomial.coeff recurrence4Scalar0Left 48 = (2136368621102294231 * 10 ^ 70 + 1079750537344504929876182011649666485911989174917325815599412911145869) * 10 ^ 70 + 6227561630131234524403065074509872953436241574619765403901242707751530
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_49 :
Polynomial.coeff recurrence4Scalar0Left 49 = -((251547369497685171175 * 10 ^ 70 + 7824942957700164079081590366373891448027260376137528997652384171467270) * 10 ^ 70 + 6209282206947599568105339281768064329716014120715673586643718153159222)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_50 :
Polynomial.coeff recurrence4Scalar0Left 50 = (24346248404410341157012 * 10 ^ 70 + 1514641543862408058511125639660316210423639262299550993736213131364567) * 10 ^ 70 + 3426164228166857885840637225827561187690250939306269609950240497019275
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_51 :
Polynomial.coeff recurrence4Scalar0Left 51 = -((2064406062535130821722014 * 10 ^ 70 + 4463286506593592066321072564980104259565514056721030699071021318119984) * 10 ^ 70 + 2702179945183116400006670290058663873999981334237329245781253580254557)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_52 :
Polynomial.coeff recurrence4Scalar0Left 52 = (157789986329012843071787155 * 10 ^ 70 + 8254931901052224852216906721650421109502634479381740787856220660602042) * 10 ^ 70 + 1096388111164052151511227265247656518290502649625290571836965688568302
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_53 :
Polynomial.coeff recurrence4Scalar0Left 53 = -((11042594003763968968714548594 * 10 ^ 70 + 1495239039181503563604517722576282135341192730858790811923489064085013) * 10 ^ 70 + 5357788014430445404699853096795617806995853483725641984749397475338950)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_54 :
Polynomial.coeff recurrence4Scalar0Left 54 = (714491855508415378571944036865 * 10 ^ 70 + 2266349460104601107895469291887679533835288710648929764047595804303177) * 10 ^ 70 + 1107255919611041330435694578080393042700531492557935258018009044046853
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_55 :
Polynomial.coeff recurrence4Scalar0Left 55 = -((43025889348345054023874462573630 * 10 ^ 70 + 5749874122913476493408122567728166161603717152314568730035211752832066) * 10 ^ 70 + 8107804106089387748339082585014806453554852149610797836317510974328255)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_56 :
Polynomial.coeff recurrence4Scalar0Left 56 = (2422955436231366272363475581324589 * 10 ^ 70 + 3913743660051217937144880151326754942471077164907071611153114054693994) * 10 ^ 70 + 6882735750177578499165664238509108240030102573038503113602891544274283
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_57 :
Polynomial.coeff recurrence4Scalar0Left 57 = -((128060700447982653354194803887280913 * 10 ^ 70 + 3528281100109894536392630801211186599645506724827706384416952435401606) * 10 ^ 70 + 4730462643776946129814150113793112566042212858758356722917009318387751)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_58 :
Polynomial.coeff recurrence4Scalar0Left 58 = (6370472363502890833301238446746037215 * 10 ^ 70 + 1426259858183905892829797053978458735410977887705093075718850991120769) * 10 ^ 70 + 5064730399999307804433036624194506642510338402661162267592912700303122
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_59 :
Polynomial.coeff recurrence4Scalar0Left 59 = -((298950335688795679033121401750533446460 * 10 ^ 70 + 4897027325534179392091961693504515270762382367568135652547344611721080) * 10 ^ 70 + 362832568416544108532751014887722425690026589396449133342615773028926)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_60 :
Polynomial.coeff recurrence4Scalar0Left 60 = (13258694976504515455742934688053724842740 * 10 ^ 70 + 1957872107783871608158495256219345385806526793343723287574624850092788) * 10 ^ 70 + 7768213451550156840085158999961877697023517608791690522606264702979289
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_61 :
Polynomial.coeff recurrence4Scalar0Left 61 = -((556588575939450457332142574338175650376381 * 10 ^ 70 + 8271354462440336025928278939570000684896961242616799953854204575871767) * 10 ^ 70 + 9029405088391327431177058498987695223061272514726180676314291521066647)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_62 :
Polynomial.coeff recurrence4Scalar0Left 62 = (22142983355844128234871920744080284027573785 * 10 ^ 70 + 9222597438941621098751869863563950937900602155060159814430356536681840) * 10 ^ 70 + 5025798318948384387178856405863890527852060067816209514817920992254143
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_63 :
Polynomial.coeff recurrence4Scalar0Left 63 = -((835673477117309394887862658160478524667008582 * 10 ^ 70 + 1227959176380755363957954972386540387996833902587104093537533086707945) * 10 ^ 70 + 3722358511081787613137615415765028599976479896596557785744433119218496)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_64 :
Polynomial.coeff recurrence4Scalar0Left 64 = (29941050005790950197393061624020788742229907079 * 10 ^ 70 + 7185916946845149611366257882949696615746771878271008823694700661655390) * 10 ^ 70 + 2590446883976693199168689324880387535601424094121408429725587538859184
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_65 :
Polynomial.coeff recurrence4Scalar0Left 65 = -((1018967864265472528376782959271976095085877753406 * 10 ^ 70 + 9990714852605643035644477961406552824711602521376279649830998716033488) * 10 ^ 70 + 2117131178673134445239342996495352595322326792912073010091777755428087)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_66 :
Polynomial.coeff recurrence4Scalar0Left 66 = (32949320014544056050641747627004905683712728247160 * 10 ^ 70 + 6614940447028224034398510890156795562436944343788217598553303524128356) * 10 ^ 70 + 4250926913547332097091759878109112821786784036973703088598253834254367
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_67 :
Polynomial.coeff recurrence4Scalar0Left 67 = -((1012366463098095292706572077936745255109342006523891 * 10 ^ 70 + 9224615700322817432143639983394190760983834389936332255630049250548455) * 10 ^ 70 + 6428654714729838699742654992854730525210678906769045199084671306442733)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_68 :
Polynomial.coeff recurrence4Scalar0Left 68 = (29546614845204339697551798039632090456291729479790275 * 10 ^ 70 + 8328702251288317992591405250805296021744454338638758047790157656628768) * 10 ^ 70 + 4562809395644025728128387583871391054402091984152960425374315536240996
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_69 :
Polynomial.coeff recurrence4Scalar0Left 69 = -((818564810270816566380241802057809433833602845513007015 * 10 ^ 70 + 9023657315438892267341899289592815383590996247027252720843369334192160) * 10 ^ 70 + 5525998226743206481788582516878737191545336850733740646393171327180885)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_70 :
Polynomial.coeff recurrence4Scalar0Left 70 = (21499763434067793421474101801215550727478434484859157425 * 10 ^ 70 + 8113859410640711325896823804742105974421480993837927331384588629864058) * 10 ^ 70 + 1735582091587726997536136117436992227213052365835734988653953420208250
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_71 :
Polynomial.coeff recurrence4Scalar0Left 71 = -((534286216755380557396827564349533087523418983223039461780 * 10 ^ 70 + 5941905845594411551712079861066501351950749375129466888826665397307648) * 10 ^ 70 + 5328773380074387546807866329410097423484643388471461582861690916013296)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_72 :
Polynomial.coeff recurrence4Scalar0Left 72 = (12522582316623892643730113979161041121333372944073147840898 * 10 ^ 70 + 1047344260966898382963541786723385113309823178907056778672847590825449) * 10 ^ 70 + 4335424796254724911469723440384560262503424971355590396249603202929339
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_73 :
Polynomial.coeff recurrence4Scalar0Left 73 = -((275424373492871105539597386546613844009001096102753634843418 * 10 ^ 70 + 5729207229439613740860653438332780144496126682794930045260109720781542) * 10 ^ 70 + 177400444904352621932880383502996934674674606207673948049071185738156)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_74 :
Polynomial.coeff recurrence4Scalar0Left 74 = (5637594451869060909688223330024894536150633233351187101347737 * 10 ^ 70 + 9583228739338470354642173050342904850804315406242249992005742550895448) * 10 ^ 70 + 1236984394595631163087328642992398035743677118422888111592400936937210