Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupLeadingSquarePart0.Coefficients186To223

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_186 :
Polynomial.coeff recurrence2LeadingSquare 186 = (14986326286332331 * 10 ^ 70 + 631279681426255074906526615336463964238914641187019181083037487667382) * 10 ^ 70 + 8832225629771843700996964932489086562824051162992535348185468772858187
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_187 :
Polynomial.coeff recurrence2LeadingSquare 187 = -((9086361014156847 * 10 ^ 70 + 4612558774044820166246472830895421199088711474789548739884042486558571) * 10 ^ 70 + 647876631820549867914579195473415220341145242861931901795741984714480)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_188 :
Polynomial.coeff recurrence2LeadingSquare 188 = (5325300239257643 * 10 ^ 70 + 6572794702575718877739916977957379379017228347808751587521975140359994) * 10 ^ 70 + 9674957397791616804949854615550682027266328477470158879162087945318790
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_189 :
Polynomial.coeff recurrence2LeadingSquare 189 = -((3016279426461505 * 10 ^ 70 + 9508316015228691542643589080621716724803562123980904823154743481219857) * 10 ^ 70 + 2452415880586974778130436970932241836845809801538663858549432499267406)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_190 :
Polynomial.coeff recurrence2LeadingSquare 190 = (1650727842166910 * 10 ^ 70 + 3845145030097437167150021909350249052440435971368616619513570967403259) * 10 ^ 70 + 3695375507379360429118235933898536861037633968562447432363988767503992
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_191 :
Polynomial.coeff recurrence2LeadingSquare 191 = -((872665400115388 * 10 ^ 70 + 6669800089026371181771669032954299369563587312848426289737354612537640) * 10 ^ 70 + 5883723961435713960648808540216494317078315824790638027378397359462466)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_192 :
Polynomial.coeff recurrence2LeadingSquare 192 = (445521889451028 * 10 ^ 70 + 6680109398632045069138220363851799485026173579450137256020703886055717) * 10 ^ 70 + 2298340233518511695792536550785799710290951658115055586594240498396410
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_193 :
Polynomial.coeff recurrence2LeadingSquare 193 = -((219587905799455 * 10 ^ 70 + 3014549859593331837687112159164931765083060043798731919980140510940314) * 10 ^ 70 + 643635380512090967347525180696154548718630735778459441897371430380714)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_194 :
Polynomial.coeff recurrence2LeadingSquare 194 = (104453518178048 * 10 ^ 70 + 1641076070905689763142264709859359042337636027258496416605222639770336) * 10 ^ 70 + 5935110642028306029355654863583772074884198542912747826188495318744048
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_195 :
Polynomial.coeff recurrence2LeadingSquare 195 = -((47935579782235 * 10 ^ 70 + 8464633089170019625824545374157962889873901278738697698800134471868296) * 10 ^ 70 + 5140723207011661275201910127942609552300079045574211202028809728240362)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_196 :
Polynomial.coeff recurrence2LeadingSquare 196 = (21215118566463 * 10 ^ 70 + 6501680895004036664187644129151859538880156853699149105150570395209905) * 10 ^ 70 + 3280439890814794551283717636380388994588722905451525664835898869853258
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_197 :
Polynomial.coeff recurrence2LeadingSquare 197 = -((9051168786240 * 10 ^ 70 + 5441439836983832360482295106660435751555146757662186934177190966125019) * 10 ^ 70 + 8492542149933135131833808068093519969570845289951547007102929934644182)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_198 :
Polynomial.coeff recurrence2LeadingSquare 198 = (3720840246687 * 10 ^ 70 + 857812984779513470144544952763249975296051278865797461433460084201080) * 10 ^ 70 + 5772753208889227399079341345395535569582083351646129789833621462910992
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_199 :
Polynomial.coeff recurrence2LeadingSquare 199 = -((1473145455882 * 10 ^ 70 + 5732964456683428014716316899833585333561427081455722076914286343495309) * 10 ^ 70 + 6366737700969443863546567619398711289077769995511331989764582488517850)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_200 :
Polynomial.coeff recurrence2LeadingSquare 200 = (561428560264 * 10 ^ 70 + 2199486712935382136686481949688640833467451110536828033334862089416534) * 10 ^ 70 + 7046015299533944586564123955397143595573777024387052958866133874303433
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_201 :
Polynomial.coeff recurrence2LeadingSquare 201 = -((205848539228 * 10 ^ 70 + 9652587582171505717356442998855814379995469212146001916297531533077403) * 10 ^ 70 + 3689306896662532594772338789476166084284604442088645764287103700196786)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_202 :
Polynomial.coeff recurrence2LeadingSquare 202 = (72568623252 * 10 ^ 70 + 1959286265017552628139329746503025508086333319548343478076293197190786) * 10 ^ 70 + 4849192694450337361582410533320162821089593098945664717628471582291894
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_203 :
Polynomial.coeff recurrence2LeadingSquare 203 = -((24582351115 * 10 ^ 70 + 8519644431953424158709891013715060342333813834974847798802938764880273) * 10 ^ 70 + 9737116107681517212486316386892706973745856382598405221150097407987948)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_204 :
Polynomial.coeff recurrence2LeadingSquare 204 = (7996098874 * 10 ^ 70 + 2698794206824101326767543205209985161048450464971649753312748770740521) * 10 ^ 70 + 2649576412150990483685128176926485723464700542073288009491805358354276
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_205 :
Polynomial.coeff recurrence2LeadingSquare 205 = -((2495742425 * 10 ^ 70 + 73540608005033702144520493004198829511714306579665628134413366408714) * 10 ^ 70 + 2594869539507100191072451748192511992946078781798408185907761169961926)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_206 :
Polynomial.coeff recurrence2LeadingSquare 206 = (746884458 * 10 ^ 70 + 8194510803614343993663735046687399371702827044229828191466264116510209) * 10 ^ 70 + 5543568330439761253337831837084810374781260574411589082665666690192664
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_207 :
Polynomial.coeff recurrence2LeadingSquare 207 = -((214131875 * 10 ^ 70 + 4025057935649769128549900459379839011360884215641085923841322563838903) * 10 ^ 70 + 745391505051610551971271796890893598192436307375805611284795952813018)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_208 :
Polynomial.coeff recurrence2LeadingSquare 208 = (58762589 * 10 ^ 70 + 7212314018797570118160340767157235051415403775782948668896135013564107) * 10 ^ 70 + 3175823372477438550714180002583413058434039418091119505399717841591923
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_209 :
Polynomial.coeff recurrence2LeadingSquare 209 = -((15420665 * 10 ^ 70 + 640106433657232598524760722642144951740781624881186615666763952325571) * 10 ^ 70 + 3255984462006274586688686844321424659629668605539152931890290413146682)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_210 :
Polynomial.coeff recurrence2LeadingSquare 210 = (3865894 * 10 ^ 70 + 3510643320721691511950739758647762353420569909482153648533762933981736) * 10 ^ 70 + 5696967650994421620507575863535867137046349149441829866460547304856617
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_211 :
Polynomial.coeff recurrence2LeadingSquare 211 = -((924852 * 10 ^ 70 + 7261238256021057555322536937197390275022375730025557583937814968921061) * 10 ^ 70 + 5384962400575975482322893615566211998335810900439317381147967402691502)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_212 :
Polynomial.coeff recurrence2LeadingSquare 212 = (210895 * 10 ^ 70 + 9120186083789091118940517305552758272955768443611285127580236379241534) * 10 ^ 70 + 7991413798311010318219073576195167170748698999809401650262622677560044
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_213 :
Polynomial.coeff recurrence2LeadingSquare 213 = -((45782 * 10 ^ 70 + 2601972824516206469598138933949775236344718993676571710954164698310379) * 10 ^ 70 + 9379628846607076060831217172084084707365169364635283034708100428074604)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_214 :
Polynomial.coeff recurrence2LeadingSquare 214 = (9448 * 10 ^ 70 + 8766746509889255849292812731063315576284207458915266679624348279785212) * 10 ^ 70 + 9885635069649933498809517369040691188310611150235513854717606586946080
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_215 :
Polynomial.coeff recurrence2LeadingSquare 215 = -((1851 * 10 ^ 70 + 3712405206963375383080096680073657699445001432595742241329934295150539) * 10 ^ 70 + 1934748106406742675555282122996678406973347414708674645145535459138784)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_216 :
Polynomial.coeff recurrence2LeadingSquare 216 = (343 * 10 ^ 70 + 8472388040612105850856754691022873502849000507772554672767908631479709) * 10 ^ 70 + 9898770156434235785534309517006124305592756228696766550809948904680295
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_217 :
Polynomial.coeff recurrence2LeadingSquare 217 = -((60 * 10 ^ 70 + 4326362964279892456809182232038787418891779410127871892941479235512197) * 10 ^ 70 + 772942043900287562772000555670988096394051436231723001194728211388638)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_218 :
Polynomial.coeff recurrence2LeadingSquare 218 = (10 * 10 ^ 70 + 329401684757488517464079534304537745347867847229354044757424078856197) * 10 ^ 70 + 1648307642529484751939942341821424879546494140473879702747914266619247
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_219 :
Polynomial.coeff recurrence2LeadingSquare 219 = -((1 * 10 ^ 70 + 5703173748220766233378572841685589249080770261927797590607074742264867) * 10 ^ 70 + 7192523641910750664469181180040774895962677542497325266128285532172158)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_220 :
Polynomial.coeff recurrence2LeadingSquare 220 = 2312218935472285628842558733467792252174177528659053760300299711174956 * 10 ^ 70 + 9163287838227158023630917178970253568222818022541897891482908316945340
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_221 :
Polynomial.coeff recurrence2LeadingSquare 221 = -(319559832823945006546574583572961229842470370677542546198353774389343 * 10 ^ 70 + 2448652029500540205230659306111361871020509528326983259538586792558250)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_222 :
Polynomial.coeff recurrence2LeadingSquare 222 = 41349153610091287593392011456400566053374994798446085313984702078098 * 10 ^ 70 + 3956975668630826749458332048498449562205561993888997379602102055512651
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_223 :
Polynomial.coeff recurrence2LeadingSquare 223 = -(4995520856907125088556496549434134919611082967251503792589107608111 * 10 ^ 70 + 777521238124197583064949279349445676893514361490511486377601614426174)