Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupC1High.Coefficients119To142

Recurrence 2 lookup certificate: C1 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.recurrence2C1_coeff_119 :
Polynomial.coeff remainder4Coefficient1 119 = -(1386897056881075844868201486 * 10 ^ 70 + 3842343684781607512394527258519171523025860585277581178356722717009967)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_120 :
Polynomial.coeff remainder4Coefficient1 120 = 626922430927956722151146983 * 10 ^ 70 + 3113294234255109841984963546344708080215270685116192794622704739178119
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_121 :
Polynomial.coeff remainder4Coefficient1 121 = -(273252287319724008947825275 * 10 ^ 70 + 4931060169052733837388067309950901633713623800736332773038631348386682)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_122 :
Polynomial.coeff remainder4Coefficient1 122 = 114755749683313425480081954 * 10 ^ 70 + 88118055028321473487985309150451780724302785413977701856614315519369
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_123 :
Polynomial.coeff remainder4Coefficient1 123 = -(46367610398937840092910333 * 10 ^ 70 + 6364047477904953416282745852485488582340262490334116521024041391105763)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_124 :
Polynomial.coeff remainder4Coefficient1 124 = 17976433179167116345358965 * 10 ^ 70 + 5037332022733662693544706142939885054935077266689038261012468015078775
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_125 :
Polynomial.coeff remainder4Coefficient1 125 = -(6654656968012661083360849 * 10 ^ 70 + 8242358489154342840707285094501257495302513459696481323433816564720037)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_126 :
Polynomial.coeff remainder4Coefficient1 126 = 2332292100441059445809149 * 10 ^ 70 + 5003694967883150483004052753840545330304835945050858207941675078892431
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_127 :
Polynomial.coeff remainder4Coefficient1 127 = -(762355627509772260392545 * 10 ^ 70 + 9129020044352695264971612417428595617076454378843220177976414898731665)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_128 :
Polynomial.coeff remainder4Coefficient1 128 = 225971502744677180661085 * 10 ^ 70 + 5525852260351888724534114013330585989177653772033832694350594392677069
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_129 :
Polynomial.coeff remainder4Coefficient1 129 = -(57137577110467956671822 * 10 ^ 70 + 1248603944744907758820562756995981522247446060216254197850658579152982)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_130 :
Polynomial.coeff remainder4Coefficient1 130 = 10193177452723550279055 * 10 ^ 70 + 9045052741753946736055387301144344446581502262552308079366786876620792
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_131 :
Polynomial.coeff remainder4Coefficient1 131 = 163717474058853935565 * 10 ^ 70 + 2930890359741328010950289532536588709928185436563016394233749140495239
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_132 :
Polynomial.coeff remainder4Coefficient1 132 = -(1222419576429299706640 * 10 ^ 70 + 3612371111511094629799379338206645615436927272493208661872931051962118)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_133 :
Polynomial.coeff remainder4Coefficient1 133 = 676784738286958581649 * 10 ^ 70 + 2035317322802052752325313727035170951525340107950187505688299383718608
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_134 :
Polynomial.coeff remainder4Coefficient1 134 = -(228583884729503516716 * 10 ^ 70 + 8551452840567247344059108348509846028997973496103964767947358443652028)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_135 :
Polynomial.coeff remainder4Coefficient1 135 = 32772791354265001697 * 10 ^ 70 + 8449572806391556799593543301072963707228764297186407603064753050221904
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_136 :
Polynomial.coeff remainder4Coefficient1 136 = 21914082473784597656 * 10 ^ 70 + 1004735794613487125993345078472062497958015992851956245846972403780009
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_137 :
Polynomial.coeff remainder4Coefficient1 137 = -(24356917850632510890 * 10 ^ 70 + 8872980824934004892937432554154653036098288340067886403395805419004235)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_138 :
Polynomial.coeff remainder4Coefficient1 138 = 15180916494215646783 * 10 ^ 70 + 4674940901122527131805783850359230719647754674294673227354298758172644
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_139 :
Polynomial.coeff remainder4Coefficient1 139 = -(7354309902376419625 * 10 ^ 70 + 6104538642216805174855224425481376040814389597686109518541596779949748)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_140 :
Polynomial.coeff remainder4Coefficient1 140 = 2904802332343163224 * 10 ^ 70 + 5724100789233402272077878879282076021101711907007051183280621146311499
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_141 :
Polynomial.coeff remainder4Coefficient1 141 = -(882049484753851365 * 10 ^ 70 + 7771778701144288519400850385896283348493685271198884246794532396310447)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_142 :
Polynomial.coeff remainder4Coefficient1 142 = 136202684006136914 * 10 ^ 70 + 5950761817927908891475153236522072081752557034231226703980108451173122