Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupA1Low.Coefficients49To72

Recurrence 4 lookup certificate: A1 source coefficients, low half #

This is a checked coefficient-lookup shard for the fourth pseudo-division recurrence in the order-seven certificate.

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_49 :
Polynomial.coeff remainder4Coefficient1 49 = -(38976547488308 * 10 ^ 70 + 8535081623269732907378387651721548672443547865407337010760433724411380)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_50 :
Polynomial.coeff remainder4Coefficient1 50 = 227876815132903 * 10 ^ 70 + 8130399749565011639291539228787923292760631720261034048010849231666858
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_51 :
Polynomial.coeff remainder4Coefficient1 51 = -(1269510450582678 * 10 ^ 70 + 2892481863198292581256383414011578747231470300667231198801565973426807)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_52 :
Polynomial.coeff remainder4Coefficient1 52 = 6745301733634627 * 10 ^ 70 + 2231776744779339964697030812369871132254799924513142076707324150166703
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_53 :
Polynomial.coeff remainder4Coefficient1 53 = -(34210980983408997 * 10 ^ 70 + 8565791398551663863949000565087988472441523123412289097836462120581266)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_54 :
Polynomial.coeff remainder4Coefficient1 54 = 165760221770890667 * 10 ^ 70 + 8224452479287825958484598081492463395293895852036027373081113385729932
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_55 :
Polynomial.coeff remainder4Coefficient1 55 = -(767856092205903478 * 10 ^ 70 + 7722332295922980439961774002758239776092657012760543654233121873190130)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_56 :
Polynomial.coeff remainder4Coefficient1 56 = 3403153384502619035 * 10 ^ 70 + 2943571461712980749550121587784121770683821147023182173060110273946781
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_57 :
Polynomial.coeff remainder4Coefficient1 57 = -(14440660066567410247 * 10 ^ 70 + 287980673722551576562591887761278526370852514753630119267755802479784)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_58 :
Polynomial.coeff remainder4Coefficient1 58 = 58706074425889142959 * 10 ^ 70 + 4557604513109674847348769489972300756774014339650318526386503308724496
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_59 :
Polynomial.coeff remainder4Coefficient1 59 = -(228792544603131752478 * 10 ^ 70 + 5915767155317042018359168516557019633578765027858830736157915102047096)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_60 :
Polynomial.coeff remainder4Coefficient1 60 = 855307495182810774917 * 10 ^ 70 + 313852133928521286735576802571062556827825680954988027449065505642184
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_61 :
Polynomial.coeff remainder4Coefficient1 61 = -(3068810333464351392916 * 10 ^ 70 + 3822702293769927939608367962889539753670501169483301692722715689352725)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_62 :
Polynomial.coeff remainder4Coefficient1 62 = 10573495422147437811870 * 10 ^ 70 + 6975960113146400135892896094096316851286366501720999586773409669860056
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_63 :
Polynomial.coeff remainder4Coefficient1 63 = -(35001726155326599916621 * 10 ^ 70 + 8973739555062517366541477481343072499966506009582570851383762977004599)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_64 :
Polynomial.coeff remainder4Coefficient1 64 = 111376348915207219057481 * 10 ^ 70 + 730887326874863757760322028849217993721538823215105066748692981063704
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_65 :
Polynomial.coeff remainder4Coefficient1 65 = -(340822769397646769605329 * 10 ^ 70 + 6729322117803950111470866598248880441804984284505792543178905136933392)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_66 :
Polynomial.coeff remainder4Coefficient1 66 = 1003426254664093251011625 * 10 ^ 70 + 7805689974797051060371536773000316963738713186463382329270374169266577
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_67 :
Polynomial.coeff remainder4Coefficient1 67 = -(2843431416857457669197928 * 10 ^ 70 + 4540009642622081370233800703244254389781134029420728506196320001190545)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_68 :
Polynomial.coeff remainder4Coefficient1 68 = 7758364460356831420654464 * 10 ^ 70 + 6582705060785504859812589618160858740754180295319239420551237993013739
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_69 :
Polynomial.coeff remainder4Coefficient1 69 = -(20390518154643844804702799 * 10 ^ 70 + 5988998241373603909354136066005146736381546554364670148342408963828596)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_70 :
Polynomial.coeff remainder4Coefficient1 70 = 51637923203455014761685106 * 10 ^ 70 + 9286848232462922558845912860433930888479075839968059105391075478587075
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_71 :
Polynomial.coeff remainder4Coefficient1 71 = -(126047720140464444919525213 * 10 ^ 70 + 1338711699635030830934936403236827765612243610584452521167171063194312)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_72 :
Polynomial.coeff remainder4Coefficient1 72 = 296662126045632265429404094 * 10 ^ 70 + 9018023439517491037496040843323362386345956725018735847397895487915472