Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupLeadingSquarePart0.Coefficients150To185

Recurrence 2 lookup certificate: LeadingSquare coefficient convolution #

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.recurrence2LeadingSquare_coeff_150 :
Polynomial.coeff recurrence2LeadingSquare 150 = (17110797625113 * 10 ^ 70 + 7803136354220251963079489049286862744914123159981350292869984453567655) * 10 ^ 70 + 5829840466942300490220856394431217402135911992478764601119107403024203
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_151 :
Polynomial.coeff recurrence2LeadingSquare 151 = -((66674868401816 * 10 ^ 70 + 2780079362463552910070745305411224731696510162418121923428655029483340) * 10 ^ 70 + 1588864578536592429664980335202620368235379849800908284035380407939170)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_152 :
Polynomial.coeff recurrence2LeadingSquare 152 = (198060875696329 * 10 ^ 70 + 6589765158416653692001097551802121479083241208538797376701403628594383) * 10 ^ 70 + 2656435579946694090560510350834810558591884521562878942718034443015725
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_153 :
Polynomial.coeff recurrence2LeadingSquare 153 = -((506357284447979 * 10 ^ 70 + 7266226266335547070704491894519187557272627397107753688492538825594723) * 10 ^ 70 + 5429423630655691878173884915481560860585309622910647776995701255468672)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_154 :
Polynomial.coeff recurrence2LeadingSquare 154 = (1165410133137277 * 10 ^ 70 + 4254076600929588374492559981798635841383448187877256917822597838044166) * 10 ^ 70 + 6729098040554143795841370633239333555458964240461848678909808066764451
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_155 :
Polynomial.coeff recurrence2LeadingSquare 155 = -((2469290847431323 * 10 ^ 70 + 8713867468967484736279227852078564289909363216931331125088591615794132) * 10 ^ 70 + 9588956860963621905305399520838740959187031649581350967675857619794060)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_156 :
Polynomial.coeff recurrence2LeadingSquare 156 = (4879812377420622 * 10 ^ 70 + 3644614782040771001510051075364991829949051071761523100610787810143118) * 10 ^ 70 + 2686699142055411151022356709030087513369399429586959711266753881473745
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_157 :
Polynomial.coeff recurrence2LeadingSquare 157 = -((9070595625898303 * 10 ^ 70 + 3697253838118346009299964451172117819602497619593858222937748327347676) * 10 ^ 70 + 2773850950255377997119479093829362039842677350913619468548156812185072)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_158 :
Polynomial.coeff recurrence2LeadingSquare 158 = (15951979756759907 * 10 ^ 70 + 6432915155663492747524921130371108100472709421689907528406078127051213) * 10 ^ 70 + 5396348184049152367414231099604443365189081496813614071019907637984586
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_159 :
Polynomial.coeff recurrence2LeadingSquare 159 = -((26656267954113195 * 10 ^ 70 + 4944863148428924785234347156599594967499391278940227502498735232985139) * 10 ^ 70 + 9835924272667324858098516530858505528745478416779535096686640719270424)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_160 :
Polynomial.coeff recurrence2LeadingSquare 160 = (42462260821889358 * 10 ^ 70 + 8048599722423182140246951731972230594691315745124558405957631249531439) * 10 ^ 70 + 5038564117316556201463988024047381329283541521026475993742603490194503
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_161 :
Polynomial.coeff recurrence2LeadingSquare 161 = -((64644522565907105 * 10 ^ 70 + 111420052572303362650081732526273212546528981068750102730847447024483) * 10 ^ 70 + 2570365848984397006613083626401423394405718030886319893093130205281468)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_162 :
Polynomial.coeff recurrence2LeadingSquare 162 = (94247720756585141 * 10 ^ 70 + 548285100009841693011212051484520245736045033294196874316990910754201) * 10 ^ 70 + 5262019637358391591584994035311244930957584445448007293190482704564818
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_163 :
Polynomial.coeff recurrence2LeadingSquare 163 = -((131808321179580348 * 10 ^ 70 + 604944564749018442532190391953172386838444005303647405194582100059049) * 10 ^ 70 + 7387758481400842812399883716274346062903767782233273284541330747720588)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_164 :
Polynomial.coeff recurrence2LeadingSquare 164 = (177070139740146117 * 10 ^ 70 + 1554026460212924309907777448460316389740463010088882821481194503468618) * 10 ^ 70 + 4419993593040215228563970056858241850171804641252218772784154267519459
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_165 :
Polynomial.coeff recurrence2LeadingSquare 165 = -((228759172998877039 * 10 ^ 70 + 8957622966484034698299725454532066241757746197491602581983815710846928) * 10 ^ 70 + 4212605247694170406643710454898916068696553488384538942928627239511346)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_166 :
Polynomial.coeff recurrence2LeadingSquare 166 = (284488434923996265 * 10 ^ 70 + 5128043614739638670305918058857397206827631310008557768153014225224471) * 10 ^ 70 + 1711201472649932121974464793620071438065985543537001633720722506388751
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_167 :
Polynomial.coeff recurrence2LeadingSquare 167 = -((340849291862578963 * 10 ^ 70 + 7155602375680749089901391124930806354539425205508765670628640410791474) * 10 ^ 70 + 9597305233737252030007447888147002018615372587989731726619136893766366)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_168 :
Polynomial.coeff recurrence2LeadingSquare 168 = (393711498839999002 * 10 ^ 70 + 5393468418425137843442496546308349874889374918003367882552183379234511) * 10 ^ 70 + 5609887109249082143816362742604121271938235745793486089778167750181137
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_169 :
Polynomial.coeff recurrence2LeadingSquare 169 = -((438706250280023447 * 10 ^ 70 + 9315794830626408856848736537991752662825518948016803581536909139826117) * 10 ^ 70 + 8581019990857780546016833787773256626389536685424577245175639942336556)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_170 :
Polynomial.coeff recurrence2LeadingSquare 170 = (471817508450118668 * 10 ^ 70 + 8745253953030173641668037184780281979186812458942290824944423874472464) * 10 ^ 70 + 7886743605591826207328841403183397006353700064896626772598765239672698
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_171 :
Polynomial.coeff recurrence2LeadingSquare 171 = -((489971517758549278 * 10 ^ 70 + 6295474434813443592506175798300171995771936980048572122345792741895010) * 10 ^ 70 + 3913535860528468525691334815474861941888824661099241671630626952929432)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_172 :
Polynomial.coeff recurrence2LeadingSquare 172 = (491504943529613846 * 10 ^ 70 + 2803873268348120657864562966765284189311016073710450305399959256645427) * 10 ^ 70 + 991100563216025934415222199271179540237047213928760840050022475309811
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_173 :
Polynomial.coeff recurrence2LeadingSquare 173 = -((476413376328820565 * 10 ^ 70 + 4042469131841676794869069612724255999970421608891566798415264690237296) * 10 ^ 70 + 2398931059481738777350530102745520264482143350656882841261344363547470)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_174 :
Polynomial.coeff recurrence2LeadingSquare 174 = (446329348460158462 * 10 ^ 70 + 7017496237428318676686082338228054122385295926409965679363715265397592) * 10 ^ 70 + 1273223444086736593138428696663046794972828737255290532410281368882084
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_175 :
Polynomial.coeff recurrence2LeadingSquare 175 = -((404239505203883525 * 10 ^ 70 + 6435442552323175229710529313163177784154028033998804829736420734722638) * 10 ^ 70 + 1409079299455487425486106842335187912230967145414987424055419824900504)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_176 :
Polynomial.coeff recurrence2LeadingSquare 176 = (354007117760415995 * 10 ^ 70 + 7961277015278161165684734226316587483101461751545100832655887903289497) * 10 ^ 70 + 7103532007056140053337783774977501322396522260210464715953942127484309
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_177 :
Polynomial.coeff recurrence2LeadingSquare 177 = -((299803394967670974 * 10 ^ 70 + 731134628448428581492622479629012682519448067942537007391478556474969) * 10 ^ 70 + 9390868963521169687848019932663884126327098269706443998244357066199664)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_178 :
Polynomial.coeff recurrence2LeadingSquare 178 = (245560379963959955 * 10 ^ 70 + 1630039560963338965902733824437674845094935232806199810786598908730067) * 10 ^ 70 + 1199408169235597941825791339381784997360594031112557543465143179794980
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_179 :
Polynomial.coeff recurrence2LeadingSquare 179 = -((194539891360412406 * 10 ^ 70 + 1672881843698526975899647274178080393502587504889897914797525385262616) * 10 ^ 70 + 1989812595126109606091476490710889908069559092410174517951776211379634)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_180 :
Polynomial.coeff recurrence2LeadingSquare 180 = (149075226496705352 * 10 ^ 70 + 7447493202646368848088827347027378472594998010919183995090600643410940) * 10 ^ 70 + 7917994324435433751563420526168734763501909156511646178951800096618502
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_181 :
Polynomial.coeff recurrence2LeadingSquare 181 = -((110497799112994452 * 10 ^ 70 + 2241872135013172588106467042053021511395087613359186421138353682304729) * 10 ^ 70 + 2957239961105335319098725497687399336830934799041198689585023074137522)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_182 :
Polynomial.coeff recurrence2LeadingSquare 182 = (79221978279861330 * 10 ^ 70 + 7821982073305994635169150382389827528287945534585378626815338686052800) * 10 ^ 70 + 7239513874891218983877668671197068361431328212821452696414127369971537
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_183 :
Polynomial.coeff recurrence2LeadingSquare 183 = -((54936669060384169 * 10 ^ 70 + 8689556286648118449588688578599546910934586405961542073678281132594542) * 10 ^ 70 + 9375916457808369323965357804043602811761526102072119606907368968070982)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_184 :
Polynomial.coeff recurrence2LeadingSquare 184 = (36844502955873192 * 10 ^ 70 + 1701264772888659446594928845644464083576611927249761749998029708521050) * 10 ^ 70 + 2027904934455929589468100528723010062423538226424594106877839557571598
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_185 :
Polynomial.coeff recurrence2LeadingSquare 185 = -((23896522935918248 * 10 ^ 70 + 136884398156507136156508710381830256462634378529393120402453090829310) * 10 ^ 70 + 3058977628029452723993133566461525569047648063439653182893123531632036)