Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupA0Low

Recurrence 2 lookup certificate: A0 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.recurrence2A0_coeff_0 :
Polynomial.coeff remainder2Coefficient0 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_1 :
Polynomial.coeff remainder2Coefficient0 1 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_2 :
Polynomial.coeff remainder2Coefficient0 2 = 1
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_3 :
Polynomial.coeff remainder2Coefficient0 3 = 21998
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_4 :
Polynomial.coeff remainder2Coefficient0 4 = 1213258
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_5 :
Polynomial.coeff remainder2Coefficient0 5 = -6591719746
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_6 :
Polynomial.coeff remainder2Coefficient0 6 = 887174420015
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_7 :
Polynomial.coeff remainder2Coefficient0 7 = 10898850087779
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_8 :
Polynomial.coeff remainder2Coefficient0 8 = -4242577921555076
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_9 :
Polynomial.coeff remainder2Coefficient0 9 = -9044841330557190
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_10 :
Polynomial.coeff remainder2Coefficient0 10 = 5905879565633563356
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_11 :
Polynomial.coeff remainder2Coefficient0 11 = 73367409398595165996
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_12 :
Polynomial.coeff remainder2Coefficient0 12 = -3131219520021488355261
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_13 :
Polynomial.coeff remainder2Coefficient0 13 = -66505908255265167228909
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_14 :
Polynomial.coeff remainder2Coefficient0 14 = 409155522983929358223454
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_15 :
Polynomial.coeff remainder2Coefficient0 15 = 22027542795128115872321226
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_16 :
Polynomial.coeff remainder2Coefficient0 16 = 76735418560623238749227979
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_17 :
Polynomial.coeff remainder2Coefficient0 17 = -3234018323272692008644959524
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_18 :
Polynomial.coeff remainder2Coefficient0 18 = -29738389409425638678174724443
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_19 :
Polynomial.coeff remainder2Coefficient0 19 = 253887039826360477352885637974
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_20 :
Polynomial.coeff remainder2Coefficient0 20 = 3839461295707575052402511711145
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_21 :
Polynomial.coeff remainder2Coefficient0 21 = -7632953412497286154928754530167
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_22 :
Polynomial.coeff remainder2Coefficient0 22 = -325902109613993235482591511158062
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_23 :
Polynomial.coeff remainder2Coefficient0 23 = -54189002951574352392486001446389
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_24 :
Polynomial.coeff remainder2Coefficient0 24 = 17939832588070721406987746062937250
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_25 :
Polynomial.coeff remainder2Coefficient0 25 = 31826313445941491054485986255887620
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_26 :
Polynomial.coeff remainder2Coefficient0 26 = -849488679231132760490374031074814762
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_27 :
Polynomial.coeff remainder2Coefficient0 27 = -1614355931044266796217772307414613716
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_28 :
Polynomial.coeff remainder2Coefficient0 28 = 31358151232828134232489089258528740581
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_29 :
Polynomial.coeff remainder2Coefficient0 29 = 59173772590237271321614902242554864604
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_30 :
Polynomial.coeff remainder2Coefficient0 30 = -1037909449069702050995790634079279527234
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_31 :
Polynomial.coeff remainder2Coefficient0 31 = -1165280355746439384243786350455420790049
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_32 :
Polynomial.coeff remainder2Coefficient0 32 = 28927249338570910072158119743920309724861
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_33 :
Polynomial.coeff remainder2Coefficient0 33 = 3724415618239167221623117838218836606730
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_34 :
Polynomial.coeff remainder2Coefficient0 34 = -681578237840065642926261228656071824770362
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_35 :
Polynomial.coeff remainder2Coefficient0 35 = 762752762879364689572744288733998737444098
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_36 :
Polynomial.coeff remainder2Coefficient0 36 = 12747758848377365623179496199857217975063094
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_37 :
Polynomial.coeff remainder2Coefficient0 37 = -33644919694007791905306165608311761387256527
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_38 :
Polynomial.coeff remainder2Coefficient0 38 = -170616046135731321807523659719437449607831382
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_39 :
Polynomial.coeff remainder2Coefficient0 39 = 854731750744759183117612048451503577686718350
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_40 :
Polynomial.coeff remainder2Coefficient0 40 = 1070589103141380188990437600705938082237411849
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_41 :
Polynomial.coeff remainder2Coefficient0 41 = -14533737069505132262481138493185774319227901666
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_42 :
Polynomial.coeff remainder2Coefficient0 42 = 14847492001852093904509154446647689144549047900
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_43 :
Polynomial.coeff remainder2Coefficient0 43 = 155606299034522954166844058198548068896279977537
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_44 :
Polynomial.coeff remainder2Coefficient0 44 = -519630700961647778633579607877224146206648309539
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_45 :
Polynomial.coeff remainder2Coefficient0 45 = -598801835612111105880235198090447628712531519493
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_46 :
Polynomial.coeff remainder2Coefficient0 46 = 6947902940277472273331017092804828544810974028139
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_47 :
Polynomial.coeff remainder2Coefficient0 47 = -10475530471061913847079100899254638337734396287104
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_48 :
Polynomial.coeff remainder2Coefficient0 48 = -40332554873310579622123872668669900409407948080662
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_49 :
Polynomial.coeff remainder2Coefficient0 49 = 193107590045649299339279328984668292960892819799483
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_50 :
Polynomial.coeff remainder2Coefficient0 50 = -149432665535261992857347330551770721950842375691980
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_51 :
Polynomial.coeff remainder2Coefficient0 51 = -1133497054982079041065679089970365931806088756989147
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_52 :
Polynomial.coeff remainder2Coefficient0 52 = 4040747699608870687257985013647732806121074286902738
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_53 :
Polynomial.coeff remainder2Coefficient0 53 = -2785848571080064457962537035628974255157624433659535
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_54 :
Polynomial.coeff remainder2Coefficient0 54 = -18687086537014865119121801645888755694124474167125176
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_55 :
Polynomial.coeff remainder2Coefficient0 55 = 66681838947911016521021237852219792660730576150126032
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_56 :
Polynomial.coeff remainder2Coefficient0 56 = -74259866442592643309907716195443028789570438134352762
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_57 :
Polynomial.coeff remainder2Coefficient0 57 = -147265800657316553789244740368621751889157008294390057
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_58 :
Polynomial.coeff remainder2Coefficient0 58 = 755349943097198560274645640023835200357276309089105499
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A0_coeff_59 :
Polynomial.coeff remainder2Coefficient0 59 = -1379867726824908573819612208907630171932514084636054614