Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupA2Low

Recurrence 2 lookup certificate: A2 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.recurrence2A2_coeff_0 :
Polynomial.coeff remainder2Coefficient2 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_1 :
Polynomial.coeff remainder2Coefficient2 1 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_2 :
Polynomial.coeff remainder2Coefficient2 2 = -4313
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_3 :
Polynomial.coeff remainder2Coefficient2 3 = 18508415
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_4 :
Polynomial.coeff remainder2Coefficient2 4 = -1179368522
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_5 :
Polynomial.coeff remainder2Coefficient2 5 = -726119201869
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_6 :
Polynomial.coeff remainder2Coefficient2 6 = 64443948614929
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_7 :
Polynomial.coeff remainder2Coefficient2 7 = -1634796781931808
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_8 :
Polynomial.coeff remainder2Coefficient2 8 = -53104121001510770
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_9 :
Polynomial.coeff remainder2Coefficient2 9 = 4429251272553627031
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_10 :
Polynomial.coeff remainder2Coefficient2 10 = 44894677717832501843
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_11 :
Polynomial.coeff remainder2Coefficient2 11 = -3305729713116580021438
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_12 :
Polynomial.coeff remainder2Coefficient2 12 = -44370403879186022184327
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_13 :
Polynomial.coeff remainder2Coefficient2 13 = 1038308847642591349427606
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_14 :
Polynomial.coeff remainder2Coefficient2 14 = 15998025457352783001220174
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_15 :
Polynomial.coeff remainder2Coefficient2 15 = -100565161540304756843088699
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_16 :
Polynomial.coeff remainder2Coefficient2 16 = -3838383077263422427097601024
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_17 :
Polynomial.coeff remainder2Coefficient2 17 = 10609409481487786287893449330
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_18 :
Polynomial.coeff remainder2Coefficient2 18 = 357912551995618314750281664824
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_19 :
Polynomial.coeff remainder2Coefficient2 19 = 928321599646397579187788779389
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_20 :
Polynomial.coeff remainder2Coefficient2 20 = -39010431621283220839231554468746
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_21 :
Polynomial.coeff remainder2Coefficient2 21 = -44113655110558033415564496971977
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_22 :
Polynomial.coeff remainder2Coefficient2 22 = 1998385302311546909527456011604480
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_23 :
Polynomial.coeff remainder2Coefficient2 23 = 7168047773872259887036010762730379
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_24 :
Polynomial.coeff remainder2Coefficient2 24 = -120219085005287976859016785080841404
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_25 :
Polynomial.coeff remainder2Coefficient2 25 = -272065361572137179529501208609249331
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_26 :
Polynomial.coeff remainder2Coefficient2 26 = 4809921067274839057864714570624963506
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_27 :
Polynomial.coeff remainder2Coefficient2 27 = 10977775776437172250288677711940278903
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_28 :
Polynomial.coeff remainder2Coefficient2 28 = -182892475529011048951487063637634553314
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_29 :
Polynomial.coeff remainder2Coefficient2 29 = -225651086921399577429239301721385471573
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_30 :
Polynomial.coeff remainder2Coefficient2 30 = 5594738952022077263553172674468414526285
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_31 :
Polynomial.coeff remainder2Coefficient2 31 = 1277630644490436651545302781724918563567
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_32 :
Polynomial.coeff remainder2Coefficient2 32 = -143971490148075201103356211213635554595906
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_33 :
Polynomial.coeff remainder2Coefficient2 33 = 141516256736775030680012138512082832312497
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_34 :
Polynomial.coeff remainder2Coefficient2 34 = 2934737362609721978989121199535211802940135
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_35 :
Polynomial.coeff remainder2Coefficient2 35 = -6992542448096665025565927640957960661978556
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_36 :
Polynomial.coeff remainder2Coefficient2 36 = -44072802935403696670155203768536842732121167
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_37 :
Polynomial.coeff remainder2Coefficient2 37 = 192741970197878757144563539088813369313968168
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_38 :
Polynomial.coeff remainder2Coefficient2 38 = 378998640258419723632070884120051362325277745
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_39 :
Polynomial.coeff remainder2Coefficient2 39 = -3579749608066737552394659611752271346887827974
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_40 :
Polynomial.coeff remainder2Coefficient2 40 = 1470706088616565346583942807448141460401188945
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_41 :
Polynomial.coeff remainder2Coefficient2 41 = 43883561445677244621270552241179903867916776540
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_42 :
Polynomial.coeff remainder2Coefficient2 42 = -107804191716905270671379301045017348646752444777
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_43 :
Polynomial.coeff remainder2Coefficient2 43 = -272368018417738155386465688834341829656727182307
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_44 :
Polynomial.coeff remainder2Coefficient2 44 = 1744552560514683292522850401633464103487164073490
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_45 :
Polynomial.coeff remainder2Coefficient2 45 = -1198159366924519362911282886347893563461138591211
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_46 :
Polynomial.coeff remainder2Coefficient2 46 = -13522380586587904137675170102049123376972642598255
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_47 :
Polynomial.coeff remainder2Coefficient2 47 = 42291960744969586573911774792841144736581005599284
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_48 :
Polynomial.coeff remainder2Coefficient2 48 = 8750926432463064317977843549196908261718546612891
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_49 :
Polynomial.coeff remainder2Coefficient2 49 = -344058533433772745293613097758239454232314009302575
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_50 :
Polynomial.coeff remainder2Coefficient2 50 = 793414301057079276958444135752994668657004652391566
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_51 :
Polynomial.coeff remainder2Coefficient2 51 = 286105840767256631723520274510890065023572362924729
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_52 :
Polynomial.coeff remainder2Coefficient2 52 = -5647611372358746763496541225068797862088473076319126
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_53 :
Polynomial.coeff remainder2Coefficient2 53 = 12919974019283142044299163386735064499292846351870647
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_54 :
Polynomial.coeff remainder2Coefficient2 54 = -3359642529712813552784602758031437157300360833007150
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A2_coeff_55 :
Polynomial.coeff remainder2Coefficient2 55 = -55264383613182431624803628335662273260436933996676443