Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupA1Low

Recurrence 2 lookup certificate: A1 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.recurrence2A1_coeff_0 :
Polynomial.coeff remainder2Coefficient1 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_1 :
Polynomial.coeff remainder2Coefficient1 1 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_2 :
Polynomial.coeff remainder2Coefficient1 2 = -23
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_3 :
Polynomial.coeff remainder2Coefficient1 3 = 991446
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_4 :
Polynomial.coeff remainder2Coefficient1 4 = 34314719
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_5 :
Polynomial.coeff remainder2Coefficient1 5 = -182010007593
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_6 :
Polynomial.coeff remainder2Coefficient1 6 = 12713487257368
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_7 :
Polynomial.coeff remainder2Coefficient1 7 = 809774120213950
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_8 :
Polynomial.coeff remainder2Coefficient1 8 = -24940064428596179
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_9 :
Polynomial.coeff remainder2Coefficient1 9 = -1511187499165252688
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_10 :
Polynomial.coeff remainder2Coefficient1 10 = -1401006467656754001
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_11 :
Polynomial.coeff remainder2Coefficient1 11 = 1057485838428164119588
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_12 :
Polynomial.coeff remainder2Coefficient1 12 = 14904717066199156916092
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_13 :
Polynomial.coeff remainder2Coefficient1 13 = -230250439109250632924208
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_14 :
Polynomial.coeff remainder2Coefficient1 14 = -7159433264249329204390444
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_15 :
Polynomial.coeff remainder2Coefficient1 15 = -800944141195000428913534
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_16 :
Polynomial.coeff remainder2Coefficient1 16 = 1336715720568965017819040794
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_17 :
Polynomial.coeff remainder2Coefficient1 17 = 9371219754866468327646862794
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_18 :
Polynomial.coeff remainder2Coefficient1 18 = -152159977597680694262199235725
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_19 :
Polynomial.coeff remainder2Coefficient1 19 = -1476675698552842302366816083544
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_20 :
Polynomial.coeff remainder2Coefficient1 20 = 7423831494855042805865550540966
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_21 :
Polynomial.coeff remainder2Coefficient1 21 = 166980362579297990515818353437658
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_22 :
Polynomial.coeff remainder2Coefficient1 22 = -338050950523730163560503266156439
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_23 :
Polynomial.coeff remainder2Coefficient1 23 = -10229350116733897326878981007695336
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_24 :
Polynomial.coeff remainder2Coefficient1 24 = -2125560260375172499905965264154931
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_25 :
Polynomial.coeff remainder2Coefficient1 25 = 563370211501071328312802386841574086
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_26 :
Polynomial.coeff remainder2Coefficient1 26 = 268943619019748947580124367300453358
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_27 :
Polynomial.coeff remainder2Coefficient1 27 = -22337226396841398490007237712497405760
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_28 :
Polynomial.coeff remainder2Coefficient1 28 = -16302087361960395159433645119209771205
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_29 :
Polynomial.coeff remainder2Coefficient1 29 = 782884778513075620609733485006308898812
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_30 :
Polynomial.coeff remainder2Coefficient1 30 = 169100928911810487969607712933238095601
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_31 :
Polynomial.coeff remainder2Coefficient1 31 = -22434483518242757074625435655352319831718
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_32 :
Polynomial.coeff remainder2Coefficient1 32 = 12149129729855203374463191490851350845219
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_33 :
Polynomial.coeff remainder2Coefficient1 33 = 537688842212710594891401914117782804026329
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_34 :
Polynomial.coeff remainder2Coefficient1 34 = -866296460575465796670455267867388753669369
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_35 :
Polynomial.coeff remainder2Coefficient1 35 = -10178800343993652398732960755834833985355521
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_36 :
Polynomial.coeff remainder2Coefficient1 36 = 30845305703298606992929688144684386050348722
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_37 :
Polynomial.coeff remainder2Coefficient1 37 = 138143825322861061374501546913615689092833736
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_38 :
Polynomial.coeff remainder2Coefficient1 38 = -744345593375753309946174316548546440583310611
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_39 :
Polynomial.coeff remainder2Coefficient1 39 = -895207211253094452398187469388442171570590165
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_40 :
Polynomial.coeff remainder2Coefficient1 40 = 12602628389526258851354891566204867902883476569
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_41 :
Polynomial.coeff remainder2Coefficient1 41 = -11789716434675680598066479227024573301751833031
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_42 :
Polynomial.coeff remainder2Coefficient1 42 = -139165872516838418896158854667393896510709872301
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_43 :
Polynomial.coeff remainder2Coefficient1 43 = 432112768142442353814148894616481470942321809786
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_44 :
Polynomial.coeff remainder2Coefficient1 44 = 648401638615966186456668747610539522190161225558
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_45 :
Polynomial.coeff remainder2Coefficient1 45 = -6037767278326563296666525835768529343305035119745
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_46 :
Polynomial.coeff remainder2Coefficient1 46 = 7319164040280728673013255566132109193578495146294
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_47 :
Polynomial.coeff remainder2Coefficient1 47 = 39376151809298759682298403303322297574478351376786
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_48 :
Polynomial.coeff remainder2Coefficient1 48 = -158544148055671054942981428221540990703068279312848
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_49 :
Polynomial.coeff remainder2Coefficient1 49 = 63358724873144633399933389938629023169622069684614
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_50 :
Polynomial.coeff remainder2Coefficient1 50 = 1064558347078202935519998281089920262378412868830515
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_51 :
Polynomial.coeff remainder2Coefficient1 51 = -3146619741164609779553998395203135504539567542823798
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_52 :
Polynomial.coeff remainder2Coefficient1 52 = 876307759424208137110477158844935261665956234512959
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_53 :
Polynomial.coeff remainder2Coefficient1 53 = 17552225484796966209684620157723463839167888348993832
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_54 :
Polynomial.coeff remainder2Coefficient1 54 = -51060801395036558645419750914266778279505713183364077
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_55 :
Polynomial.coeff remainder2Coefficient1 55 = 38708632590349550038909320209836313832035801399688659
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_56 :
Polynomial.coeff remainder2Coefficient1 56 = 156122700235894541215359928419238137620803549708792141
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A1_coeff_57 :
Polynomial.coeff remainder2Coefficient1 57 = -595906504110546317847580435390630519293736106243862022