Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupLeadingSquarePart0.Coefficients163To189

Recurrence 4 lookup certificate: LeadingSquare 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.recurrence4LeadingSquare_coeff_163 :

Polynomial.coeff recurrence4LeadingSquare 163 = (837318115446979635495087694903284866101427140478437938463293417537 * 10 ^ 70 + 2712858652617545113402551206760491108443038654489997639747755827677143) * 10 ^ 70 + 6167806090240560858299282513939504919804964531592790073412518566328190

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_164 :

Polynomial.coeff recurrence4LeadingSquare 164 = -((827605214713464825219866873697743967097915724868492662002340922419 * 10 ^ 70 + 6592097480285415548893601645100117393217943132237794333578769586145835) * 10 ^ 70 + 5827346839643299711989434168934988016398276380936740703796002986198819)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_165 :

Polynomial.coeff recurrence4LeadingSquare 165 = (761776395750897860001676882701927981774909967221639014797457011014 * 10 ^ 70 + 8197688070159743007640686975850722281612998495843481784853268571405582) * 10 ^ 70 + 9200629076069655035045712423752922299161705140176971950981110779325986

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_166 :

Polynomial.coeff recurrence4LeadingSquare 166 = -((655001459518548318380337527108124069506388780212302546174053126637 * 10 ^ 70 + 2033493412034869329046767160396898170359839458220235669237265778928487) * 10 ^ 70 + 990724237116850289130006510846164371667270343223991895445106089932607)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_167 :

Polynomial.coeff recurrence4LeadingSquare 167 = (524224977263957768957460841823558454489630417630360968767528156878 * 10 ^ 70 + 57459879090861845110785187139172651213693435546200677823586905261657) * 10 ^ 70 + 4197850333885647022929090825816669106875160900162014331207827640548218

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_168 :

Polynomial.coeff recurrence4LeadingSquare 168 = -((385830243214283869097874490813317374360436565447461371267921207637 * 10 ^ 70 + 4267158747196068785727681183062183804999481806058965226505129669262741) * 10 ^ 70 + 1992063223744970347339282156152238003521965313560949459664835940583435)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_169 :

Polynomial.coeff recurrence4LeadingSquare 169 = (253747114393593449536030776044437150893574118724292180234876556467 * 10 ^ 70 + 7752527768760132640662682663809575446250760174502647867634132191315506) * 10 ^ 70 + 627275818872975751136043523459920058646363903898996587371001343372760

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_170 :

Polynomial.coeff recurrence4LeadingSquare 170 = -((138235003035896504637634421387034539552754981749327691077872196979 * 10 ^ 70 + 3162843225189385776035310908316682188518301961431271675181262020307734) * 10 ^ 70 + 8452741673921032958238765868759081660195691776636215770608770979099137)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_171 :

Polynomial.coeff recurrence4LeadingSquare 171 = (45414444956533158455779373736567845608226336209056793012278886942 * 10 ^ 70 + 9632146029959315114680679517444604917678977877426118513304142852704316) * 10 ^ 70 + 5227861124245574758038502023845617505954395542301272023543523739028134

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_172 :

Polynomial.coeff recurrence4LeadingSquare 172 = (22525141907092053402660785404837884414702147497527944229781793785 * 10 ^ 70 + 2781251723554891782971941667065372558159640463091428321097514245344798) * 10 ^ 70 + 5088502037912418898041588740546418888968234756701526725671330262005091

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_173 :

Polynomial.coeff recurrence4LeadingSquare 173 = -((66618530425766791120096630457718427015145937217432369863819838718 * 10 ^ 70 + 568300084663008477477473782740142429702956664141804932507035729263011) * 10 ^ 70 + 8287016987060671877834712397837658609497092728773177944333754258094820)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_174 :

Polynomial.coeff recurrence4LeadingSquare 174 = (90144666026527989555547934906854821629906272996804774247712167623 * 10 ^ 70 + 7377597772058183663756238623445306127050336719688241354398404899590317) * 10 ^ 70 + 9416248525240046521788102760107513287662533128250054818554445442139610

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_175 :

Polynomial.coeff recurrence4LeadingSquare 175 = -((97594312156446209732460989547409350471316446003993429131655522930 * 10 ^ 70 + 8981142330140553183985689988790996516192936106800456577968528967899750) * 10 ^ 70 + 3422688766371698016709815840315038351680222914821601431695642674504620)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_176 :

Polynomial.coeff recurrence4LeadingSquare 176 = (93759782940891402868351736704197845356217844441083034948706090488 * 10 ^ 70 + 8051900139711289180750271005753135322628529208618899162247437208663651) * 10 ^ 70 + 8031567490954005926602621140571084329282287679205930833728927155261302

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_177 :

Polynomial.coeff recurrence4LeadingSquare 177 = -((83053442329299933801673203942571470787989281113116832495944316625 * 10 ^ 70 + 8334350170688637862291087110891419166067341792611353068167534880874709) * 10 ^ 70 + 8835811249583853969454141105501540267518695912076035997721606793564330)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_178 :

Polynomial.coeff recurrence4LeadingSquare 178 = (69092074754004621748465050817926119887220607789414352059075923005 * 10 ^ 70 + 2368994417668275352121844554854229628161654927558325266482513165496862) * 10 ^ 70 + 7635385671048378620263788784989540224792898139681290424382888503457227

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_179 :

Polynomial.coeff recurrence4LeadingSquare 179 = -((54527662505134348048755481403345343475135112273963252246306297071 * 10 ^ 70 + 5867139428658354816568186691845009164464602107855429120716645338990863) * 10 ^ 70 + 841060017061043969902944023637287700582006812569890751776800048224854)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_180 :

Polynomial.coeff recurrence4LeadingSquare 180 = (41069334904829665223429420691885354147690383822646332439204146434 * 10 ^ 70 + 1274583547075494602820521096612911775918549939854693055255903553532871) * 10 ^ 70 + 7974908353985676960792199046252432258208517452186321151587928736623548

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_181 :

Polynomial.coeff recurrence4LeadingSquare 181 = -((29627179825165827780785859958084825598820914877394685035577634931 * 10 ^ 70 + 1141340996096814057190369508276311840812290425131973919232863150188079) * 10 ^ 70 + 203531675740674464201093523288140401920010244632339135525187422967060)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_182 :

Polynomial.coeff recurrence4LeadingSquare 182 = (20512082050075401465402704132563630919865096411408404633327304953 * 10 ^ 70 + 5894315194534747975228346261928155999066676801706866216765034148423815) * 10 ^ 70 + 2754633670650918571360208115167007003605698661644078046836031472048544

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_183 :

Polynomial.coeff recurrence4LeadingSquare 183 = -((13640151924655458478605124992121883098498735849394152004177450278 * 10 ^ 70 + 1108969284404221450689836428488261314845148372916771293560357675034849) * 10 ^ 70 + 4384541785221592780803345029984723074298410898124611286738801400584026)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_184 :

Polynomial.coeff recurrence4LeadingSquare 184 = (8708899677694449368390884871933188124987861981658393337181060605 * 10 ^ 70 + 671706148296579093767836037980950247935637062337371194964556646093085) * 10 ^ 70 + 2026697372434093491869433423960042365947375907117122480119527763686449

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_185 :

Polynomial.coeff recurrence4LeadingSquare 185 = -((5329857611244955750094269894261024700221815681923578375374932014 * 10 ^ 70 + 2445288203463178085755156069027111210561443759377683743548472495428993) * 10 ^ 70 + 1946982518501859720299883256776095169405118614131255081120456674979630)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_186 :

Polynomial.coeff recurrence4LeadingSquare 186 = (3115781803338343378749910981530944617448471166692068149122411109 * 10 ^ 70 + 5542822601127559208601321230759416156987576400403077751850073233040472) * 10 ^ 70 + 2672809582429015881171832469266087244673885081700007448448922546660769

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_187 :

Polynomial.coeff recurrence4LeadingSquare 187 = -((1728864879779653182642533572085641520282383296963250946203179442 * 10 ^ 70 + 1196052238766766462240552552642168425120683034872981813696319288138777) * 10 ^ 70 + 6185499813309192304744914537940610880819968339474682645488020591615410)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_188 :

Polynomial.coeff recurrence4LeadingSquare 188 = (900039877845548416690007908005419183714681244503497258028229643 * 10 ^ 70 + 1163526285230190291330789993758878015690936697130327572284210549262924) * 10 ^ 70 + 6721404678688055428925964799154507652240406217152833519762210848584983

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_189 :

Polynomial.coeff recurrence4LeadingSquare 189 = -((429712233199633839991567293363439365139532470445696674062340781 * 10 ^ 70 + 1266080421415402396014443132396550435974585103110738532959311604829995) * 10 ^ 70 + 5488963517010354888201163563854527455213849092513384386559782951416072)