Recurrence 2 lookup certificate: Scalar4Left coefficient convolution #
This is a checked coefficient-lookup shard for the second pseudo-division recurrence in the order-seven certificate.
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_269 :
Polynomial.coeff recurrence2Scalar4Left 269 = (28427970017993771507080412894788068136120555081193291051548715681 * 10 ^ 70 + 6011915415710140948170712271178475452516449963036285637551913175485444) * 10 ^ 70 + 7091026198380642034338994237446765905719149304994840577505977930252393
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_270 :
Polynomial.coeff recurrence2Scalar4Left 270 = -((11510293473120708703611579634731686058673394796206928559045602110 * 10 ^ 70 + 7377526094437848321167958400489984192319493169374069761680068248023925) * 10 ^ 70 + 1474563383068953637748543236887482213552415101640645296320578045469808)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_271 :
Polynomial.coeff recurrence2Scalar4Left 271 = (4296614298140162404018048278698315561752261419226833937469332391 * 10 ^ 70 + 4144832620549594422476946282955812889649571990306445971038847240705841) * 10 ^ 70 + 2454817955891048794930339520057049514574111790022526708554563641353226
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_272 :
Polynomial.coeff recurrence2Scalar4Left 272 = -((1448085344032067502770306113331825953981639131034672403396249708 * 10 ^ 70 + 5373378360006952532589086441546942402915317379905268722408349609248225) * 10 ^ 70 + 4265162534984675837972545344662646592023905595825332964368373194653546)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_273 :
Polynomial.coeff recurrence2Scalar4Left 273 = (420450192132521630357486273720824931292589631884824166964412735 * 10 ^ 70 + 1675470434678709221668124604812677776109385322946475331199390525215215) * 10 ^ 70 + 8997888327656599569378058875078717104780234552324159967007613521541926
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_274 :
Polynomial.coeff recurrence2Scalar4Left 274 = -((91300578828140533398622176780356450619325626113988039316254132 * 10 ^ 70 + 7583388456479625759202387247480344336122448539062021741744871691976136) * 10 ^ 70 + 8222555888114477222793769199811708811913067537195476615944893418656577)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_275 :
Polynomial.coeff recurrence2Scalar4Left 275 = (4114714635489679352994626200800956295210012444669182375288588 * 10 ^ 70 + 2517245726198283229186030472622313998876706494652831650077696723583425) * 10 ^ 70 + 317053807870997306181603231874432764134477770028488473609343545234937
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_276 :
Polynomial.coeff recurrence2Scalar4Left 276 = (10392680321115095816488363452174781262323775241857249414238572 * 10 ^ 70 + 3782482394332909854142199466910884097663012039666231133660615037115943) * 10 ^ 70 + 2454071175313344115912836910024230212205696681938475077631503062061958
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_277 :
Polynomial.coeff recurrence2Scalar4Left 277 = -((8046710335714732988993378397088585326572757160810114334765657 * 10 ^ 70 + 2510439117175715077798866303439446220871649144171704989503882497010745) * 10 ^ 70 + 9538872543910860464391292178347355849806590006000297541878687740449485)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_278 :
Polynomial.coeff recurrence2Scalar4Left 278 = (4253791137616590615290580362117089726991850676695893576479406 * 10 ^ 70 + 9300809602469059980278479880259573204675712243412201412017782148669079) * 10 ^ 70 + 2108623816352614744121712549104310745566799799954746369417639828181581
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_279 :
Polynomial.coeff recurrence2Scalar4Left 279 = -((1885275634202824625890844985690583379681913611180454277853059 * 10 ^ 70 + 3894769358330479619991340798886902435572608166552913560098096500884548) * 10 ^ 70 + 2129087966181079488796385521676843858070980901332552324461852548264414)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_280 :
Polynomial.coeff recurrence2Scalar4Left 280 = (742092265898185163415386351938209228944289361264412252842093 * 10 ^ 70 + 2290253663150701409673707835855084426128969324412324820959557929003814) * 10 ^ 70 + 8578933491800368818431939985269610787597903127299641398539985654112113
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_281 :
Polynomial.coeff recurrence2Scalar4Left 281 = -((265306703771013852536250085324508450940963712857308533033846 * 10 ^ 70 + 3919980169893187050004711205263812928344243756255806542691155107921419) * 10 ^ 70 + 6290614945798025339439129351617554584057947883309646913978645857727446)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_282 :
Polynomial.coeff recurrence2Scalar4Left 282 = (86881799891303435095512332241954701801343443439841159763642 * 10 ^ 70 + 428302597427483182366668463132025253334591032562260685617207464596553) * 10 ^ 70 + 1545622973919440928439104210100397083797996524762090320738133875009340
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_283 :
Polynomial.coeff recurrence2Scalar4Left 283 = -((26071384310513519505814049392739300317006817343891484031931 * 10 ^ 70 + 5628491259954131570852102491797484318054528517260093476421240137945523) * 10 ^ 70 + 5238861582135205041936214714959197947767134141474740896081698519008850)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_284 :
Polynomial.coeff recurrence2Scalar4Left 284 = (7118207274410863827033690025056176970571665082082420458540 * 10 ^ 70 + 4827420798902158824403197402147894441846491728333117195807312671609950) * 10 ^ 70 + 6814126898771093205267224132587089421591014680817737885002414860282885
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_285 :
Polynomial.coeff recurrence2Scalar4Left 285 = -((1736282065925091421718448179674578949236923858755212945775 * 10 ^ 70 + 5494685501541256785329244810791143866991658734648419260062203396352235) * 10 ^ 70 + 2981600231739178428359647960253929373875364462294896034708590293628624)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_286 :
Polynomial.coeff recurrence2Scalar4Left 286 = (362389362052085944052438716606987229747704528572164555672 * 10 ^ 70 + 2210506204547632418563160430596232248615975700015394756518523623416768) * 10 ^ 70 + 5914223388130095739983987654417766435490924976376270978483187135333752
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_287 :
Polynomial.coeff recurrence2Scalar4Left 287 = -((56937382280754893348948479744681794926664146287013709001 * 10 ^ 70 + 5391646098736000640345546460808169247262034829225592177805898244892021) * 10 ^ 70 + 2434939748835080229229551702266023413555761805702324982190252460719160)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_288 :
Polynomial.coeff recurrence2Scalar4Left 288 = (2606981767087592999246844019782320777835855689410833586 * 10 ^ 70 + 8843448551488518861036620593485221835715244058556400118661491878027555) * 10 ^ 70 + 2909110041110080198811549227572758066700068319592389792869451330468994
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_289 :
Polynomial.coeff recurrence2Scalar4Left 289 = (2668436677642448745970122373417747310491822395411568835 * 10 ^ 70 + 7932056178384795780064913360988526196392348265466268722256604819110597) * 10 ^ 70 + 4160804679625567056886439008432820509989636862402911920786474918144846
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_290 :
Polynomial.coeff recurrence2Scalar4Left 290 = -((1468209251092698970368108145600861469426972637884189368 * 10 ^ 70 + 395546323149485402592590172349931028199991394029846335763120898266899) * 10 ^ 70 + 7738132453768682318892393586472218039336691600920483968463884434380263)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_291 :
Polynomial.coeff recurrence2Scalar4Left 291 = (525977744765869581421283024998222380556276698962660574 * 10 ^ 70 + 5464938992207299973156172241759843669247325806446992257684786018285365) * 10 ^ 70 + 3146788709104438918831320626277350557548841490247482501073815815317708
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_292 :
Polynomial.coeff recurrence2Scalar4Left 292 = -((154292793797424938224845148192682551660013782471079350 * 10 ^ 70 + 1652851545931657038218556625171174948670824180805089964535144571203863) * 10 ^ 70 + 767642255717460569434127471773318106943671966305413805952781033212506)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_293 :
Polynomial.coeff recurrence2Scalar4Left 293 = (39309704832120650311090189159214876904407991299689230 * 10 ^ 70 + 1221716171684843817269676272601996894922612878855222407402361104335164) * 10 ^ 70 + 551976984973656768653085813320400155121162055653140339617063149965128
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_294 :
Polynomial.coeff recurrence2Scalar4Left 294 = -((8860445955804332551544309182193075844049375495891088 * 10 ^ 70 + 3519969204792300586566522241354111170864331622675018233730712004173356) * 10 ^ 70 + 8322275042097405050696151398427825830293891756614944869773148655730023)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_295 :
Polynomial.coeff recurrence2Scalar4Left 295 = (1766233617528752172175754038472002302875010327630762 * 10 ^ 70 + 4643595322035982917410001373635639930386025569216769887929768692022279) * 10 ^ 70 + 5430763417868992203319405925204748235399807998416688656393030406018323
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_296 :
Polynomial.coeff recurrence2Scalar4Left 296 = -((305702950738270039452472755989960054997906420432592 * 10 ^ 70 + 4958426518972284467947335932644699132997795018335186374346644539106863) * 10 ^ 70 + 1362864364036875599251907622188042801134909609046449572557212101921512)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_297 :
Polynomial.coeff recurrence2Scalar4Left 297 = (43533056904275133006623156853806333104694217640612 * 10 ^ 70 + 9704846700414654154743118953907065163408651669444785730412265451413521) * 10 ^ 70 + 8137906491023853184119742929596666528605932153864320577733402334831824
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_298 :
Polynomial.coeff recurrence2Scalar4Left 298 = -((4224019963070870916266269094855187712768480073246 * 10 ^ 70 + 8055082257829541848739627011561564082084148521925646637566547845572229) * 10 ^ 70 + 3342281952488215591456345826174412031801900607936388921945887519667515)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_299 :
Polynomial.coeff recurrence2Scalar4Left 299 = -((62179020055548805274407778915589061093792655040 * 10 ^ 70 + 6435377489150262929684673451723017437225645561701969570024440736309972) * 10 ^ 70 + 8615205672098910433105637308463850670237644040829040961664285414226023)