Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupA3High

Recurrence 2 lookup certificate: A3 source coefficients, high 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.recurrence2A3_coeff_54 :
Polynomial.coeff remainder2Coefficient3 54 = 6528414277076057223769874840538652984052724118938262
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_55 :
Polynomial.coeff remainder2Coefficient3 55 = -12769021039988110628010405073972212117566839200854058
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_56 :
Polynomial.coeff remainder2Coefficient3 56 = 6710727525884742257164468557671762523932017203572218
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_57 :
Polynomial.coeff remainder2Coefficient3 57 = 30175747630459063031095711692767385422885342369621140
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_58 :
Polynomial.coeff remainder2Coefficient3 58 = -100248785764461368577107612512630767697897557742058640
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_59 :
Polynomial.coeff remainder2Coefficient3 59 = 162413156184027760713153186952743394367606631091432890
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_60 :
Polynomial.coeff remainder2Coefficient3 60 = -133590640082852617628624946301179103567220806508211600
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_61 :
Polynomial.coeff remainder2Coefficient3 61 = -55673262195842482703446022644446419291453166881173181
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_62 :
Polynomial.coeff remainder2Coefficient3 62 = 379361394804245037899965367824579083277847555619049027
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_63 :
Polynomial.coeff remainder2Coefficient3 63 = -686623311988715580285156571990752862180113043652979055
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_64 :
Polynomial.coeff remainder2Coefficient3 64 = 780972389252802949479690830881112451831860821719407528
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_65 :
Polynomial.coeff remainder2Coefficient3 65 = -565007106884647134434957499720230902141386345251579967
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_66 :
Polynomial.coeff remainder2Coefficient3 66 = 128285820961084225455490897714271781640264571770333288
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_67 :
Polynomial.coeff remainder2Coefficient3 67 = 307039001341708743292866630993907577620549133022106270
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_68 :
Polynomial.coeff remainder2Coefficient3 68 = -540472668043227544901564871029126882753385776539977491
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_69 :
Polynomial.coeff remainder2Coefficient3 69 = 516912697505258064725658443400572658051263163444854079
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_70 :
Polynomial.coeff remainder2Coefficient3 70 = -328582041573588224747298523953274430364919446483101658
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_71 :
Polynomial.coeff remainder2Coefficient3 71 = 119023298000490316931922150843289794983990553606648252
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_72 :
Polynomial.coeff remainder2Coefficient3 72 = 15764024619483439326093495308983445835761470859004150
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_73 :
Polynomial.coeff remainder2Coefficient3 73 = -60110943040894486198742741258328108783002759133650284
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_74 :
Polynomial.coeff remainder2Coefficient3 74 = 49212362666451763724724451742959451554558004333520726
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_75 :
Polynomial.coeff remainder2Coefficient3 75 = -23922300774913644624801096610556066181099864130444627
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_76 :
Polynomial.coeff remainder2Coefficient3 76 = 6148808417178414816994974845600455137044668236983729
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_77 :
Polynomial.coeff remainder2Coefficient3 77 = 830245972089719503095319268574266026478437444563336
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_78 :
Polynomial.coeff remainder2Coefficient3 78 = -1678360061583332653851771133247003577297695703634195
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_79 :
Polynomial.coeff remainder2Coefficient3 79 = 839159059157663174522296883868759738485717148535281
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_80 :
Polynomial.coeff remainder2Coefficient3 80 = -203349744888727517211709358660650029083115727665296
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_81 :
Polynomial.coeff remainder2Coefficient3 81 = -7140027856396353107780592363086475355669233733768
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_82 :
Polynomial.coeff remainder2Coefficient3 82 = 24851537352247083860767221184131530805323720822241
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_83 :
Polynomial.coeff remainder2Coefficient3 83 = -8747969004708684199605992861862970138447612526507
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_84 :
Polynomial.coeff remainder2Coefficient3 84 = 926599088367198945920418698771499128199733035260
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_85 :
Polynomial.coeff remainder2Coefficient3 85 = 336721822876300553696392160754947126360892447982
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_86 :
Polynomial.coeff remainder2Coefficient3 86 = -141326484419013466682318415823838359102645815341
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_87 :
Polynomial.coeff remainder2Coefficient3 87 = 13779964434773641076795436769502131326743233685
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_88 :
Polynomial.coeff remainder2Coefficient3 88 = 3490413213896667872921484488540653929129509249
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_89 :
Polynomial.coeff remainder2Coefficient3 89 = -995591552697449920616804017169423479210992753
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_90 :
Polynomial.coeff remainder2Coefficient3 90 = 11753883545940184043689853651614097074310681
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_91 :
Polynomial.coeff remainder2Coefficient3 91 = 22019885059282066352198371338729758987417033
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_92 :
Polynomial.coeff remainder2Coefficient3 92 = -1241360921762821318591252624819852067585689
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_93 :
Polynomial.coeff remainder2Coefficient3 93 = -292540411516541400976854683925085011124788
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_94 :
Polynomial.coeff remainder2Coefficient3 94 = 8991237744046789505603825182565214706852
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_95 :
Polynomial.coeff remainder2Coefficient3 95 = 2730140599159216551065616103945835624732
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_96 :
Polynomial.coeff remainder2Coefficient3 96 = 144957512445012928435501885822570771046
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_97 :
Polynomial.coeff remainder2Coefficient3 97 = 3415621928189986890998128674465258779
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_98 :
Polynomial.coeff remainder2Coefficient3 98 = 39742507950836905779404512839757906
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_99 :
Polynomial.coeff remainder2Coefficient3 99 = 222522177019934397987749429416808
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_100 :
Polynomial.coeff remainder2Coefficient3 100 = 482011122008097505290949836698
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_101 :
Polynomial.coeff remainder2Coefficient3 101 = -258756034495996674981616083
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_102 :
Polynomial.coeff remainder2Coefficient3 102 = -2132096922036802698650356
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_103 :
Polynomial.coeff remainder2Coefficient3 103 = -1765206011740968795608
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_104 :
Polynomial.coeff remainder2Coefficient3 104 = -267857578388844983
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_105 :
Polynomial.coeff remainder2Coefficient3 105 = -3772299553634
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A3_coeff_106 :
Polynomial.coeff remainder2Coefficient3 106 = -794294