Recurrence 4 lookup certificate: A0 source coefficients, high half #
This is a checked coefficient-lookup shard for the fourth pseudo-division recurrence in the order-seven certificate.
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_98 :
Polynomial.coeff remainder4Coefficient0 98 = 12662604029483479757195248051429 * 10 ^ 70 + 2180009587081760533165610098963522774357757065017484508971799156382836
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_99 :
Polynomial.coeff remainder4Coefficient0 99 = -(12632148482534420193536655608232 * 10 ^ 70 + 6148735100196612474026939368204357909253178140160758936454815644166696)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_100 :
Polynomial.coeff remainder4Coefficient0 100 = 12230126503601930341531452801230 * 10 ^ 70 + 4907393025986429557483066527253106630883182523782152055356014364325738
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_101 :
Polynomial.coeff remainder4Coefficient0 101 = -(11495563806837846253007446464285 * 10 ^ 70 + 9908237737801388516615475027501476851818983893644236746873240044281827)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_102 :
Polynomial.coeff remainder4Coefficient0 102 = 10493526471039670206565701912836 * 10 ^ 70 + 3206581172654491977992962981300636989593654077415105199601658010018037
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_103 :
Polynomial.coeff remainder4Coefficient0 103 = -(9305654995741843011486379733974 * 10 ^ 70 + 2466549319657923719821590313925592279407849583250057840444537701689525)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_104 :
Polynomial.coeff remainder4Coefficient0 104 = 8019374579993495546092908358739 * 10 ^ 70 + 6213766088863321819627230907331641852778063353176704322117091952393838
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_105 :
Polynomial.coeff remainder4Coefficient0 105 = -(6717716837624141703740563540663 * 10 ^ 70 + 7009835423428541809074248361209103000730135920219318270762023196963841)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_106 :
Polynomial.coeff remainder4Coefficient0 106 = 5471293281582856614101615982839 * 10 ^ 70 + 7660686624970568832893382254160742719901660530258973068987360397800664
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_107 :
Polynomial.coeff remainder4Coefficient0 107 = -(4333300911435324100510622347716 * 10 ^ 70 + 9006285099269362645699371981190478917957817576353834422942697688414949)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_108 :
Polynomial.coeff remainder4Coefficient0 108 = 3337722509207044125978682844943 * 10 ^ 70 + 6888088146998009550775937263797688852956198465792959932334606410340605
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_109 :
Polynomial.coeff remainder4Coefficient0 109 = -(2500288624320017241248628512307 * 10 ^ 70 + 7333040066900144193559513134335415011920789386673805526194072509470971)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_110 :
Polynomial.coeff remainder4Coefficient0 110 = 1821400921560176799412849637655 * 10 ^ 70 + 4248134440622365374814229327520036047042332052019722107045243251748107
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_111 :
Polynomial.coeff remainder4Coefficient0 111 = -(1290098797641827245511677042636 * 10 ^ 70 + 1117259237589694742558650146762244516615780377440442632468301836509693)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_112 :
Polynomial.coeff remainder4Coefficient0 112 = 888237308756652257076169893393 * 10 ^ 70 + 1998564198884533227143845133678795769295569834266830431762401028405012
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_113 :
Polynomial.coeff remainder4Coefficient0 113 = -(594254865299328145856774634785 * 10 ^ 70 + 2255136537423787501429144906382914636755851784277345405858704500248988)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_114 :
Polynomial.coeff remainder4Coefficient0 114 = 386162167414565511039597145135 * 10 ^ 70 + 8927048912926417243294689358176233525448625139119174233523511264696948
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_115 :
Polynomial.coeff remainder4Coefficient0 115 = -(243616817395785654293355366889 * 10 ^ 70 + 569449587307747636021921105236983100534372388041396308390473458905844)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_116 :
Polynomial.coeff remainder4Coefficient0 116 = 149125063373972638456726829127 * 10 ^ 70 + 75882600450616815235209148286537305636532802475313193501966740361357
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_117 :
Polynomial.coeff remainder4Coefficient0 117 = -(88521693551638962344433609686 * 10 ^ 70 + 5658420195959387878825044945900972219761050604641867818095167097415767)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_118 :
Polynomial.coeff remainder4Coefficient0 118 = 50926725241697205679038206318 * 10 ^ 70 + 1109735462791639457453461198421574353339340863613119796821972197776385
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_119 :
Polynomial.coeff remainder4Coefficient0 119 = -(28377767018573920800728208444 * 10 ^ 70 + 4411767286395976604516072586918306535338214559109218648594455052823570)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_120 :
Polynomial.coeff remainder4Coefficient0 120 = 15307050905468875091689382938 * 10 ^ 70 + 8517833970706280802032143818843438745772413605297262732057065643004876
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_121 :
Polynomial.coeff remainder4Coefficient0 121 = -(7988067482521468214447588041 * 10 ^ 70 + 5021401559061301876770854651563396310945684215254224789233995147201916)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_122 :
Polynomial.coeff remainder4Coefficient0 122 = 4030910409351765866568855177 * 10 ^ 70 + 4002702699996601610905479054242087687966505088654551009611193854506956
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_123 :
Polynomial.coeff remainder4Coefficient0 123 = -(1965959803442018964242243123 * 10 ^ 70 + 7518250458131436693718989939518336017115117182576367161321289862539042)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_124 :
Polynomial.coeff remainder4Coefficient0 124 = 926369873267232628347995011 * 10 ^ 70 + 9063956543496492515726203072200778978532344750130083074292290492617528
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_125 :
Polynomial.coeff remainder4Coefficient0 125 = -(421591279968884999075981042 * 10 ^ 70 + 3574630129915741252372484670899997963862324261798153052452984602912208)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_126 :
Polynomial.coeff remainder4Coefficient0 126 = 185259622283411307861515761 * 10 ^ 70 + 4276997510506997085284286083259069147730550769855520321525719001923194
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_127 :
Polynomial.coeff remainder4Coefficient0 127 = -(78585826526001038936607656 * 10 ^ 70 + 9384857276472626283626358731911234352063969411485792704621660776776354)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_128 :
Polynomial.coeff remainder4Coefficient0 128 = 32169581093595491238347410 * 10 ^ 70 + 5457065748459244161943360879419341203113287467726101807530815010869209
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_129 :
Polynomial.coeff remainder4Coefficient0 129 = -(12701532305580758981869393 * 10 ^ 70 + 9983861809005141790222295341517889348189439411915412935684901186703249)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_130 :
Polynomial.coeff remainder4Coefficient0 130 = 4832407485142669103604109 * 10 ^ 70 + 4721842852474137295827183509955857824460899585581078019896944505665114
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_131 :
Polynomial.coeff remainder4Coefficient0 131 = -(1768686219770742383612894 * 10 ^ 70 + 8229003143792222106171519931896192825804973477202712212640706043473210)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_132 :
Polynomial.coeff remainder4Coefficient0 132 = 621114531918855517631801 * 10 ^ 70 + 8717277488710337064758040279934454229239953558466606442510120418980142
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_133 :
Polynomial.coeff remainder4Coefficient0 133 = -(208486816178194828335375 * 10 ^ 70 + 1867957221253412805803519634062942669876278621148888472516713577948315)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_134 :
Polynomial.coeff remainder4Coefficient0 134 = 66582855886621409456102 * 10 ^ 70 + 3655397455171852542239374068652319004731304805759406940300851074927160
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_135 :
Polynomial.coeff remainder4Coefficient0 135 = -(20159260850093237946271 * 10 ^ 70 + 7923808634549548301395976506419878063048853253855941199215641267367734)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_136 :
Polynomial.coeff remainder4Coefficient0 136 = 5811057359225377074159 * 10 ^ 70 + 2308783698209844404775846232880797963742703507883672587042853145083240
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_137 :
Polynomial.coeff remainder4Coefficient0 137 = -(1646781746325023378546 * 10 ^ 70 + 3002771692627547415566507959451894040923261544260465977194023645689406)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_138 :
Polynomial.coeff remainder4Coefficient0 138 = 506767745695882665649 * 10 ^ 70 + 4802377291967996322488940339032824922973525105513771493673889786327703
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_139 :
Polynomial.coeff remainder4Coefficient0 139 = -(197946152086317438183 * 10 ^ 70 + 8963682910249173038027472331925446763620985973139180598096838704353132)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_140 :
Polynomial.coeff remainder4Coefficient0 140 = 101242643784047159708 * 10 ^ 70 + 7639851903285467950777554264908212689932507934270083873145824625390286
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_141 :
Polynomial.coeff remainder4Coefficient0 141 = -(58711666528865418899 * 10 ^ 70 + 84485370387462315861002146253164023248959322499495099409498451605896)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_142 :
Polynomial.coeff remainder4Coefficient0 142 = 34074759913310788545 * 10 ^ 70 + 3681430593449313176893901264438370580639581632036713276967762101034757
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_143 :
Polynomial.coeff remainder4Coefficient0 143 = -(18836755067944890009 * 10 ^ 70 + 2307650178385255172990306481893427253590432990430689415464963467522189)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_144 :
Polynomial.coeff remainder4Coefficient0 144 = 9789817918703860593 * 10 ^ 70 + 2460234275820622197149787784046631454571167813448784816051813439014143
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_145 :
Polynomial.coeff remainder4Coefficient0 145 = -(4771656339941745681 * 10 ^ 70 + 5817923802835406294553144121332619012770916698889854590375114699627608)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_146 :
Polynomial.coeff remainder4Coefficient0 146 = 2179059921661511888 * 10 ^ 70 + 991752452806648450968465558688246233946116322420926607056820994759497
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_147 :
Polynomial.coeff remainder4Coefficient0 147 = -(930438017594896638 * 10 ^ 70 + 6650817082302097075734917481119248244934997071052476678789216854859040)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_148 :
Polynomial.coeff remainder4Coefficient0 148 = 370078080084612672 * 10 ^ 70 + 6356268494519348454107964577116556841179398797321382685185587977969958
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_149 :
Polynomial.coeff remainder4Coefficient0 149 = -(136324086262083576 * 10 ^ 70 + 8246127665592509277672122803695542468580504597063369582241026083316053)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_150 :
Polynomial.coeff remainder4Coefficient0 150 = 46114161072042203 * 10 ^ 70 + 1619855561256426869109327039185942397130099847618310755502120843935805
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_151 :
Polynomial.coeff remainder4Coefficient0 151 = -(14141637145293236 * 10 ^ 70 + 6696660424614082136556413716638760770015715444095244284927265056776749)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_152 :
Polynomial.coeff remainder4Coefficient0 152 = 3849065333280932 * 10 ^ 70 + 8191852857828602130803663147684770773644642822376664781584286416155514
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_153 :
Polynomial.coeff remainder4Coefficient0 153 = -(892538137145727 * 10 ^ 70 + 8589245934693804232998064720111038488256438425342463453413630502594490)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_154 :
Polynomial.coeff remainder4Coefficient0 154 = 158900984539287 * 10 ^ 70 + 8213885013155175857050104770356610490363088824067103302086798702172890
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_155 :
Polynomial.coeff remainder4Coefficient0 155 = -(12845979152437 * 10 ^ 70 + 3952102125208711633256306570477379602297413297266602914312942847991116)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_156 :
Polynomial.coeff remainder4Coefficient0 156 = -(4952009817960 * 10 ^ 70 + 9766051920037663089847934235957144678347013097709693482200759458430610)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_157 :
Polynomial.coeff remainder4Coefficient0 157 = 3130923925535 * 10 ^ 70 + 7051172609300198008448717376092167422365900102224697565232535215125597
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_158 :
Polynomial.coeff remainder4Coefficient0 158 = -(1090353929656 * 10 ^ 70 + 1802487035470916553142686351407780548265950620925894539180506989180889)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_159 :
Polynomial.coeff remainder4Coefficient0 159 = 289732706217 * 10 ^ 70 + 2954703749019295892016393876716821923603526598093827252836550846592953
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_160 :
Polynomial.coeff remainder4Coefficient0 160 = -(62735336779 * 10 ^ 70 + 2789377103612303012058938534008591191932022968962835664652448891380099)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_161 :
Polynomial.coeff remainder4Coefficient0 161 = 11201421520 * 10 ^ 70 + 8401315213701625437984408347409685991178020441655906033199560639454476
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_162 :
Polynomial.coeff remainder4Coefficient0 162 = -(1624714740 * 10 ^ 70 + 7361104903942987222452242785258853936932178308834787764395759665560181)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_163 :
Polynomial.coeff remainder4Coefficient0 163 = 182584385 * 10 ^ 70 + 7604499146126937649075375543776365546152693771193848074797577335659711
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_164 :
Polynomial.coeff remainder4Coefficient0 164 = -(13817162 * 10 ^ 70 + 7214269463011922325848156704753591889865036468984965071567793113452941)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_165 :
Polynomial.coeff remainder4Coefficient0 165 = 209782 * 10 ^ 70 + 2094106489120588856037917536419340071433635105084013564343611263547470
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_166 :
Polynomial.coeff remainder4Coefficient0 166 = 145206 * 10 ^ 70 + 4528597046033119626948008317148313523207739024886427213817137504083847
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_167 :
Polynomial.coeff remainder4Coefficient0 167 = -(35509 * 10 ^ 70 + 721851320102010514722188083833589047530319007515966311486773027305418)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_168 :
Polynomial.coeff remainder4Coefficient0 168 = 6653 * 10 ^ 70 + 5492775502688787126444689998100435765105082833122206676907646117739069
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_169 :
Polynomial.coeff remainder4Coefficient0 169 = -(1073 * 10 ^ 70 + 1787471038864785302093506654383403722115820053168548171692481888824813)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_170 :
Polynomial.coeff remainder4Coefficient0 170 = 126 * 10 ^ 70 + 4465680900694424296929497460633001937576356380218108765012949936948604
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_171 :
Polynomial.coeff remainder4Coefficient0 171 = -(7 * 10 ^ 70 + 566883241089539501574168803224841998247744390462042092115746606585737)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_172 :
Polynomial.coeff remainder4Coefficient0 172 = -5949021069314912499218015499466762175779153381151659091216591557085197
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_173 :
Polynomial.coeff remainder4Coefficient0 173 = 1550380030422564465875269695055190298347996242193328209760210880699813
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_174 :
Polynomial.coeff remainder4Coefficient0 174 = -105855926497116723523780251450470580706896012768015499477968758417400
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_175 :
Polynomial.coeff remainder4Coefficient0 175 = -2838077055611550274189583444950879257865316421125520017061330837915
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_176 :
Polynomial.coeff remainder4Coefficient0 176 = 783590988982254652111397081543146640551367615803055901369869344387
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_177 :
Polynomial.coeff remainder4Coefficient0 177 = -18372827940877057673746240632768768859675347009073454012456445736
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_178 :
Polynomial.coeff remainder4Coefficient0 178 = -2274138631337607890492464187160830175346527766501608262674397586
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_179 :
Polynomial.coeff remainder4Coefficient0 179 = 49144424934164725853973261610454550096791534782749823789854331
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_180 :
Polynomial.coeff remainder4Coefficient0 180 = 4883363746765941070383021567347045919911709669465415663317523
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_181 :
Polynomial.coeff remainder4Coefficient0 181 = 104482058353109320795095882459950782183495671711564601157820
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_182 :
Polynomial.coeff remainder4Coefficient0 182 = 1013312218865942400154746725814114442928670347104302841719
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_183 :
Polynomial.coeff remainder4Coefficient0 183 = 4929570330808463102337290866341963053483875340733703656