Recurrence 5 lookup certificate: A3Square coefficient convolution #
This is a checked coefficient-lookup shard for the fifth pseudo-division recurrence in the order-seven certificate.
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_171 :
Polynomial.coeff recurrence5A3Square 171 = (45414444956533158455779373736567845608226336209056793012278886942 * 10 ^ 70 + 9632146029959315114680679517444604917678977877426118513304142852704316) * 10 ^ 70 + 5227861124245574758038502023845617505954395542301272023543523739028134
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_172 :
Polynomial.coeff recurrence5A3Square 172 = (22525141907092053402660785404837884414702147497527944229781793785 * 10 ^ 70 + 2781251723554891782971941667065372558159640463091428321097514245344798) * 10 ^ 70 + 5088502037912418898041588740546418888968234756701526725671330262005091
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_173 :
Polynomial.coeff recurrence5A3Square 173 = -((66618530425766791120096630457718427015145937217432369863819838718 * 10 ^ 70 + 568300084663008477477473782740142429702956664141804932507035729263011) * 10 ^ 70 + 8287016987060671877834712397837658609497092728773177944333754258094820)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_174 :
Polynomial.coeff recurrence5A3Square 174 = (90144666026527989555547934906854821629906272996804774247712167623 * 10 ^ 70 + 7377597772058183663756238623445306127050336719688241354398404899590317) * 10 ^ 70 + 9416248525240046521788102760107513287662533128250054818554445442139610
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_175 :
Polynomial.coeff recurrence5A3Square 175 = -((97594312156446209732460989547409350471316446003993429131655522930 * 10 ^ 70 + 8981142330140553183985689988790996516192936106800456577968528967899750) * 10 ^ 70 + 3422688766371698016709815840315038351680222914821601431695642674504620)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_176 :
Polynomial.coeff recurrence5A3Square 176 = (93759782940891402868351736704197845356217844441083034948706090488 * 10 ^ 70 + 8051900139711289180750271005753135322628529208618899162247437208663651) * 10 ^ 70 + 8031567490954005926602621140571084329282287679205930833728927155261302
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_177 :
Polynomial.coeff recurrence5A3Square 177 = -((83053442329299933801673203942571470787989281113116832495944316625 * 10 ^ 70 + 8334350170688637862291087110891419166067341792611353068167534880874709) * 10 ^ 70 + 8835811249583853969454141105501540267518695912076035997721606793564330)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_178 :
Polynomial.coeff recurrence5A3Square 178 = (69092074754004621748465050817926119887220607789414352059075923005 * 10 ^ 70 + 2368994417668275352121844554854229628161654927558325266482513165496862) * 10 ^ 70 + 7635385671048378620263788784989540224792898139681290424382888503457227
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_179 :
Polynomial.coeff recurrence5A3Square 179 = -((54527662505134348048755481403345343475135112273963252246306297071 * 10 ^ 70 + 5867139428658354816568186691845009164464602107855429120716645338990863) * 10 ^ 70 + 841060017061043969902944023637287700582006812569890751776800048224854)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_180 :
Polynomial.coeff recurrence5A3Square 180 = (41069334904829665223429420691885354147690383822646332439204146434 * 10 ^ 70 + 1274583547075494602820521096612911775918549939854693055255903553532871) * 10 ^ 70 + 7974908353985676960792199046252432258208517452186321151587928736623548
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_181 :
Polynomial.coeff recurrence5A3Square 181 = -((29627179825165827780785859958084825598820914877394685035577634931 * 10 ^ 70 + 1141340996096814057190369508276311840812290425131973919232863150188079) * 10 ^ 70 + 203531675740674464201093523288140401920010244632339135525187422967060)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_182 :
Polynomial.coeff recurrence5A3Square 182 = (20512082050075401465402704132563630919865096411408404633327304953 * 10 ^ 70 + 5894315194534747975228346261928155999066676801706866216765034148423815) * 10 ^ 70 + 2754633670650918571360208115167007003605698661644078046836031472048544
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_183 :
Polynomial.coeff recurrence5A3Square 183 = -((13640151924655458478605124992121883098498735849394152004177450278 * 10 ^ 70 + 1108969284404221450689836428488261314845148372916771293560357675034849) * 10 ^ 70 + 4384541785221592780803345029984723074298410898124611286738801400584026)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_184 :
Polynomial.coeff recurrence5A3Square 184 = (8708899677694449368390884871933188124987861981658393337181060605 * 10 ^ 70 + 671706148296579093767836037980950247935637062337371194964556646093085) * 10 ^ 70 + 2026697372434093491869433423960042365947375907117122480119527763686449
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_185 :
Polynomial.coeff recurrence5A3Square 185 = -((5329857611244955750094269894261024700221815681923578375374932014 * 10 ^ 70 + 2445288203463178085755156069027111210561443759377683743548472495428993) * 10 ^ 70 + 1946982518501859720299883256776095169405118614131255081120456674979630)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_186 :
Polynomial.coeff recurrence5A3Square 186 = (3115781803338343378749910981530944617448471166692068149122411109 * 10 ^ 70 + 5542822601127559208601321230759416156987576400403077751850073233040472) * 10 ^ 70 + 2672809582429015881171832469266087244673885081700007448448922546660769
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_187 :
Polynomial.coeff recurrence5A3Square 187 = -((1728864879779653182642533572085641520282383296963250946203179442 * 10 ^ 70 + 1196052238766766462240552552642168425120683034872981813696319288138777) * 10 ^ 70 + 6185499813309192304744914537940610880819968339474682645488020591615410)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_188 :
Polynomial.coeff recurrence5A3Square 188 = (900039877845548416690007908005419183714681244503497258028229643 * 10 ^ 70 + 1163526285230190291330789993758878015690936697130327572284210549262924) * 10 ^ 70 + 6721404678688055428925964799154507652240406217152833519762210848584983
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_189 :
Polynomial.coeff recurrence5A3Square 189 = -((429712233199633839991567293363439365139532470445696674062340781 * 10 ^ 70 + 1266080421415402396014443132396550435974585103110738532959311604829995) * 10 ^ 70 + 5488963517010354888201163563854527455213849092513384386559782951416072)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_190 :
Polynomial.coeff recurrence5A3Square 190 = (178554888260308744798605351965166093713191465780846669387654255 * 10 ^ 70 + 1932855898491804881767894909025224494921709035648160131941557785913763) * 10 ^ 70 + 3081809341175198990974473162624653973840552685051314099683159627887249
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_191 :
Polynomial.coeff recurrence5A3Square 191 = -((54550356320818597438313412533021651033068850470973022003055685 * 10 ^ 70 + 6851165584780857508574054735426056336397454108972425173765766917419896) * 10 ^ 70 + 2592832681028403285712879691308962779731925453896005595910323154106704)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_192 :
Polynomial.coeff recurrence5A3Square 192 = (79947986079124818781411508187643733264007354146059326235826 * 10 ^ 70 + 8788641382508637812167172088113913542853935351261498657428237994829208) * 10 ^ 70 + 8383355844330055557577817296688410381994863836563461300715694302074870
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_193 :
Polynomial.coeff recurrence5A3Square 193 = (19033585229871521603635727455854202438437269180620431995229184 * 10 ^ 70 + 6887226835084185243990397228568769895764039907375549617772294725447126) * 10 ^ 70 + 7733711428957881454155092267570076416130860253939500444169016806327422
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_194 :
Polynomial.coeff recurrence5A3Square 194 = -((21908149269648278913052561826394292426415896710593631842298270 * 10 ^ 70 + 7565396811212562719419877134326117000322586212972673598492327025181976) * 10 ^ 70 + 9220873766674773731400734255703854588622606299268753445166094278595146)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_195 :
Polynomial.coeff recurrence5A3Square 195 = (18525154999457191607976867945439538629780998034019553937159367 * 10 ^ 70 + 3399246308375386732823591470794107201397977864713150157160542741290606) * 10 ^ 70 + 541550666544015390877695442926669895765494946888180752712087473334776
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_196 :
Polynomial.coeff recurrence5A3Square 196 = -((13642155493564864168801327951141252711060597176702372943301745 * 10 ^ 70 + 1372836877418335030369345481056357285541438473873664775315050696012610) * 10 ^ 70 + 8428952499319725181187355720474458726530280358329790169220372948614205)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_197 :
Polynomial.coeff recurrence5A3Square 197 = (9222556739430457217591477642043334320190993912415588673929429 * 10 ^ 70 + 8761117695608078945469975531605396282759945780590815082813037157635986) * 10 ^ 70 + 8110621472275898222800497071759086378856074107190639038055011012874822