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_319 :
Polynomial.coeff recurrence4Scalar0Left 319 = (((44901604054193222049 * 10 ^ 70 + 7198499961702983857020114316562483983751339912941861932416397943403199) * 10 ^ 70 + 9809122012744941271169154886183553957517743752379284881334176880414566) * 10 ^ 70 + 3093715988816277902313614201988172404021445289034119263779908140440909) * 10 ^ 70 + 5252504683495969722690520630123349948761303699322213212509035298063557
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_320 :
Polynomial.coeff recurrence4Scalar0Left 320 = -((((24170949961983710526 * 10 ^ 70 + 5011020768287742449432931485191693374355945738358782369307597668109809) * 10 ^ 70 + 3127170073249260198757445235788587377946731569153393043225048774401476) * 10 ^ 70 + 1477102173183319338550459897526473931327996831839355788045862362950900) * 10 ^ 70 + 8106492504251377079082749843777618462409064427778748309189529799694716)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_321 :
Polynomial.coeff recurrence4Scalar0Left 321 = (((12569831636944203093 * 10 ^ 70 + 6807029919647262813411124038860856537698534212153738118311659263327972) * 10 ^ 70 + 6471198791511277952981610446127036442958920021796578855205634618760085) * 10 ^ 70 + 8444219727426140553980438530266838805913082972178457923905499275349218) * 10 ^ 70 + 6455191516875216193495218227944180102672687261255295988200993977483281
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_322 :
Polynomial.coeff recurrence4Scalar0Left 322 = -((((6287743511366963394 * 10 ^ 70 + 3385443163850702118589886864746903155524893797320628498922063018870918) * 10 ^ 70 + 3806489591033005495527859132434921619241118998024774032504870831035456) * 10 ^ 70 + 3253340088418775207938481742821651839471816202801648013685112669288253) * 10 ^ 70 + 3734327375704762759172794222555965392260059278849731182497420402598845)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_323 :
Polynomial.coeff recurrence4Scalar0Left 323 = (((3002122077363566228 * 10 ^ 70 + 4896826059104912978365373539918480143928516934969934592258556761988133) * 10 ^ 70 + 888651751149076535235658665834304840620500705658570277524538522308335) * 10 ^ 70 + 7761634250351829266645043916188564766177051845228041772408455869679528) * 10 ^ 70 + 4074400968865432363883100374969076465166575456280485347728081701919986
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_324 :
Polynomial.coeff recurrence4Scalar0Left 324 = -((((1348913959626982944 * 10 ^ 70 + 737055833761907341684247514014240972350883093845361958288454045586299) * 10 ^ 70 + 8077277734713931854036126745548065971897599055146192128450285507648445) * 10 ^ 70 + 8840462724590508674351677090799622292560063843759051044373963656436466) * 10 ^ 70 + 3307319950120082473105638257114415340648009340080538869865641612766926)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_325 :
Polynomial.coeff recurrence4Scalar0Left 325 = (((554380381465020753 * 10 ^ 70 + 1532846897064529475437667999145300763470566639532369829478437516276168) * 10 ^ 70 + 9815416324686333104464494761152958944155310116603213579250513121143855) * 10 ^ 70 + 6978907501356574981534300391362229300828135351310915863304541814792036) * 10 ^ 70 + 8976175560175845828352556596524931076761697317235881808320938310329391
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_326 :
Polynomial.coeff recurrence4Scalar0Left 326 = -((((194407264180134043 * 10 ^ 70 + 4359832607843018009065435876703624656061076457437494551750375385811616) * 10 ^ 70 + 7177819356584887719896812352447396972622741746519067954447663332373422) * 10 ^ 70 + 8868762305974053862737793135249424583317251624304527065516924216706383) * 10 ^ 70 + 2665547445718285610392314812754537792941414027526792618157734494679820)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_327 :
Polynomial.coeff recurrence4Scalar0Left 327 = (((44617243512810394 * 10 ^ 70 + 6649332003986563358001232113733218085922110580025372424256895816096937) * 10 ^ 70 + 9849521340678688481276497462554952637106912045872982149139048575271838) * 10 ^ 70 + 9472089015604338786357168653627544868410597567620112409892977047033501) * 10 ^ 70 + 5738413590918075142846174722215252990347994058646271777473306507393092
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_328 :
Polynomial.coeff recurrence4Scalar0Left 328 = (((9194787032639301 * 10 ^ 70 + 2033356689216206312723289103082417421051960308182637483996056037706678) * 10 ^ 70 + 8572509945359899114562724198093294455255646388510399587538778744469370) * 10 ^ 70 + 5761547109082033126587581788673149089395617655759450850320968383055175) * 10 ^ 70 + 7284650128975752661905954176341422460458263533125033205749226408985218
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_329 :
Polynomial.coeff recurrence4Scalar0Left 329 = -((((22608633224951657 * 10 ^ 70 + 9312267408684962971416601050583990437369428919328896630381264716675371) * 10 ^ 70 + 6831635872892288412171070344544038132322760926731331491514398711425774) * 10 ^ 70 + 4585063908765813078123405494480060549814559629819094502074687277929799) * 10 ^ 70 + 381808514025224777813480449904941635852853776042925260353867922676141)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_330 :
Polynomial.coeff recurrence4Scalar0Left 330 = (((21194825908364070 * 10 ^ 70 + 7260590360102543372721416747612703415981903643126629890731986320256939) * 10 ^ 70 + 3454058540649349110148761575935030514703414568615204835163862236883070) * 10 ^ 70 + 3557269304095087085493750101184962123561091973245611862695060836821836) * 10 ^ 70 + 1325660348452850701656612899370196973331090707621842590108228678738059
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_331 :
Polynomial.coeff recurrence4Scalar0Left 331 = -((((15831236289491772 * 10 ^ 70 + 6475579609625318304682753814011808932366344467286191472167278814689752) * 10 ^ 70 + 9149837404278009039618681100970040961806380402723147419030548201648357) * 10 ^ 70 + 7512666546439917669650514982988422777770664201125823783968605930813575) * 10 ^ 70 + 8775681601715619983734416443613909040740437549804220685041022226389024)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_332 :
Polynomial.coeff recurrence4Scalar0Left 332 = (((10587712520144674 * 10 ^ 70 + 9407657958446679131740995943689486291816420634162329650438674657244344) * 10 ^ 70 + 8756545000208565937600759414616800839856527634924671764188530723368249) * 10 ^ 70 + 6235206403341600904763024440665449798022392512324533293610131054153569) * 10 ^ 70 + 6549332170790150749617189132295602351841929900646649872847815657853030
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_333 :
Polynomial.coeff recurrence4Scalar0Left 333 = -((((6609165774858349 * 10 ^ 70 + 1855250113265282282747938024181180491250502679459175910543926805553276) * 10 ^ 70 + 6804583647216778808499621326162993849944479633253189342067168637118936) * 10 ^ 70 + 3521497290809016349525551982493668442699614862389515913263286289109946) * 10 ^ 70 + 4471377006556271190779952480440690053124003576298255663127914480565549)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_334 :
Polynomial.coeff recurrence4Scalar0Left 334 = (((3927154956380052 * 10 ^ 70 + 6402448482987200543191454713590274027824820735670013781901790569202609) * 10 ^ 70 + 6727904769348355229134139432746925737001646709070912654842619162965324) * 10 ^ 70 + 174270397755234125865328078488643264811618451104657079722633574090726) * 10 ^ 70 + 1327334040329948631069207373595536707337363402629270192487288394160704
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_335 :
Polynomial.coeff recurrence4Scalar0Left 335 = -((((2245406832710003 * 10 ^ 70 + 4211061426008746971436860743258361652919950504896544616376872887524684) * 10 ^ 70 + 4407087167756503591154920271509272151386894844787255676662363417616211) * 10 ^ 70 + 9945289555376602848429314976557646920399385047028996546457609378319703) * 10 ^ 70 + 9913194645240222592466111756249514633484042975220854310422182061644504)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_336 :
Polynomial.coeff recurrence4Scalar0Left 336 = (((1243507338315788 * 10 ^ 70 + 7632730229118315023536387343111325935980374496076518487412213272701811) * 10 ^ 70 + 1249104926879734306025809294887664565256454428510953685897061836337184) * 10 ^ 70 + 6359353982446791759647401165677991738750047653869743653269559174107391) * 10 ^ 70 + 1038358234996936852911257328006959060939050523438390083525174433793442
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_337 :
Polynomial.coeff recurrence4Scalar0Left 337 = -((((669858286282407 * 10 ^ 70 + 4552494608917341954389310989104358416486122053378761460432841434552305) * 10 ^ 70 + 6912857292949471726214908810160435020003751911511994341600344921500991) * 10 ^ 70 + 1145502078678942325086008090377526721702258217717976112059488188895718) * 10 ^ 70 + 4312350191362523871703158588593430843251495235201066359471168438968895)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_338 :
Polynomial.coeff recurrence4Scalar0Left 338 = (((352002990834944 * 10 ^ 70 + 8763453302877835908905787847175504396068275187191371606974182128036842) * 10 ^ 70 + 7816346694623291199599129752358523918547104676155264829959122110292998) * 10 ^ 70 + 681842994194906392246417265170850701811746984718851680135129495340277) * 10 ^ 70 + 9849250585819097073479566305335451622040942278192410491167482139304899
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_339 :
Polynomial.coeff recurrence4Scalar0Left 339 = -((((180803385631632 * 10 ^ 70 + 8241191598746332297312104564419367086627018417631299446857457635764068) * 10 ^ 70 + 9682576402637785949057252129022267993070808844893533427324914670646529) * 10 ^ 70 + 1339299911857906610923840083430912674681908120876968970249316922103388) * 10 ^ 70 + 572292069660256671999696804452612756204633094536833493895185303489944)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_340 :
Polynomial.coeff recurrence4Scalar0Left 340 = (((90902680022524 * 10 ^ 70 + 3649348746978160267953387211318516723544002454576124679482694538199830) * 10 ^ 70 + 3878308806293439489591616903673473798885025705404719867756955095017877) * 10 ^ 70 + 6129798526128434688398966019850566832145606284302879915968333130415641) * 10 ^ 70 + 6732584828673257186560176522577869624689544292608715365541196821859640
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_341 :
Polynomial.coeff recurrence4Scalar0Left 341 = -((((44780686863156 * 10 ^ 70 + 8550314848222192544648199324309756923012040101427339684490365843179032) * 10 ^ 70 + 704693610553392287241120460842080581390303849980609960776166127212300) * 10 ^ 70 + 1970961365248193656804793653500852995895195159855155292285683586574293) * 10 ^ 70 + 4845728742818010610336603692633233993379404283810383561460905468230653)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_342 :
Polynomial.coeff recurrence4Scalar0Left 342 = (((21629756929370 * 10 ^ 70 + 9284421374341042193539851937058722876375492302391543909478946693911391) * 10 ^ 70 + 9880288404508210035028809414662710451618815654254120570879038088736842) * 10 ^ 70 + 7481522294769375082504158778395932844332081718923430974815403884180163) * 10 ^ 70 + 5852926044970287934617985867897738695815002565853280496619016226933554
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_343 :
Polynomial.coeff recurrence4Scalar0Left 343 = -((((10248557028154 * 10 ^ 70 + 1253369360465461411421558000021378374880882706033815686195278377852143) * 10 ^ 70 + 5377514596394350385124235218565158835393132286497800441135870117140555) * 10 ^ 70 + 3134220848492503972205201158116128111050364261872212950260751835244225) * 10 ^ 70 + 7474967108533851054427731240546710835934238828664535700396226248802199)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_344 :
Polynomial.coeff recurrence4Scalar0Left 344 = (((4764850974428 * 10 ^ 70 + 3116492940680290056755316856875059727903103049791873928980223083260831) * 10 ^ 70 + 1373755526358285646713393834121892563593822315879256074751029693121011) * 10 ^ 70 + 9400085312366835742920105118574641923682357455701590096470783239466284) * 10 ^ 70 + 3797185031816458078699608287509932265356624121227758421232508616594154