Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupA1High

Recurrence 4 lookup certificate: A1 source coefficients, high half #

This is a checked coefficient-lookup shard for the fourth pseudo-division recurrence in the order-seven certificate.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_96 :
Polynomial.coeff remainder4Coefficient1 96 = 7475177460798968777583282313269 * 10 ^ 70 + 8066718384764117436995108586200250777778185745543772160125771622169361
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_97 :
Polynomial.coeff remainder4Coefficient1 97 = -(7482451797703971722366361355000 * 10 ^ 70 + 5270950568146464834893398230570805357347094986005454742401472601980335)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_98 :
Polynomial.coeff remainder4Coefficient1 98 = 7243614148603187414932177774770 * 10 ^ 70 + 3511422848650818334217699093914898487931426192418271730445719627103285
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_99 :
Polynomial.coeff remainder4Coefficient1 99 = -(6781690581702507758067397737376 * 10 ^ 70 + 4734538555728387632604968013737638873832540799891614027876921972604357)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_100 :
Polynomial.coeff remainder4Coefficient1 100 = 6140017427523117285803397662541 * 10 ^ 70 + 8448716634365636828083858587388839773345016179486663380073920719746749
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_101 :
Polynomial.coeff remainder4Coefficient1 101 = -(5375554210578042600925739350267 * 10 ^ 70 + 9898302329500112196149001603079423243961347340468666007474433875768123)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_102 :
Polynomial.coeff remainder4Coefficient1 102 = 4550585390331270997222547994034 * 10 ^ 70 + 7099109700348463158141813057573975091384837127745680877471881247431711
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_103 :
Polynomial.coeff remainder4Coefficient1 103 = -(3724477496928350026231910909241 * 10 ^ 70 + 666312848718010993686080104049483661578954328757820846239994666186564)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_104 :
Polynomial.coeff remainder4Coefficient1 104 = 2946975260902021780599264580861 * 10 ^ 70 + 1078341050731413751121957123404828488189389253902530281997849497641148
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_105 :
Polynomial.coeff remainder4Coefficient1 105 = -(2254005457602165681829979393411 * 10 ^ 70 + 3720179010930614624379613894284279184166161606979984431402882679108241)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_106 :
Polynomial.coeff remainder4Coefficient1 106 = 1666289279034895075944571826565 * 10 ^ 70 + 2819970357199525437735572315291797311266751764408473362168504863481880
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_107 :
Polynomial.coeff remainder4Coefficient1 107 = -(1190440923042996367756715697392 * 10 ^ 70 + 986070029279986604449811523739018628786974308457964549438364727944960)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_108 :
Polynomial.coeff remainder4Coefficient1 108 = 821803419234149993591490999051 * 10 ^ 70 + 426746426653445035338274175813464482599086124019518304690865767842911
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_109 :
Polynomial.coeff remainder4Coefficient1 109 = -(548109351697741238166283084386 * 10 ^ 70 + 9470647752374042594647276219032955259228712677159647942417641353568025)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_110 :
Polynomial.coeff remainder4Coefficient1 110 = 353133203097499911730942991457 * 10 ^ 70 + 4129773425014224605868514857643823042759024778782340646601505980952053
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_111 :
Polynomial.coeff remainder4Coefficient1 111 = -(219741463674264861095895267338 * 10 ^ 70 + 1610206486011710546496615755547375075949559716134298998318744939351872)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_112 :
Polynomial.coeff remainder4Coefficient1 112 = 132043159619196054915996181816 * 10 ^ 70 + 4065850479252478099559657915467719041118028544752132163508886933676552
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_113 :
Polynomial.coeff remainder4Coefficient1 113 = -(76608756571631665694525888022 * 10 ^ 70 + 2897239801711860293432438077723790361816585229100664145171205528497700)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_114 :
Polynomial.coeff remainder4Coefficient1 114 = 42907145090774203459211081320 * 10 ^ 70 + 9033435008776763749977098687326871981357776769175542755505404326475257
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_115 :
Polynomial.coeff remainder4Coefficient1 115 = -(23195510046346500749846600983 * 10 ^ 70 + 9129085229474743802767995792118189104328418741467371543881209847745440)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_116 :
Polynomial.coeff remainder4Coefficient1 116 = 12101586850188405689909264983 * 10 ^ 70 + 3770074072198420270202571350979399552965201310838640764313338784743622
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_117 :
Polynomial.coeff remainder4Coefficient1 117 = -(6092470096139417495259241813 * 10 ^ 70 + 2783672712156360001938658891334201444099069419098159487678889689955344)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_118 :
Polynomial.coeff remainder4Coefficient1 118 = 2959449843423416825051695423 * 10 ^ 70 + 8491588558504025273457401767263972416884924298417024656667405485064981
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_119 :
Polynomial.coeff remainder4Coefficient1 119 = -(1386897056881075844868201486 * 10 ^ 70 + 3842343684781607512394527258519171523025860585277581178356722717009967)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_120 :
Polynomial.coeff remainder4Coefficient1 120 = 626922430927956722151146983 * 10 ^ 70 + 3113294234255109841984963546344708080215270685116192794622704739178119
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_121 :
Polynomial.coeff remainder4Coefficient1 121 = -(273252287319724008947825275 * 10 ^ 70 + 4931060169052733837388067309950901633713623800736332773038631348386682)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_122 :
Polynomial.coeff remainder4Coefficient1 122 = 114755749683313425480081954 * 10 ^ 70 + 88118055028321473487985309150451780724302785413977701856614315519369
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_123 :
Polynomial.coeff remainder4Coefficient1 123 = -(46367610398937840092910333 * 10 ^ 70 + 6364047477904953416282745852485488582340262490334116521024041391105763)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_124 :
Polynomial.coeff remainder4Coefficient1 124 = 17976433179167116345358965 * 10 ^ 70 + 5037332022733662693544706142939885054935077266689038261012468015078775
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_125 :
Polynomial.coeff remainder4Coefficient1 125 = -(6654656968012661083360849 * 10 ^ 70 + 8242358489154342840707285094501257495302513459696481323433816564720037)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_126 :
Polynomial.coeff remainder4Coefficient1 126 = 2332292100441059445809149 * 10 ^ 70 + 5003694967883150483004052753840545330304835945050858207941675078892431
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_127 :
Polynomial.coeff remainder4Coefficient1 127 = -(762355627509772260392545 * 10 ^ 70 + 9129020044352695264971612417428595617076454378843220177976414898731665)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_128 :
Polynomial.coeff remainder4Coefficient1 128 = 225971502744677180661085 * 10 ^ 70 + 5525852260351888724534114013330585989177653772033832694350594392677069
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_129 :
Polynomial.coeff remainder4Coefficient1 129 = -(57137577110467956671822 * 10 ^ 70 + 1248603944744907758820562756995981522247446060216254197850658579152982)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_130 :
Polynomial.coeff remainder4Coefficient1 130 = 10193177452723550279055 * 10 ^ 70 + 9045052741753946736055387301144344446581502262552308079366786876620792
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_131 :
Polynomial.coeff remainder4Coefficient1 131 = 163717474058853935565 * 10 ^ 70 + 2930890359741328010950289532536588709928185436563016394233749140495239
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_132 :
Polynomial.coeff remainder4Coefficient1 132 = -(1222419576429299706640 * 10 ^ 70 + 3612371111511094629799379338206645615436927272493208661872931051962118)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_133 :
Polynomial.coeff remainder4Coefficient1 133 = 676784738286958581649 * 10 ^ 70 + 2035317322802052752325313727035170951525340107950187505688299383718608
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_134 :
Polynomial.coeff remainder4Coefficient1 134 = -(228583884729503516716 * 10 ^ 70 + 8551452840567247344059108348509846028997973496103964767947358443652028)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_135 :
Polynomial.coeff remainder4Coefficient1 135 = 32772791354265001697 * 10 ^ 70 + 8449572806391556799593543301072963707228764297186407603064753050221904
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_136 :
Polynomial.coeff remainder4Coefficient1 136 = 21914082473784597656 * 10 ^ 70 + 1004735794613487125993345078472062497958015992851956245846972403780009
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_137 :
Polynomial.coeff remainder4Coefficient1 137 = -(24356917850632510890 * 10 ^ 70 + 8872980824934004892937432554154653036098288340067886403395805419004235)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_138 :
Polynomial.coeff remainder4Coefficient1 138 = 15180916494215646783 * 10 ^ 70 + 4674940901122527131805783850359230719647754674294673227354298758172644
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_139 :
Polynomial.coeff remainder4Coefficient1 139 = -(7354309902376419625 * 10 ^ 70 + 6104538642216805174855224425481376040814389597686109518541596779949748)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_140 :
Polynomial.coeff remainder4Coefficient1 140 = 2904802332343163224 * 10 ^ 70 + 5724100789233402272077878879282076021101711907007051183280621146311499
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_141 :
Polynomial.coeff remainder4Coefficient1 141 = -(882049484753851365 * 10 ^ 70 + 7771778701144288519400850385896283348493685271198884246794532396310447)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_142 :
Polynomial.coeff remainder4Coefficient1 142 = 136202684006136914 * 10 ^ 70 + 5950761817927908891475153236522072081752557034231226703980108451173122
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_143 :
Polynomial.coeff remainder4Coefficient1 143 = 63833987296685336 * 10 ^ 70 + 9927896457014352553163178843160351426361393905523467070925818387006941
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_144 :
Polynomial.coeff remainder4Coefficient1 144 = -(77706310746925818 * 10 ^ 70 + 9403633184424262988037681780551087286842522895153329351979884176406813)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_145 :
Polynomial.coeff remainder4Coefficient1 145 = 49827838581298692 * 10 ^ 70 + 6820615413253005385631516989043117066448838542126675817693829149112231
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_146 :
Polynomial.coeff remainder4Coefficient1 146 = -(24999987339023179 * 10 ^ 70 + 2423386418842515798974386550642008525120457015155510342182912110759533)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_147 :
Polynomial.coeff remainder4Coefficient1 147 = 10637997518973879 * 10 ^ 70 + 9544210930931038741759333294278856596471174565216928960131597073670883
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_148 :
Polynomial.coeff remainder4Coefficient1 148 = -(3930940963288629 * 10 ^ 70 + 6315553273394981414344342170176498584790782399370749008786690806299115)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_149 :
Polynomial.coeff remainder4Coefficient1 149 = 1262336562008912 * 10 ^ 70 + 5683846670951538592040879112609354557220521235993047661661001967014925
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_150 :
Polynomial.coeff remainder4Coefficient1 150 = -(346002961033324 * 10 ^ 70 + 9623280924069551168423292386399703000518454170479798932605259239853739)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_151 :
Polynomial.coeff remainder4Coefficient1 151 = 76940976875028 * 10 ^ 70 + 1250381447313599468863811659386560414723345165060194381638294428035178
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_152 :
Polynomial.coeff remainder4Coefficient1 152 = -(11798116595990 * 10 ^ 70 + 1266487681441359892239350143809719252996705777684469693086800698811714)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_153 :
Polynomial.coeff remainder4Coefficient1 153 = 134764028710 * 10 ^ 70 + 3749399824005250007318494405695332273715697464435832669940297220384767
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_154 :
Polynomial.coeff remainder4Coefficient1 154 = 702660606139 * 10 ^ 70 + 8810161088365813323921298661676538910394339064465744026681226658424695
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_155 :
Polynomial.coeff remainder4Coefficient1 155 = -(302289043288 * 10 ^ 70 + 9290464488781490312876576753564812781320527228443094476621409514519136)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_156 :
Polynomial.coeff remainder4Coefficient1 156 = 81076818564 * 10 ^ 70 + 4552835858960223320939486592500333487733099804370226498268268865857444
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_157 :
Polynomial.coeff remainder4Coefficient1 157 = -(15064863955 * 10 ^ 70 + 3542516191515398184950568326064434999459840987436394851510740073126693)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_158 :
Polynomial.coeff remainder4Coefficient1 158 = 1577033140 * 10 ^ 70 + 3575342430895437961905750881845820513057422334386125077139738584521346
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_159 :
Polynomial.coeff remainder4Coefficient1 159 = 103143849 * 10 ^ 70 + 9419190608672874908783382977396589869424766742615775100022364462177475
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_160 :
Polynomial.coeff remainder4Coefficient1 160 = -(88848845 * 10 ^ 70 + 3598737416694792367378225998460057463258942004187451125805195248369565)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_161 :
Polynomial.coeff remainder4Coefficient1 161 = 21270475 * 10 ^ 70 + 6537571917646621422696742507746692908399014372752078350832949817247759
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_162 :
Polynomial.coeff remainder4Coefficient1 162 = -(2804518 * 10 ^ 70 + 3635839490541588126639601185006555879722503605206376046986677170440905)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A1_coeff_165 :
Polynomial.coeff remainder4Coefficient1 165 = -(11801 * 10 ^ 70 + 4729953012360969545582488938406817229717684913149581805680487802635014)