Recurrence 4 lookup certificate: Scalar0Main 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.recurrence4Scalar0Main_coeff_79 :
Polynomial.coeff recurrence4Scalar0Main 79 = (3640665295796527821224641803196295228258639398946479024117355717487 * 10 ^ 70 + 1887350205692043347602193083644860019943790401960069562698388311899232) * 10 ^ 70 + 8081969410725478205003544314396647846114696333408425921855031412227594
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_80 :
Polynomial.coeff recurrence4Scalar0Main 80 = -((189023606216219996296087485573774270345923648930511695515749279686735 * 10 ^ 70 + 2376719488175478449534714822080702698959958171752700799914909011960219) * 10 ^ 70 + 7280775591124164611404250481767345837051340913973638602212817689480936)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_81 :
Polynomial.coeff recurrence4Scalar0Main 81 = (5717165542713269845123885653633207701300223157250154255677568078207657 * 10 ^ 70 + 2118735750920037257222587891928797188631180509744436303038711740354132) * 10 ^ 70 + 1142674627758399985161117326784492318857806069797640094066910018372027
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_82 :
Polynomial.coeff recurrence4Scalar0Main 82 = -(((14 * 10 ^ 70 + 838144537466619346587787150037445396162957836526957751074501887270896) * 10 ^ 70 + 7423976817671601761833758251098409041800763523993183070613303296949105) * 10 ^ 70 + 4431279178362684034613769123628487158615829651434648878834694488207336)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_83 :
Polynomial.coeff recurrence4Scalar0Main 83 = ((305 * 10 ^ 70 + 2984574465798098005061242458535050690709780516711030733302233839394701) * 10 ^ 70 + 9998945498889341371128824994851686437946643680332631347288681743621553) * 10 ^ 70 + 9872355402240289302939117555761187843867945645287280414113341816401418
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_84 :
Polynomial.coeff recurrence4Scalar0Main 84 = -(((5988 * 10 ^ 70 + 701294016795557076486653889689770543740439850153036622483089820022783) * 10 ^ 70 + 1013847791666504003261457494567098518097636289465461808502033382930753) * 10 ^ 70 + 8185775910311807086488646399391002136890008263974943482072113386390347)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_85 :
Polynomial.coeff recurrence4Scalar0Main 85 = ((107278 * 10 ^ 70 + 6320895265178096721736315929675196011820896500579237619859430241210367) * 10 ^ 70 + 315418771343706158025374471609953070226635464974584538826373118802519) * 10 ^ 70 + 8009572667979457993107978913954066422654135106728049967537180433188123
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_86 :
Polynomial.coeff recurrence4Scalar0Main 86 = -(((1752015 * 10 ^ 70 + 7693440406506603686488141526046107321038737022186095730817919117750431) * 10 ^ 70 + 266437865337348171706679930533769340910837026222243522740961748875303) * 10 ^ 70 + 4665187663353277149501919621763634156458626444652291230228812162109609)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_87 :
Polynomial.coeff recurrence4Scalar0Main 87 = ((25690135 * 10 ^ 70 + 4388571417425585195560015858968519671557076598903153902072778813673720) * 10 ^ 70 + 1797681115700824469133625741087553973379297887064004748244384850415228) * 10 ^ 70 + 850054083812371056224819354797645561626254340510860677671631757214767
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_88 :
Polynomial.coeff recurrence4Scalar0Main 88 = -(((324260409 * 10 ^ 70 + 5498719799827570840984695750211962828475057430706483828668578998222602) * 10 ^ 70 + 8678339570695418168899585578352022036934345428666582568809916219321994) * 10 ^ 70 + 1781434191854073891008876933157385035418199800873865666851307752012694)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_89 :
Polynomial.coeff recurrence4Scalar0Main 89 = ((3079679891 * 10 ^ 70 + 9849836506561313602516589766811332756353207179510098825942812014113552) * 10 ^ 70 + 7547284713297819534218463713153559451449095828178236778697987016510870) * 10 ^ 70 + 6094497740525415921628787775854490726883367743610557605236903370828362
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_90 :
Polynomial.coeff recurrence4Scalar0Main 90 = -(((6849096723 * 10 ^ 70 + 8617875490052712808761430694307537653453669387629640155096402486008519) * 10 ^ 70 + 2786640031175580061948935982581647547934823432194609381828528762095015) * 10 ^ 70 + 8165207011349534579654213262764504243708003119049257473827979001016912)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_91 :
Polynomial.coeff recurrence4Scalar0Main 91 = -(((642101023234 * 10 ^ 70 + 2323800625463645522169313218208061983381647062408553812537477422180078) * 10 ^ 70 + 1846160276909449818409007234752864650127485115962118714072757697446491) * 10 ^ 70 + 331931257803259215359032896074823995370513157409143953283902810784448)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_92 :
Polynomial.coeff recurrence4Scalar0Main 92 = ((22246146548718 * 10 ^ 70 + 4575422451605088969722354379016473579848541404899738393965769173566987) * 10 ^ 70 + 6366428315627278360867860703944632278444431842006465631953633514390165) * 10 ^ 70 + 2648070212168889732822457886863023162887878955803084046382273220004725
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_93 :
Polynomial.coeff recurrence4Scalar0Main 93 = -(((527684291176305 * 10 ^ 70 + 335298406864992489037506917509449767189286803686629529144029952258180) * 10 ^ 70 + 4345976047249713396373330470662320935342813581055391501448619088949015) * 10 ^ 70 + 8187098462542525058547030047883772725262668356903511392687444046093447)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_94 :
Polynomial.coeff recurrence4Scalar0Main 94 = ((10626389944767773 * 10 ^ 70 + 2209096003110102267924304453512854475122973376224479819282865007931411) * 10 ^ 70 + 287978916018730741841020880562147705559592123295923142288990498735614) * 10 ^ 70 + 3455393119536955510926832201777832212550350733243938341936875944929553
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_95 :
Polynomial.coeff recurrence4Scalar0Main 95 = -(((193378096232968347 * 10 ^ 70 + 4617241749251885908474786521071839003438361567117087863247478604184421) * 10 ^ 70 + 148203595502747548505608082573627932893897802468788807581363203667704) * 10 ^ 70 + 7454616621299393024033644581970419070452585643765710215895136683764333)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_96 :
Polynomial.coeff recurrence4Scalar0Main 96 = ((3267846578554576414 * 10 ^ 70 + 5345174029815583946889333610658405753420452425191863814322128607519600) * 10 ^ 70 + 2975764278233740361486765297154834381871275673725723070589756636742090) * 10 ^ 70 + 7208867887480501316427435188495326926187309183125392814739876924329468
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_97 :
Polynomial.coeff recurrence4Scalar0Main 97 = -(((52030134821240555786 * 10 ^ 70 + 8506361499163761979596628598189027575095506863679711662902115596454830) * 10 ^ 70 + 5501840100710366374614393471138737617204708829900640585046412090124658) * 10 ^ 70 + 8520070237110914058091755286257881217234926181870542873250611201834295)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_98 :
Polynomial.coeff recurrence4Scalar0Main 98 = ((787407029466912706785 * 10 ^ 70 + 3697456334294324794440777315854331542921216662371525495842892635425817) * 10 ^ 70 + 7442610933779003303162333553936994229582499009361330674246240650183514) * 10 ^ 70 + 2752307039233217015641183025712784283985257854699873625275256978427347
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_99 :
Polynomial.coeff recurrence4Scalar0Main 99 = -(((11392210912737808016869 * 10 ^ 70 + 8373138659306802752738918548056126290300329652853776626369847536131589) * 10 ^ 70 + 1907177626263891113338956874275319467364796957582822565736886301235287) * 10 ^ 70 + 2999318994205816103833857506505800273911436802037350242015001404440875)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_100 :
Polynomial.coeff recurrence4Scalar0Main 100 = ((158215179608606498250322 * 10 ^ 70 + 9887248735836737257409915558691457765772910129211911032206810236467383) * 10 ^ 70 + 526776988246295161826675924565673104477427477678675905200762140452705) * 10 ^ 70 + 5152266999493287045946347773683554411869245759079679072997829583907668
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_101 :
Polynomial.coeff recurrence4Scalar0Main 101 = -(((2115559937381414365865889 * 10 ^ 70 + 4887846885832792986784050164218577031959656643676469183557972975001135) * 10 ^ 70 + 2104084946440503069058840593033147734501791597099744288342070706170927) * 10 ^ 70 + 7797344772182184029683124862495768626914686355576493108254588460247801)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_102 :
Polynomial.coeff recurrence4Scalar0Main 102 = ((27298792254493506209598691 * 10 ^ 70 + 2383967247300580052758883187987196359431048789869033290194175070349003) * 10 ^ 70 + 2159008947688610991639838004032987031164786369575527640929652640775041) * 10 ^ 70 + 8436232577304695381058284369624138887024570290841866722115365285118633
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_103 :
Polynomial.coeff recurrence4Scalar0Main 103 = -(((340564793520984298364350553 * 10 ^ 70 + 7146262466469102367108900671287781117979269384042349794736502846821829) * 10 ^ 70 + 7621200379241888037799465863340578042126398574372781314765955235391280) * 10 ^ 70 + 2984492826550102986747221902674222542401092105874250110052030966897121)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_104 :
Polynomial.coeff recurrence4Scalar0Main 104 = ((4113815941821813194697714924 * 10 ^ 70 + 1318556220053835324001280698566818696927190792684644322571369797566041) * 10 ^ 70 + 602043806082792085445613319367643622247277364965821434912555310047772) * 10 ^ 70 + 5523404913424955161507187184964155718580465130910250562369890317590642
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_105 :
Polynomial.coeff recurrence4Scalar0Main 105 = -(((48175008292779303173316219754 * 10 ^ 70 + 1748437547414548604200889540922144902773068213290147391328909145079080) * 10 ^ 70 + 3560093996834082617042798943422563062602541125607876111143974276510127) * 10 ^ 70 + 6846510113667766527786511816715199210237229315985068556241745936194166)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_106 :
Polynomial.coeff recurrence4Scalar0Main 106 = ((547510808127156934680658636972 * 10 ^ 70 + 8506557864451056623748517347089560420619325128778217424270834164901410) * 10 ^ 70 + 4038360536568904496680113562995529337761360645847453346775612620063347) * 10 ^ 70 + 8374210474846798186144947731691803392770157296425845876181252072283195
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_107 :
Polynomial.coeff recurrence4Scalar0Main 107 = -(((6044458017669642701055270918399 * 10 ^ 70 + 297324026913492323526781228912798301795878484088641854865186941154736) * 10 ^ 70 + 9733143916927197936051872742933665706054249159669152036626658818263515) * 10 ^ 70 + 6225627293287322815062616638880900508296451425869525336631802398692611)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_108 :
Polynomial.coeff recurrence4Scalar0Main 108 = ((64873400686784454711463442464291 * 10 ^ 70 + 2400003085338951633394440544448097108391730989711963283589429250698944) * 10 ^ 70 + 2283061794608452288521309565491347749679061011195476145617968925127699) * 10 ^ 70 + 914858306467878175620311649875048147922834234744837934868808148695836
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_109 :
Polynomial.coeff recurrence4Scalar0Main 109 = -(((677379902554120506280460330170470 * 10 ^ 70 + 9772619144763418588805042028071625361578800460313461374104020706486497) * 10 ^ 70 + 491545871678695677883660102537760828682279670761881582409260084170175) * 10 ^ 70 + 860708316655478720417912698498154381124544312809479729403974054657914)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_110 :
Polynomial.coeff recurrence4Scalar0Main 110 = ((6885479727549983003564084836459653 * 10 ^ 70 + 5937946825366033006580433126430847060130394795154262104396258908086327) * 10 ^ 70 + 4852066660524336249373995533975086723611535324603325580821919726266342) * 10 ^ 70 + 8931038169876847492619223563905288899655737250701473955978483965536106
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_111 :
Polynomial.coeff recurrence4Scalar0Main 111 = -(((68175142742470849405125796284522631 * 10 ^ 70 + 8926396286191662296959556270695720533632729531436357491950530298342248) * 10 ^ 70 + 8834633194854351515927868818246095842977027503337395024248470210902234) * 10 ^ 70 + 9305914904573581160031220266131599585239389207041410954975614627886572)