Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupC1High.Coefficients166To190

Recurrence 2 lookup certificate: C1 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.recurrence2C1_coeff_166 :
Polynomial.coeff remainder4Coefficient1 166 = 1250 * 10 ^ 70 + 7903442222304732803123971906028783063848574119434822864816834563953003
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_167 :
Polynomial.coeff remainder4Coefficient1 167 = -(14 * 10 ^ 70 + 9989615836734697970532791043680633945266608971793423361466969110295794)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_168 :
Polynomial.coeff remainder4Coefficient1 168 = -(14 * 10 ^ 70 + 8696398539325476469068356168921780691864510622423485343401920923605166)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_169 :
Polynomial.coeff remainder4Coefficient1 169 = 2 * 10 ^ 70 + 237063316334925680608760927303605068267938560261997819558586394122914
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_170 :
Polynomial.coeff remainder4Coefficient1 170 = -748371003927271741154170478339583777836960419996028824929270989581123
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_171 :
Polynomial.coeff remainder4Coefficient1 171 = -85500969710033529515701255008079454173238356005406635218287093039812
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_172 :
Polynomial.coeff remainder4Coefficient1 172 = 9805356358872421213404169395195216896652001757665991741785888748610
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_173 :
Polynomial.coeff remainder4Coefficient1 173 = -61345332488416245192841569760865389874036903242755294008937358735
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_174 :
Polynomial.coeff remainder4Coefficient1 174 = -30602577928356269945403679237996685764814476605133233014722791183
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_175 :
Polynomial.coeff remainder4Coefficient1 175 = 323186898189767301851367256237775098177011900046387817145431534
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_176 :
Polynomial.coeff remainder4Coefficient1 176 = 57076164149317311983241554774282234744487139323987989294860309
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_177 :
Polynomial.coeff remainder4Coefficient1 177 = 1329663713510284822304878170309472305717733391736680340167785
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_178 :
Polynomial.coeff remainder4Coefficient1 178 = 13522759127750948405565665267486800697891120261481180520272
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_179 :
Polynomial.coeff remainder4Coefficient1 179 = 68440232685480362737473256330659552453146279574330053768
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_180 :
Polynomial.coeff remainder4Coefficient1 180 = 156301300456882419884388060396740496525691255162599401
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_181 :
Polynomial.coeff remainder4Coefficient1 181 = 20821378000265036417859664107395263307004515217945
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_182 :
Polynomial.coeff remainder4Coefficient1 182 = -561782912259307626492836017518121175468993499202
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_183 :
Polynomial.coeff remainder4Coefficient1 183 = -908825169258193200572233082016061743080333582
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_184 :
Polynomial.coeff remainder4Coefficient1 184 = -492227487195799594960341191069630546220098
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_185 :
Polynomial.coeff remainder4Coefficient1 185 = -90673694400791428354037928543020554710
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_186 :
Polynomial.coeff remainder4Coefficient1 186 = -4894913024786264472437929522098555
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_187 :
Polynomial.coeff remainder4Coefficient1 187 = -60464546983171638597828541088
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_188 :
Polynomial.coeff remainder4Coefficient1 188 = -115387634732139429500246
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_189 :
Polynomial.coeff remainder4Coefficient1 189 = -16865704796555725
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_190 :
Polynomial.coeff remainder4Coefficient1 190 = -47165519