Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupC1High.Coefficients143To165

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_143 :
Polynomial.coeff remainder4Coefficient1 143 = 63833987296685336 * 10 ^ 70 + 9927896457014352553163178843160351426361393905523467070925818387006941
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_144 :
Polynomial.coeff remainder4Coefficient1 144 = -(77706310746925818 * 10 ^ 70 + 9403633184424262988037681780551087286842522895153329351979884176406813)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_145 :
Polynomial.coeff remainder4Coefficient1 145 = 49827838581298692 * 10 ^ 70 + 6820615413253005385631516989043117066448838542126675817693829149112231
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_146 :
Polynomial.coeff remainder4Coefficient1 146 = -(24999987339023179 * 10 ^ 70 + 2423386418842515798974386550642008525120457015155510342182912110759533)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_147 :
Polynomial.coeff remainder4Coefficient1 147 = 10637997518973879 * 10 ^ 70 + 9544210930931038741759333294278856596471174565216928960131597073670883
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_148 :
Polynomial.coeff remainder4Coefficient1 148 = -(3930940963288629 * 10 ^ 70 + 6315553273394981414344342170176498584790782399370749008786690806299115)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_149 :
Polynomial.coeff remainder4Coefficient1 149 = 1262336562008912 * 10 ^ 70 + 5683846670951538592040879112609354557220521235993047661661001967014925
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_150 :
Polynomial.coeff remainder4Coefficient1 150 = -(346002961033324 * 10 ^ 70 + 9623280924069551168423292386399703000518454170479798932605259239853739)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_151 :
Polynomial.coeff remainder4Coefficient1 151 = 76940976875028 * 10 ^ 70 + 1250381447313599468863811659386560414723345165060194381638294428035178
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_152 :
Polynomial.coeff remainder4Coefficient1 152 = -(11798116595990 * 10 ^ 70 + 1266487681441359892239350143809719252996705777684469693086800698811714)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_153 :
Polynomial.coeff remainder4Coefficient1 153 = 134764028710 * 10 ^ 70 + 3749399824005250007318494405695332273715697464435832669940297220384767
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_154 :
Polynomial.coeff remainder4Coefficient1 154 = 702660606139 * 10 ^ 70 + 8810161088365813323921298661676538910394339064465744026681226658424695
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_155 :
Polynomial.coeff remainder4Coefficient1 155 = -(302289043288 * 10 ^ 70 + 9290464488781490312876576753564812781320527228443094476621409514519136)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_156 :
Polynomial.coeff remainder4Coefficient1 156 = 81076818564 * 10 ^ 70 + 4552835858960223320939486592500333487733099804370226498268268865857444
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_157 :
Polynomial.coeff remainder4Coefficient1 157 = -(15064863955 * 10 ^ 70 + 3542516191515398184950568326064434999459840987436394851510740073126693)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_158 :
Polynomial.coeff remainder4Coefficient1 158 = 1577033140 * 10 ^ 70 + 3575342430895437961905750881845820513057422334386125077139738584521346
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_159 :
Polynomial.coeff remainder4Coefficient1 159 = 103143849 * 10 ^ 70 + 9419190608672874908783382977396589869424766742615775100022364462177475
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_160 :
Polynomial.coeff remainder4Coefficient1 160 = -(88848845 * 10 ^ 70 + 3598737416694792367378225998460057463258942004187451125805195248369565)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_161 :
Polynomial.coeff remainder4Coefficient1 161 = 21270475 * 10 ^ 70 + 6537571917646621422696742507746692908399014372752078350832949817247759
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_162 :
Polynomial.coeff remainder4Coefficient1 162 = -(2804518 * 10 ^ 70 + 3635839490541588126639601185006555879722503605206376046986677170440905)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_163 :
Polynomial.coeff remainder4Coefficient1 163 = 90136 * 10 ^ 70 + 2894240406696292517930480562922572098781818044089546111066844659963741
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_164 :
Polynomial.coeff remainder4Coefficient1 164 = 48665 * 10 ^ 70 + 4674396098259235177996779972908935063818266904937086611840757378704573
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_165 :
Polynomial.coeff remainder4Coefficient1 165 = -(11801 * 10 ^ 70 + 4729953012360969545582488938406817229717684913149581805680487802635014)