Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupC3Low

Recurrence 2 lookup certificate: C3 source coefficients, low half #

This is a checked coefficient-lookup shard for the second pseudo-division recurrence in the order-seven certificate.

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_0 :
Polynomial.coeff remainder4Coefficient3 0 = -7616
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_1 :
Polynomial.coeff remainder4Coefficient3 1 = 23629396
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_2 :
Polynomial.coeff remainder4Coefficient3 2 = 58932891758
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_3 :
Polynomial.coeff remainder4Coefficient3 3 = -101789216513848
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_4 :
Polynomial.coeff remainder4Coefficient3 4 = 24905087386651268
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_5 :
Polynomial.coeff remainder4Coefficient3 5 = 2001081781821722943
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_6 :
Polynomial.coeff remainder4Coefficient3 6 = -667056002337536511217
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_7 :
Polynomial.coeff remainder4Coefficient3 7 = -77234185748797243479815
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_8 :
Polynomial.coeff remainder4Coefficient3 8 = 64020759979726943306282040
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_9 :
Polynomial.coeff remainder4Coefficient3 9 = -25288748029848523739897038488
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_10 :
Polynomial.coeff remainder4Coefficient3 10 = 7300343282146366199862564940260
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_11 :
Polynomial.coeff remainder4Coefficient3 11 = -1604983998422124665226856786580890
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_12 :
Polynomial.coeff remainder4Coefficient3 12 = 280063413607009459944662920136899040
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_13 :
Polynomial.coeff remainder4Coefficient3 13 = -39836705852626321198484094015320186719
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_14 :
Polynomial.coeff remainder4Coefficient3 14 = 4705699001915517302227575987346835340291
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_15 :
Polynomial.coeff remainder4Coefficient3 15 = -468462320210055742493123276582195904343317
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_16 :
Polynomial.coeff remainder4Coefficient3 16 = 39783714118134389111331084075750880162985953
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_17 :
Polynomial.coeff remainder4Coefficient3 17 = -2911841972879974303016806756728570199616202077
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_18 :
Polynomial.coeff remainder4Coefficient3 18 = 185314130585738044570745419712469338945444236050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_19 :
Polynomial.coeff remainder4Coefficient3 19 = -10334918482420387545971834870050575452476132688008
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_20 :
Polynomial.coeff remainder4Coefficient3 20 = 508591730138059299965846106018491097105069144624610
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_21 :
Polynomial.coeff remainder4Coefficient3 21 = -22222586450892042949714855548866906170527911350885778
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_22 :
Polynomial.coeff remainder4Coefficient3 22 = 867013210352089439619037112221710776892657448685279619
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_23 :
Polynomial.coeff remainder4Coefficient3 23 = -30358970081220483053746604020669295849210977010557373990
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_24 :
Polynomial.coeff remainder4Coefficient3 24 = 958549932918181534168698458367991162511273384123683668925
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_25 :
Polynomial.coeff remainder4Coefficient3 25 = -27408224837271437607113020452955629138896453848291157807357
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_26 :
Polynomial.coeff remainder4Coefficient3 26 = 712546452039532100343877008622930485719273277740471821354561
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_27 :
Polynomial.coeff remainder4Coefficient3 27 = -16904840327259068167910287415613687228127951366770675663137123
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_28 :
Polynomial.coeff remainder4Coefficient3 28 = 367248148725530123287379405094893962092224422107284683991055190
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_29 :
Polynomial.coeff remainder4Coefficient3 29 = -7328936256050768257442442385040526539912647330781583192183234343
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_30 :
Polynomial.coeff remainder4Coefficient3 30 = 134754790433530815027688277849096376546478491198475048344833764475
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_31 :
Polynomial.coeff remainder4Coefficient3 31 = -2289149482085260253403876502309858107748901235349124368436987881648
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_32 :
Polynomial.coeff remainder4Coefficient3 32 = 36021229464291217989389134979735591213549505133352803754096776485647
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_33 :
Polynomial.coeff remainder4Coefficient3 33 = -526325834255430488728353153076527252153101129986627852491429014375454
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_34 :
Polynomial.coeff remainder4Coefficient3 34 = 7157400131119243975030359253826818341912189462149261973259840327566624
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_35 :
Polynomial.coeff remainder4Coefficient3 35 = -(9 * 10 ^ 70 + 780693227907727741706804856687061065684925243940551419908147830810647)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_36 :
Polynomial.coeff remainder4Coefficient3 36 = 107 * 10 ^ 70 + 6087137600442387103020668378959092243060557998844135318561096240782175
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_37 :
Polynomial.coeff remainder4Coefficient3 37 = -(1194 * 10 ^ 70 + 3851926644693827928561150135540377093440353256382488385316957806029989)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_38 :
Polynomial.coeff remainder4Coefficient3 38 = 12435 * 10 ^ 70 + 5353316209464298652411339259684633616148416377578518477590756372369666
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_39 :
Polynomial.coeff remainder4Coefficient3 39 = -(121658 * 10 ^ 70 + 8981461377356276118894252080253034951418050688051876615714839546903304)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_40 :
Polynomial.coeff remainder4Coefficient3 40 = 1120154 * 10 ^ 70 + 5700006657874512750042443660160551344288227222878660602085264462141303
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_41 :
Polynomial.coeff remainder4Coefficient3 41 = -(9721291 * 10 ^ 70 + 7874385236989461213995153192849912266323621442347552791987033814011373)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_42 :
Polynomial.coeff remainder4Coefficient3 42 = 79634932 * 10 ^ 70 + 8812669157617274692546069445170591879432976287010545566441611160454230
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_43 :
Polynomial.coeff remainder4Coefficient3 43 = -(616602437 * 10 ^ 70 + 2971021994548258522205209363837801466519201862219578863345484230057377)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_44 :
Polynomial.coeff remainder4Coefficient3 44 = 4518413712 * 10 ^ 70 + 1782037323462868241125242081914160804237194876588248734113168526624428
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_45 :
Polynomial.coeff remainder4Coefficient3 45 = -(31374279953 * 10 ^ 70 + 3398932986127055903753407290844111818219232994146154981264266312084289)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_46 :
Polynomial.coeff remainder4Coefficient3 46 = 206665955018 * 10 ^ 70 + 9853123910196592861971301502374650733395637270963552577659336064834752
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_47 :
Polynomial.coeff remainder4Coefficient3 47 = -(1292843691442 * 10 ^ 70 + 3443747586447538365589461029069585544298145161513284882836310635406040)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_48 :
Polynomial.coeff remainder4Coefficient3 48 = 7688739840799 * 10 ^ 70 + 4062450600520925749578666725908320006586536194710238267178603437126487
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_49 :
Polynomial.coeff remainder4Coefficient3 49 = -(43513455148816 * 10 ^ 70 + 138808008960436624962849771065693365379653972588730664017346990750967)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_50 :
Polynomial.coeff remainder4Coefficient3 50 = 234561512742118 * 10 ^ 70 + 7797357872467025137267397853104724282502673068013864112946545200812482
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_51 :
Polynomial.coeff remainder4Coefficient3 51 = -(1205423822336854 * 10 ^ 70 + 3688341955214657759705056771932106625902570291914474503900926639874603)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_52 :
Polynomial.coeff remainder4Coefficient3 52 = 5910691684737118 * 10 ^ 70 + 1490537238395383521573549331045772415807717606142427311272445541711955
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_53 :
Polynomial.coeff remainder4Coefficient3 53 = -(27675770395183778 * 10 ^ 70 + 3417625360114089375915156499542446039001454108000008832128672540437435)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_54 :
Polynomial.coeff remainder4Coefficient3 54 = 123838017802424772 * 10 ^ 70 + 2285128813620963137533327495660058940106978905370184931473429801454087
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_55 :
Polynomial.coeff remainder4Coefficient3 55 = -(529925266289348895 * 10 ^ 70 + 3182188329646959484967787993984372253939286647903329211287559533338841)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_56 :
Polynomial.coeff remainder4Coefficient3 56 = 2170098630242407913 * 10 ^ 70 + 7294415269457435219252305979344240371389484534184419706849732858757275
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_57 :
Polynomial.coeff remainder4Coefficient3 57 = -(8510038022267733582 * 10 ^ 70 + 6487345205969852514902265145721357265400467885648246742563974307760266)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_58 :
Polynomial.coeff remainder4Coefficient3 58 = 31977132843479892915 * 10 ^ 70 + 7198707630552023701634044314024800333800286926291578203891849610886569
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_59 :
Polynomial.coeff remainder4Coefficient3 59 = -(115201692446233855399 * 10 ^ 70 + 1690070432355271286941235790070175854008216454197867367866776431540214)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_60 :
Polynomial.coeff remainder4Coefficient3 60 = 398136487191221237606 * 10 ^ 70 + 6248891098841594697251302002750330752116229148176061210136909063789274
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_61 :
Polynomial.coeff remainder4Coefficient3 61 = -(1320654071156342915753 * 10 ^ 70 + 2377930498554300320615213173474873462479074392759662961033464828791656)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_62 :
Polynomial.coeff remainder4Coefficient3 62 = 4206768424231584262923 * 10 ^ 70 + 9608450429898959935770937424979281004994028722787094532067595877950555
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_63 :
Polynomial.coeff remainder4Coefficient3 63 = -(12874127932169583448986 * 10 ^ 70 + 8229589983169199308679175431201465069901293581379721389509758176396370)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_64 :
Polynomial.coeff remainder4Coefficient3 64 = 37869818901217598590214 * 10 ^ 70 + 2684189650113752618990603588130000367168724536285271053293315781893240
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_65 :
Polynomial.coeff remainder4Coefficient3 65 = -(107117652372300457653530 * 10 ^ 70 + 2820438646931477662914417804416016743264598496496376644293653595881791)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_66 :
Polynomial.coeff remainder4Coefficient3 66 = 291472520655757624173293 * 10 ^ 70 + 9318407221502233772779373922960807076604420762370008498635745436062436
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_67 :
Polynomial.coeff remainder4Coefficient3 67 = -(763255251261824813446920 * 10 ^ 70 + 663392015126849047088005903228127894112915849723930040310267243534773)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_68 :
Polynomial.coeff remainder4Coefficient3 68 = 1924134123708768457970621 * 10 ^ 70 + 3858766004763946451059514069998257159151086156477369369904758035586916
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_69 :
Polynomial.coeff remainder4Coefficient3 69 = -(4671358596863882506937197 * 10 ^ 70 + 4607530141062994742416789604742585907951309682530483772473407079150256)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_70 :
Polynomial.coeff remainder4Coefficient3 70 = 10925313582757997447119037 * 10 ^ 70 + 1203173760456059708058576033981709342934246155642205223674264748246070
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_71 :
Polynomial.coeff remainder4Coefficient3 71 = -(24622934642878660593157367 * 10 ^ 70 + 3357171702151507033194275056968014187668490157672808431725030659478844)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_72 :
Polynomial.coeff remainder4Coefficient3 72 = 53491576224476315570591120 * 10 ^ 70 + 7616078311043927508073497568813104240899397053739775261472170319418578
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_73 :
Polynomial.coeff remainder4Coefficient3 73 = -(112043723397455956258232126 * 10 ^ 70 + 7733157513605233991939355882333685459730009074923019445965198858005588)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_74 :
Polynomial.coeff remainder4Coefficient3 74 = 226337091364494966347794659 * 10 ^ 70 + 1502277746545911310307221472340018277559597428174046746526451661084661
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_75 :
Polynomial.coeff remainder4Coefficient3 75 = -(441054601901686700619299692 * 10 ^ 70 + 1724347500140079239516180910028795188100506364583632783297769581582843)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_76 :
Polynomial.coeff remainder4Coefficient3 76 = 829264093409921641203331198 * 10 ^ 70 + 2631361253669475146952727960264173445943913949256711140820590999958711
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_77 :
Polynomial.coeff remainder4Coefficient3 77 = -(1504686293150239720538056545 * 10 ^ 70 + 673279847508665206965539321043334579609782446054165238406422987935828)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_78 :
Polynomial.coeff remainder4Coefficient3 78 = 2635323034131858622864248028 * 10 ^ 70 + 1160865291812191698700183030407192593425287303006320852572963120867419
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_79 :
Polynomial.coeff remainder4Coefficient3 79 = -(4455868535293460241289148536 * 10 ^ 70 + 9056962650126648688109729548551190686680552259888223124808147527714126)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_80 :
Polynomial.coeff remainder4Coefficient3 80 = 7274633662313967423976710516 * 10 ^ 70 + 6516859814540005554852213480715214336394056292484245374552224658963018
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_81 :
Polynomial.coeff remainder4Coefficient3 81 = -(11469215614884445157030799907 * 10 ^ 70 + 5071724930974058515006252029554182229322469277554972107165099342701197)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_82 :
Polynomial.coeff remainder4Coefficient3 82 = 17464566618595354816947065542 * 10 ^ 70 + 389043829981722676166583905580549629734913501976491534271568877345444
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_83 :
Polynomial.coeff remainder4Coefficient3 83 = -(25688297043961157740869759420 * 10 ^ 70 + 1837509490473555219552360296395708279183349155109405322342660980891147)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_84 :
Polynomial.coeff remainder4Coefficient3 84 = 36501647278996069549443593797 * 10 ^ 70 + 9459564800358228253967084647499925554901632789004196578234884521360594
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_85 :
Polynomial.coeff remainder4Coefficient3 85 = -(50110641123168082716766158500 * 10 ^ 70 + 9014461038714557812331053718913445477112391705587955989794091414765793)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_86 :
Polynomial.coeff remainder4Coefficient3 86 = 66469598171426207587588527273 * 10 ^ 70 + 5553047847158229315562194407793096608740892655211345026805121398781099
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_87 :
Polynomial.coeff remainder4Coefficient3 87 = -(85196479599277902758016711398 * 10 ^ 70 + 8640214830215079889260459041437774369742629957332327091327787831340584)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_88 :
Polynomial.coeff remainder4Coefficient3 88 = 105523791107890834557777531798 * 10 ^ 70 + 9703648770617045396882137448897179689092220569267028088911957491445320
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_89 :
Polynomial.coeff remainder4Coefficient3 89 = -(126307374817510221291726220219 * 10 ^ 70 + 9909324262182354980719504978326965469372748881127582823873908530577747)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_90 :
Polynomial.coeff remainder4Coefficient3 90 = 146106973995793965173726715424 * 10 ^ 70 + 4778894440889510909997659030272716539324801399583469113074395479516212
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C3_coeff_91 :
Polynomial.coeff remainder4Coefficient3 91 = -(163337672718356691756719939335 * 10 ^ 70 + 9265976049075004945941217714524057724774255021178445864100388080550674)