Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupA3High

Recurrence 4 lookup certificate: A3 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.recurrence4A3_coeff_92 :
Polynomial.coeff remainder4Coefficient3 92 = 176473385274789241837392718516 * 10 ^ 70 + 982747015888460662198709227079720842388611628989672141453076644495590
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_93 :
Polynomial.coeff remainder4Coefficient3 93 = -(184267523154347832662993382789 * 10 ^ 70 + 2331600543518685231226110809092316041540282752680344181264185937438711)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_94 :
Polynomial.coeff remainder4Coefficient3 94 = 185947126009607934978739452010 * 10 ^ 70 + 4925149782700238059717281009253639961586281559191142076347303417279029
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_95 :
Polynomial.coeff remainder4Coefficient3 95 = -(181338781754327948328037886149 * 10 ^ 70 + 5910969449061829548911610912009345890801384750740394232244220790305342)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_96 :
Polynomial.coeff remainder4Coefficient3 96 = 170898026186980064134473531030 * 10 ^ 70 + 8792652215120492987053762497236748463473918861393220405508017747355876
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_97 :
Polynomial.coeff remainder4Coefficient3 97 = -(155635345667211120426214160261 * 10 ^ 70 + 2810881101969296649776030742297880857785399860292294493559867890291365)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_98 :
Polynomial.coeff remainder4Coefficient3 98 = 136955377753757312870694983358 * 10 ^ 70 + 3184668269630637911157150809910172656821222705971535041015937089604267
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_99 :
Polynomial.coeff remainder4Coefficient3 99 = -(116444656727476734612279126401 * 10 ^ 70 + 7339854213209270800270590025416037055438399201236525558883619271536937)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_100 :
Polynomial.coeff remainder4Coefficient3 100 = 95652144093327838293790355899 * 10 ^ 70 + 9401742732288687997964431433478088083255333089172882998097381524861447
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_101 :
Polynomial.coeff remainder4Coefficient3 101 = -(75903996333230026382439846932 * 10 ^ 70 + 7722766929827925629698390945089800158299573819753617593331621322067580)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_102 :
Polynomial.coeff remainder4Coefficient3 102 = 58181445440687775046921112637 * 10 ^ 70 + 2312228514222012036448111881122888356968009096274469224877111716449663
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_103 :
Polynomial.coeff remainder4Coefficient3 103 = -(43072930026168003558941124228 * 10 ^ 70 + 2572521572083738592604777143108468777170791672659615118559872265113791)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_104 :
Polynomial.coeff remainder4Coefficient3 104 = 30794232145005058207521234329 * 10 ^ 70 + 5023654388748488025754663300088680602785710391526345509263212383916376
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_105 :
Polynomial.coeff remainder4Coefficient3 105 = -(21257844054666340032918890399 * 10 ^ 70 + 6651951419112378465454427532977997962162412668300190128561804392002306)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_106 :
Polynomial.coeff remainder4Coefficient3 106 = 14167344151357462258553470309 * 10 ^ 70 + 362545497692308724895744414032736416193683922164774746612234423585873
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_107 :
Polynomial.coeff remainder4Coefficient3 107 = -(9113939393630718930392049703 * 10 ^ 70 + 8853651992130687155879859103889800506596345445567843981944630977269690)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_108 :
Polynomial.coeff remainder4Coefficient3 108 = 5658427511013853518622954762 * 10 ^ 70 + 6211089361166854968938163810626406852108212249596016989233906078892612
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_109 :
Polynomial.coeff remainder4Coefficient3 109 = -(3389806746333968469680039414 * 10 ^ 70 + 6573658019918964381953355396073497953039215996244393540520294236026118)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_110 :
Polynomial.coeff remainder4Coefficient3 110 = 1959093798977341411901076074 * 10 ^ 70 + 8535189002444420553780638678155087392621845336597690492881284736605936
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_111 :
Polynomial.coeff remainder4Coefficient3 111 = -(1092048120510662783206136156 * 10 ^ 70 + 676051511299682632899560986633923169809086424964405012638370227444059)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_112 :
Polynomial.coeff remainder4Coefficient3 112 = 586993116935681584840736220 * 10 ^ 70 + 1919350713865214816830779311659945179831847552187491410601345271337213
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_113 :
Polynomial.coeff remainder4Coefficient3 113 = -(304172808945607598683979734 * 10 ^ 70 + 4499612882974177869325658837674013608837094572823587644737759559765755)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_114 :
Polynomial.coeff remainder4Coefficient3 114 = 151910704842196142209882497 * 10 ^ 70 + 2382999243094599440090491518910907156231194781116445432241807824877411
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_115 :
Polynomial.coeff remainder4Coefficient3 115 = -(73099595631230280325206112 * 10 ^ 70 + 70793112430484702325413531155248649221727297149062161532066504098032)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_116 :
Polynomial.coeff remainder4Coefficient3 116 = 33882332954984642778561477 * 10 ^ 70 + 3820804768531740287711515571794132771153365533156929607882417314586377
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_117 :
Polynomial.coeff remainder4Coefficient3 117 = -(15122902149330239841165866 * 10 ^ 70 + 8128075030377744965170374800242649512606742882149195720968994942824104)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_118 :
Polynomial.coeff remainder4Coefficient3 118 = 6497966021375530904313245 * 10 ^ 70 + 240672650550574707536452882422460639368321470950190129782641237496299
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_119 :
Polynomial.coeff remainder4Coefficient3 119 = -(2687158721072196903153304 * 10 ^ 70 + 9479749620208473971994248542300021158436520054416376118405511770926595)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_120 :
Polynomial.coeff remainder4Coefficient3 120 = 1069323165678915503923484 * 10 ^ 70 + 4433052426485068593826311228692474359229677832366040167901603216952640
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_121 :
Polynomial.coeff remainder4Coefficient3 121 = -(409455984444779808541789 * 10 ^ 70 + 6418157018161753409951353504760407600758844774528077630862364817336807)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_122 :
Polynomial.coeff remainder4Coefficient3 122 = 150888783553353839422656 * 10 ^ 70 + 8910256446539785832756053507015439620520167418111593329581571679804254
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_123 :
Polynomial.coeff remainder4Coefficient3 123 = -(53535801485746155776805 * 10 ^ 70 + 6057287935963117902385157780063985583237170594353294546161083630999250)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_124 :
Polynomial.coeff remainder4Coefficient3 124 = 18301924947629422074174 * 10 ^ 70 + 1632701538664775820651064420965680916344169757483868125902687615200995
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_125 :
Polynomial.coeff remainder4Coefficient3 125 = -(6035156688308510334621 * 10 ^ 70 + 5231974900826773200124788015357824866192640621217557378321203959237944)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_126 :
Polynomial.coeff remainder4Coefficient3 126 = 1922312304256268430934 * 10 ^ 70 + 6707626267801966647489410462750256418131824989131787276890961981606037
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_127 :
Polynomial.coeff remainder4Coefficient3 127 = -(592433276435154301038 * 10 ^ 70 + 7521575441256690901149228082702865388144409126844516721348939257884575)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_128 :
Polynomial.coeff remainder4Coefficient3 128 = 177088607875047042091 * 10 ^ 70 + 3230365089098629244038125760830735646836165103879779377413046979699671
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_129 :
Polynomial.coeff remainder4Coefficient3 129 = -(51601590765205889665 * 10 ^ 70 + 9858643047069216575905817170663286377494951100705815133031414267194503)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_130 :
Polynomial.coeff remainder4Coefficient3 130 = 14847912830643731742 * 10 ^ 70 + 743031372173481168651497569495291661894331894880277431155781563674464
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_131 :
Polynomial.coeff remainder4Coefficient3 131 = -(4352603552699508176 * 10 ^ 70 + 2495129050860873617178192092238007707779865793963810213773283153669119)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_132 :
Polynomial.coeff remainder4Coefficient3 132 = 1377244768107497777 * 10 ^ 70 + 5482122965522486228107777662161008626716679042899544292659136422439732
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_133 :
Polynomial.coeff remainder4Coefficient3 133 = -(499658828023131603 * 10 ^ 70 + 2799825365138056246341966657455872235270255274996065298133171773154231)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_134 :
Polynomial.coeff remainder4Coefficient3 134 = 207699603250264637 * 10 ^ 70 + 1256759509479349899292290388645248952637575887906350900379018312867083
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_135 :
Polynomial.coeff remainder4Coefficient3 135 = -(91769796553905303 * 10 ^ 70 + 4632507067092885548139982510666664888556477412820073992851635974699773)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_136 :
Polynomial.coeff remainder4Coefficient3 136 = 39332485312782678 * 10 ^ 70 + 3998681280819662608407261846836122289706157624998779732763792086090013
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_137 :
Polynomial.coeff remainder4Coefficient3 137 = -(15092430299684798 * 10 ^ 70 + 3685576211103818442186411079410809830514442796940887379675877414460350)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_138 :
Polynomial.coeff remainder4Coefficient3 138 = 4657208485277643 * 10 ^ 70 + 2778679041473559912311693920611412708553328658175144501928284214097193
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_139 :
Polynomial.coeff remainder4Coefficient3 139 = -(788272057103497 * 10 ^ 70 + 9905284501067927947459849182118137209658298636041716758126560186773715)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_140 :
Polynomial.coeff remainder4Coefficient3 140 = -(289389134448183 * 10 ^ 70 + 234482396875656949386206366238490122630698334674495904732983104655864)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_141 :
Polynomial.coeff remainder4Coefficient3 141 = 387458105070408 * 10 ^ 70 + 7290217259661452022661790646466103340836328273420206027089601394339523
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_142 :
Polynomial.coeff remainder4Coefficient3 142 = -(252740290434241 * 10 ^ 70 + 222873814658861301648844020209383938468991764041686548768398572197537)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_143 :
Polynomial.coeff remainder4Coefficient3 143 = 126865679732660 * 10 ^ 70 + 2073819349766682631278235671165446753619285485969410050283032391681739
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_144 :
Polynomial.coeff remainder4Coefficient3 144 = -(53491222458111 * 10 ^ 70 + 9127447608666298080670646784178147188563055217056843025332002660440173)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_145 :
Polynomial.coeff remainder4Coefficient3 145 = 19450864279384 * 10 ^ 70 + 1728640833993218764160070826998751519689058802761158483747094531394883
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_146 :
Polynomial.coeff remainder4Coefficient3 146 = -(6119014773678 * 10 ^ 70 + 4320553597331358413476387439106794408833006763342657709013383907720059)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_147 :
Polynomial.coeff remainder4Coefficient3 147 = 1641951112820 * 10 ^ 70 + 4446662609155753406954039122145831885462204392141023001306883700933573
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_148 :
Polynomial.coeff remainder4Coefficient3 148 = -(360610900071 * 10 ^ 70 + 5812968628521305914460892686792408692100154300407298413718324499120819)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_149 :
Polynomial.coeff remainder4Coefficient3 149 = 57338060556 * 10 ^ 70 + 8532571362967442919059634499209121137006446797194603505400027790593220
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_150 :
Polynomial.coeff remainder4Coefficient3 150 = -(2941217882 * 10 ^ 70 + 4040288801601615298919010316219132542834229810049884746544353891877341)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_151 :
Polynomial.coeff remainder4Coefficient3 151 = -(2029742867 * 10 ^ 70 + 7215496040348999888451357727922336715341483568452855372131477898983808)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_152 :
Polynomial.coeff remainder4Coefficient3 152 = 954851903 * 10 ^ 70 + 8777118683187602189966660339636999333589401061944063342247707488913605
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_153 :
Polynomial.coeff remainder4Coefficient3 153 = -(261523293 * 10 ^ 70 + 3985222630176398449348893763254794386295979768311644249549522726189836)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_154 :
Polynomial.coeff remainder4Coefficient3 154 = 52016130 * 10 ^ 70 + 6250820114246916347297255811826116776870176386468820960141010874861453
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_155 :
Polynomial.coeff remainder4Coefficient3 155 = -(7529738 * 10 ^ 70 + 8882614122119469278855918786920959646204592361785392329918892741887177)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A3_coeff_158 :
Polynomial.coeff remainder4Coefficient3 158 = -(13763 * 10 ^ 70 + 1343868770129886441278872977682933376295326019616474534153022713142713)