Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupC0Low.Coefficients0To25

Recurrence 2 lookup certificate: C0 source coefficients, low 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.recurrence2C0_coeff_0 :
Polynomial.coeff remainder4Coefficient0 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_1 :
Polynomial.coeff remainder4Coefficient0 1 = -480
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_2 :
Polynomial.coeff remainder4Coefficient0 2 = -1155556
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_3 :
Polynomial.coeff remainder4Coefficient0 3 = 9736172392
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_4 :
Polynomial.coeff remainder4Coefficient0 4 = -16423440806733
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_5 :
Polynomial.coeff remainder4Coefficient0 5 = 4962878559054749
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_6 :
Polynomial.coeff remainder4Coefficient0 6 = 102164852818091143
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_7 :
Polynomial.coeff remainder4Coefficient0 7 = -174570283367325557914
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_8 :
Polynomial.coeff remainder4Coefficient0 8 = 16971635485316593160253
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_9 :
Polynomial.coeff remainder4Coefficient0 9 = -1987372853128920730284497
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_10 :
Polynomial.coeff remainder4Coefficient0 10 = 1037153502365342951467098014
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_11 :
Polynomial.coeff remainder4Coefficient0 11 = -349526738997984038153494449661
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_12 :
Polynomial.coeff remainder4Coefficient0 12 = 84901689992003848492177873655587
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_13 :
Polynomial.coeff remainder4Coefficient0 13 = -16352667734463880226360448854219828
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_14 :
Polynomial.coeff remainder4Coefficient0 14 = 2565177297628097530010580556359543693
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_15 :
Polynomial.coeff remainder4Coefficient0 15 = -333800508239121059175948637360295552192
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_16 :
Polynomial.coeff remainder4Coefficient0 16 = 36587384198255758979280741147876340582674
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_17 :
Polynomial.coeff remainder4Coefficient0 17 = -3419412929303129369590936763792570525919843
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_18 :
Polynomial.coeff remainder4Coefficient0 18 = 275266221231594527722590210037775210341936415
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_19 :
Polynomial.coeff remainder4Coefficient0 19 = -19254132146361394764594199340404152527817392416
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_20 :
Polynomial.coeff remainder4Coefficient0 20 = 1179191434858326803678139570533696562234113231007
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_21 :
Polynomial.coeff remainder4Coefficient0 21 = -63662698240520829270727927863644116342844301394297
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_22 :
Polynomial.coeff remainder4Coefficient0 22 = 3048456799788126981426530242874006721063169129975568
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_23 :
Polynomial.coeff remainder4Coefficient0 23 = -130190017247630784430273724525535800743183253852586767
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_24 :
Polynomial.coeff remainder4Coefficient0 24 = 4984012111357720919132972081171726882070498470418930825
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_25 :
Polynomial.coeff remainder4Coefficient0 25 = -171833374329887690929979143920362797722934521553807165394