Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupC2High.Coefficients140To186

Recurrence 2 lookup certificate: C2 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.recurrence2C2_coeff_140 :
Polynomial.coeff remainder4Coefficient2 140 = 545495042251656678 * 10 ^ 70 + 4448047402110233460146282112556757291567967665075212206962081089569165
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_141 :
Polynomial.coeff remainder4Coefficient2 141 = -(239635525698333278 * 10 ^ 70 + 2313879726027214180604480213380039675328710039723652185594984982722881)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_142 :
Polynomial.coeff remainder4Coefficient2 142 = 98936186088592686 * 10 ^ 70 + 999798035647160554046509150553892349377879300720051505481113835226060
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_143 :
Polynomial.coeff remainder4Coefficient2 143 = -(38184727599314742 * 10 ^ 70 + 9711642300618301348353547144994237822801814416213389089581355340798977)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_144 :
Polynomial.coeff remainder4Coefficient2 144 = 13685700167421208 * 10 ^ 70 + 441960218832716707883599606323854120524379319121072077228824611642072
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_145 :
Polynomial.coeff remainder4Coefficient2 145 = -(4512962701163464 * 10 ^ 70 + 8481994650197117062797183134315190447379958138072976622656384777476829)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_146 :
Polynomial.coeff remainder4Coefficient2 146 = 1349937174563399 * 10 ^ 70 + 2366383376103963424797613579139842371246961828632613065521410288659204
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_147 :
Polynomial.coeff remainder4Coefficient2 147 = -(357504839514598 * 10 ^ 70 + 6264001012184531861179826681129668217238819294980375827349814318187155)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_148 :
Polynomial.coeff remainder4Coefficient2 148 = 79794795263487 * 10 ^ 70 + 3001422348877838102440219321132104321794504097291801071751528264013964
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_149 :
Polynomial.coeff remainder4Coefficient2 149 = -(13085779699821 * 10 ^ 70 + 7561263622115097279825692105824275409705351569275370805001196731315909)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_150 :
Polynomial.coeff remainder4Coefficient2 150 = 557848508684 * 10 ^ 70 + 3194049029470949951372079004904281088440799602826741906765519633180691
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_151 :
Polynomial.coeff remainder4Coefficient2 151 = 656491974330 * 10 ^ 70 + 1259271028764794897564872386758683949788656350642552684179839014462251
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_152 :
Polynomial.coeff remainder4Coefficient2 152 = -(340265097786 * 10 ^ 70 + 9073936987252594643044456356652589106723432010870921611703964077502102)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_153 :
Polynomial.coeff remainder4Coefficient2 153 = 110261265197 * 10 ^ 70 + 6606211127788267877361795094128304590273551701327081125314949560654168
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_154 :
Polynomial.coeff remainder4Coefficient2 154 = -(27369200514 * 10 ^ 70 + 3007499319135674520415723558904852651605530633918761890006680036424865)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_155 :
Polynomial.coeff remainder4Coefficient2 155 = 5341863670 * 10 ^ 70 + 3533521403882490129350488568993074985030032417003855160123865201318551
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_156 :
Polynomial.coeff remainder4Coefficient2 156 = -(777462185 * 10 ^ 70 + 4287032543423151395136377560713134475394336387200732060197148451687229)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_157 :
Polynomial.coeff remainder4Coefficient2 157 = 64874925 * 10 ^ 70 + 4819097285143644149880824481890867775232475613171423661072952397032363
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_158 :
Polynomial.coeff remainder4Coefficient2 158 = 4066755 * 10 ^ 70 + 9961745948466811916356930393490027724357280090943765495520663687537879
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_159 :
Polynomial.coeff remainder4Coefficient2 159 = -(2671670 * 10 ^ 70 + 449768319193609518989633960724072860960250174953457224823174829481186)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_160 :
Polynomial.coeff remainder4Coefficient2 160 = 527435 * 10 ^ 70 + 6025225703046170242979901357741635181363681816204785116299129863311508
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_161 :
Polynomial.coeff remainder4Coefficient2 161 = -(57843 * 10 ^ 70 + 3365242037667793316025326110860620185301292048009247099537570690234235)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_162 :
Polynomial.coeff remainder4Coefficient2 162 = 1759 * 10 ^ 70 + 8377451888598060835054508831783532371938876082709989283341087212863893
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_163 :
Polynomial.coeff remainder4Coefficient2 163 = 585 * 10 ^ 70 + 7324080631565493577444444058116452194427675603956331700136455457121921
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_164 :
Polynomial.coeff remainder4Coefficient2 164 = -(112 * 10 ^ 70 + 7047228734001551804772221975168972668695974820502998424925313345626848)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_165 :
Polynomial.coeff remainder4Coefficient2 165 = 8 * 10 ^ 70 + 6170654803447237825628813806279840136283737627718799899506883417704738
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_166 :
Polynomial.coeff remainder4Coefficient2 166 = 260304475161797145398747507909755831126921362946186995357748453767939
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_167 :
Polynomial.coeff remainder4Coefficient2 167 = -623110430768711450652133308005580578248691415521024213386880594118973
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_168 :
Polynomial.coeff remainder4Coefficient2 168 = 41776801331108241105978128716420030700017442670779391098954405488922
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_169 :
Polynomial.coeff remainder4Coefficient2 169 = 552873088182398204575602962978492116170266734493275883094696905346
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_170 :
Polynomial.coeff remainder4Coefficient2 170 = -146641573414660105079274449564423591228713461852171327308007703462
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_171 :
Polynomial.coeff remainder4Coefficient2 171 = 140414764137155687548391560719402298423384047790785358226966828
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_172 :
Polynomial.coeff remainder4Coefficient2 172 = 246756829723010629400696609968495046438482087364781599416547030
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_173 :
Polynomial.coeff remainder4Coefficient2 173 = 6374876097679124864271013837989479431461389504478683404698450
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_174 :
Polynomial.coeff remainder4Coefficient2 174 = 68644985716931685935093412619381806311742578076046833518791
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_175 :
Polynomial.coeff remainder4Coefficient2 175 = 364752712682660817273052048753785522516042208091698118328
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_176 :
Polynomial.coeff remainder4Coefficient2 176 = 887672225200959590046747140069739815284081905985503186
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_177 :
Polynomial.coeff remainder4Coefficient2 177 = 260416846363090404572065299936426001227011827652536
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_178 :
Polynomial.coeff remainder4Coefficient2 178 = -2999868740724368539976749597623483368695197658822
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_179 :
Polynomial.coeff remainder4Coefficient2 179 = -5293787106788466174945020234609187203594277827
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_180 :
Polynomial.coeff remainder4Coefficient2 180 = -3092215409250669568723570087366039416554849
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_181 :
Polynomial.coeff remainder4Coefficient2 181 = -623385139448741590273548450203781354774
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_182 :
Polynomial.coeff remainder4Coefficient2 182 = -37819466164327403912651638801913724
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_183 :
Polynomial.coeff remainder4Coefficient2 183 = -547300143822422198021388493673
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_184 :
Polynomial.coeff remainder4Coefficient2 184 = -1310874591511338125412131
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_185 :
Polynomial.coeff remainder4Coefficient2 185 = -274805999919516755
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_186 :
Polynomial.coeff remainder4Coefficient2 186 = -1255012469