Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupB5High

Recurrence 2 lookup certificate: B5 source coefficients, high 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.recurrence2B5_coeff_68 :
Polynomial.coeff remainder3Coefficient5 68 = 1573 * 10 ^ 70 + 3700482159318132242512486410154453982346751587044020014681765236104936
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_69 :
Polynomial.coeff remainder3Coefficient5 69 = -(7704 * 10 ^ 70 + 918225517736074921729336195990513293135974166709962259944549347487984)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_70 :
Polynomial.coeff remainder3Coefficient5 70 = 21548 * 10 ^ 70 + 9784207940916533650299384876288246083729670829769966431539795282755301
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_71 :
Polynomial.coeff remainder3Coefficient5 71 = -(37778 * 10 ^ 70 + 1753888803961828638061639688835594512078997877013100237833213875331715)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_72 :
Polynomial.coeff remainder3Coefficient5 72 = 14469 * 10 ^ 70 + 3952666072833585053620515821037495162493008316823504075366429204108104
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_73 :
Polynomial.coeff remainder3Coefficient5 73 = 189550 * 10 ^ 70 + 8554447424250237432462766301765926181207829128055282173822134556985390
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_74 :
Polynomial.coeff remainder3Coefficient5 74 = -(923653 * 10 ^ 70 + 5594132348555596946779758091358231885991776368090587872494569704894555)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_75 :
Polynomial.coeff remainder3Coefficient5 75 = 2891307 * 10 ^ 70 + 5527356861206989739822304185594896592679563225301983049716920497522603
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_76 :
Polynomial.coeff remainder3Coefficient5 76 = -(7282798 * 10 ^ 70 + 2308281931102051921601933607417406329156971195387916888822612581704519)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_77 :
Polynomial.coeff remainder3Coefficient5 77 = 15796790 * 10 ^ 70 + 9333484461609288275868338609808176164588548581655633392941335843756709
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_78 :
Polynomial.coeff remainder3Coefficient5 78 = -(30430443 * 10 ^ 70 + 1198938751297424810222037624245617522712593614063490138278830609064811)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_79 :
Polynomial.coeff remainder3Coefficient5 79 = 52961212 * 10 ^ 70 + 3679280822372791683194641512267340837658158128418351041129922782048672
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_80 :
Polynomial.coeff remainder3Coefficient5 80 = -(84171041 * 10 ^ 70 + 7408893468985812214369360201503454660116734631626444100440639462004271)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_81 :
Polynomial.coeff remainder3Coefficient5 81 = 123040369 * 10 ^ 70 + 9005659483630457618521670262184337185591494109073399139827395928714682
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_82 :
Polynomial.coeff remainder3Coefficient5 82 = -(166273088 * 10 ^ 70 + 2017418057918669283278748618087014388397199910139714258714508328729345)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_83 :
Polynomial.coeff remainder3Coefficient5 83 = 208496561 * 10 ^ 70 + 8315258459843686050587028944636622744493983962353207759297044654731947
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_84 :
Polynomial.coeff remainder3Coefficient5 84 = -(243264732 * 10 ^ 70 + 6235158778861948905430387116985610128303329311138506996275486962607249)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_85 :
Polynomial.coeff remainder3Coefficient5 85 = 264644716 * 10 ^ 70 + 6741888933563934245131887161077794221571807873883191441673518770514292
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_86 :
Polynomial.coeff remainder3Coefficient5 86 = -(268858287 * 10 ^ 70 + 8365336436617406242871454627367694745114585140934013065063317671139375)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_87 :
Polynomial.coeff remainder3Coefficient5 87 = 255359355 * 10 ^ 70 + 7271417913201208446836563835930399275607651619991705100169760218752352
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_88 :
Polynomial.coeff remainder3Coefficient5 88 = -(226930445 * 10 ^ 70 + 8244851130786977824229705264836156732253056194702450059501876420201137)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_89 :
Polynomial.coeff remainder3Coefficient5 89 = 188784429 * 10 ^ 70 + 7009957210035837767091600120116933918934224364197779982762460968274730
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_90 :
Polynomial.coeff remainder3Coefficient5 90 = -(147056074 * 10 ^ 70 + 9271792529933718642297334643268309425912084999014088297796059317143268)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_91 :
Polynomial.coeff remainder3Coefficient5 91 = 107264601 * 10 ^ 70 + 5655485347770105478432796670080315351963895547759087326290334576030275
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_92 :
Polynomial.coeff remainder3Coefficient5 92 = -(73250322 * 10 ^ 70 + 8668572862156810803118007404263776587791988126342028672689814708556496)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_93 :
Polynomial.coeff remainder3Coefficient5 93 = 46814430 * 10 ^ 70 + 853714753179464768165001736359478988720474738074794201969067930200703
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_94 :
Polynomial.coeff remainder3Coefficient5 94 = -(27984736 * 10 ^ 70 + 1235686798847775630656184850506128403611491407807494217458046530359994)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_95 :
Polynomial.coeff remainder3Coefficient5 95 = 15635270 * 10 ^ 70 + 4291582908774896798775330773343512151522814191987918443839200574530752
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_96 :
Polynomial.coeff remainder3Coefficient5 96 = -(8156796 * 10 ^ 70 + 4059342537181242914268387620031594439668585633103548300433367776799500)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_97 :
Polynomial.coeff remainder3Coefficient5 97 = 3968845 * 10 ^ 70 + 707802158972314189699432560347948576501612799974069615748044579376778
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_98 :
Polynomial.coeff remainder3Coefficient5 98 = -(1798653 * 10 ^ 70 + 2606676608036032930939094674071980371221241581198247246483649023772656)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_99 :
Polynomial.coeff remainder3Coefficient5 99 = 758018 * 10 ^ 70 + 4208916519539297790360378321882817195130328393419482122791868070465564
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_100 :
Polynomial.coeff remainder3Coefficient5 100 = -(296527 * 10 ^ 70 + 2352933744063046617640492315934479033772964798254129430881919971030965)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_101 :
Polynomial.coeff remainder3Coefficient5 101 = 107445 * 10 ^ 70 + 4443066940163824257190740599399667653184295345415616823262510873205420
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_102 :
Polynomial.coeff remainder3Coefficient5 102 = -(35975 * 10 ^ 70 + 3689819533977161037169955334229921734293980497730097550408841912945356)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_103 :
Polynomial.coeff remainder3Coefficient5 103 = 11100 * 10 ^ 70 + 304750588690367789764447195187821765514094402108803291725926867574462
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_104 :
Polynomial.coeff remainder3Coefficient5 104 = -(3146 * 10 ^ 70 + 1878559035609974432185665843772417900361319406666511490799428414130423)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_105 :
Polynomial.coeff remainder3Coefficient5 105 = 816 * 10 ^ 70 + 2689132900902153483871891507015679161297263692329257292945453729701981
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_106 :
Polynomial.coeff remainder3Coefficient5 106 = -(193 * 10 ^ 70 + 596903859232854114376492422850788611645700447386490662054897860910174)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_107 :
Polynomial.coeff remainder3Coefficient5 107 = 41 * 10 ^ 70 + 4301773830745419847878688478118867785217992374857152748342667625328316
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_108 :
Polynomial.coeff remainder3Coefficient5 108 = -(8 * 10 ^ 70 + 232712501281461530959948749617306803171906720627872012789886366106333)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_109 :
Polynomial.coeff remainder3Coefficient5 109 = 1 * 10 ^ 70 + 3933501439803518606305450146542102579122155314673201932427275093563651
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_110 :
Polynomial.coeff remainder3Coefficient5 110 = -2154010580000914123888347706398050309774017660112198043582971557811006
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_111 :
Polynomial.coeff remainder3Coefficient5 111 = 293867853613697882417068445880469772403917429438929376490465112531229
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_112 :
Polynomial.coeff remainder3Coefficient5 112 = -35018937038253135983096510644117003315940010844022081388059837272272
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_113 :
Polynomial.coeff remainder3Coefficient5 113 = 3600251316487800894275753333865655352187404784049787781823472171617
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_114 :
Polynomial.coeff remainder3Coefficient5 114 = -314569908194423288328232713754290979147036329351124493885887477841
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_115 :
Polynomial.coeff remainder3Coefficient5 115 = 22930458519256445288231122943193823159909427427981409944781646074
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_116 :
Polynomial.coeff remainder3Coefficient5 116 = -1362504344401340245160496691822587524683394673409576352415777549
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_117 :
Polynomial.coeff remainder3Coefficient5 117 = 64061390604558097883906764110598623800098919211954763283360665
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_118 :
Polynomial.coeff remainder3Coefficient5 118 = -2292100627717888929660294276473888128612784009271797951977446
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_119 :
Polynomial.coeff remainder3Coefficient5 119 = 59151732100970484544108579724157902403400413763886616722712
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_120 :
Polynomial.coeff remainder3Coefficient5 120 = -1016073560684526630577199370871922826342038529185970779716
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_121 :
Polynomial.coeff remainder3Coefficient5 121 = 10012740810256628612796853277483596506283317629267265714
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_122 :
Polynomial.coeff remainder3Coefficient5 122 = -33354150504035218502672229077114828172928999151260057
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_123 :
Polynomial.coeff remainder3Coefficient5 123 = -255742389286012772217283101849178090848564383478337
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_124 :
Polynomial.coeff remainder3Coefficient5 124 = 2285350403425215580504322667170907334123440058042
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_125 :
Polynomial.coeff remainder3Coefficient5 125 = -2818287159834181677550113595790244618964107953
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_126 :
Polynomial.coeff remainder3Coefficient5 126 = -19577197265577220913540397294542570172671329
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_127 :
Polynomial.coeff remainder3Coefficient5 127 = 68539716393261301098654953524650645861846
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_128 :
Polynomial.coeff remainder3Coefficient5 128 = -80955427547538972733980674317060011479
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_129 :
Polynomial.coeff remainder3Coefficient5 129 = 37352905326245285965819736386876315
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_130 :
Polynomial.coeff remainder3Coefficient5 130 = -5905487124530116060313320642201
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_131 :
Polynomial.coeff remainder3Coefficient5 131 = 249741379239703289263231179
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_132 :
Polynomial.coeff remainder3Coefficient5 132 = -1912620390008597624124
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_133 :
Polynomial.coeff remainder3Coefficient5 133 = 1363823716622532
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_134 :
Polynomial.coeff remainder3Coefficient5 134 = -9250229