Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar2LeftPart1.Coefficients340To378

Recurrence 2 lookup certificate: Scalar2Left 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.recurrence2Scalar2Left_coeff_340 :
Polynomial.coeff recurrence2Scalar2Left 340 = -((40708407017 * 10 ^ 70 + 8504022484933540598833242249133096394891875824398006365427428632934663) * 10 ^ 70 + 2043608291140668427114048956423025649533008655223002133016964080573854)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_341 :
Polynomial.coeff recurrence2Scalar2Left 341 = (634631686 * 10 ^ 70 + 3742985392917109849977339316151991937632756486920873968074292639691605) * 10 ^ 70 + 5263716612608886088961367119087799424711570427859971232058823252702357
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_342 :
Polynomial.coeff recurrence2Scalar2Left 342 = -((141585 * 10 ^ 70 + 5781915359238123969400060388662028737397891803528403729045367528183708) * 10 ^ 70 + 9447118960331124915370297144611248012986982184958116820432038310939834)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_343 :
Polynomial.coeff recurrence2Scalar2Left 343 = -((137958 * 10 ^ 70 + 6067080147428829535913947132489682643028212328858975140820298332914754) * 10 ^ 70 + 1422661978780556683980295405168599734725089766664923133291917057384832)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_344 :
Polynomial.coeff recurrence2Scalar2Left 344 = (1666 * 10 ^ 70 + 6708684550033839668658984277347252104802747870111899347665281492102261) * 10 ^ 70 + 8051853403921508876028752526491148034058602346745360116226737192044339
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_345 :
Polynomial.coeff recurrence2Scalar2Left 345 = (2 * 10 ^ 70 + 3077150461792369414461759803145344781523149488193016747887319212309355) * 10 ^ 70 + 5488028719859956711567979293530239170599576121172397015609585197556313
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_346 :
Polynomial.coeff recurrence2Scalar2Left 346 = -(1804471947942635003028027279223331276003470183176823465239562817855022 * 10 ^ 70 + 8218362127691463035236126946200286600228152727489593920375776172635529)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_347 :
Polynomial.coeff recurrence2Scalar2Left 347 = 7795996385656912117607016265998944504198808066702154529842141931609 * 10 ^ 70 + 3679465891171055282453238312107624153294132633931610937941244504857688
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_348 :
Polynomial.coeff recurrence2Scalar2Left 348 = 77370453674922051339538767665300552521681502470316296352204762856 * 10 ^ 70 + 6433015689437960898403963130389135913706118560036823881932888980107999
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_349 :
Polynomial.coeff recurrence2Scalar2Left 349 = -(610025508901501215157421317594029468876334287722601850013513524 * 10 ^ 70 + 1328822544467791436028545018175221741155440205511190974030333254768612)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_350 :
Polynomial.coeff recurrence2Scalar2Left 350 = -(1381797314573962088702339675965693583262010261117877094334892 * 10 ^ 70 + 9969038555257337079722954490779913165833718679387569761644331581310844)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_351 :
Polynomial.coeff recurrence2Scalar2Left 351 = 20508955284546651535880119579542971692849146436304705756823 * 10 ^ 70 + 7113872019016680717576408952860218371870123447720877524719206169741818
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_352 :
Polynomial.coeff recurrence2Scalar2Left 352 = -(2542568150077443108637755644014902200395149114143348778 * 10 ^ 70 + 5514232751889585870894323052897113967278107840068294402028269686239849)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_353 :
Polynomial.coeff recurrence2Scalar2Left 353 = -(364863057946255163615247076886654957755118548827579359 * 10 ^ 70 + 1178631619699265435713397124160389837177166053433042165295334905115536)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_354 :
Polynomial.coeff recurrence2Scalar2Left 354 = 532200493993842524544307930536907574353935483020983 * 10 ^ 70 + 8576632966863146084937107244670182106326551930643757034743278924189547
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_355 :
Polynomial.coeff recurrence2Scalar2Left 355 = 3365148061082629138355466629996445736086283273840 * 10 ^ 70 + 3912388244156226477667596266133142492477200675891641423047100504607328
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_356 :
Polynomial.coeff recurrence2Scalar2Left 356 = -(8958673106345730467956178475423282083134446884 * 10 ^ 70 + 2395612599131988392970163620874446062573250835664554325935554383436863)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_357 :
Polynomial.coeff recurrence2Scalar2Left 357 = -(11526276649966096593593846001241934408592380 * 10 ^ 70 + 5457445805886603053311948087836970204988935937548064543980262654224803)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_358 :
Polynomial.coeff recurrence2Scalar2Left 358 = 62230281519292080353328103661998284136149 * 10 ^ 70 + 4992570157082701856866919567571203326389998140440556305057296342766707
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_359 :
Polynomial.coeff recurrence2Scalar2Left 359 = -(34005294992908469187483516233116000627 * 10 ^ 70 + 9113883548582348149409454813520524197440068427726273191539809148720134)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_360 :
Polynomial.coeff recurrence2Scalar2Left 360 = -(143476662966419478070951742551888422 * 10 ^ 70 + 2975823137217593690026078456837171351277536306294630672209454120228400)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_361 :
Polynomial.coeff recurrence2Scalar2Left 361 = 258266752598609706894148994719421 * 10 ^ 70 + 2355742230385039858076612216115498340760039103349558806877034038751004
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_362 :
Polynomial.coeff recurrence2Scalar2Left 362 = -(113508781085075293009636672752 * 10 ^ 70 + 7964953088162664516452966131177920065816315508520004733765730301495458)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_363 :
Polynomial.coeff recurrence2Scalar2Left 363 = -(88517437888567200231829520 * 10 ^ 70 + 7425513021196020965811622493663505273826014572662116905583294464840405)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_364 :
Polynomial.coeff recurrence2Scalar2Left 364 = 114153677450027860522058 * 10 ^ 70 + 4078681459268105657201641388912318448434215460345399605299010293288158
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_365 :
Polynomial.coeff recurrence2Scalar2Left 365 = -(44227618253274786699 * 10 ^ 70 + 5062413085514763492116059357486171410706000749220210774888321138022335)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_366 :
Polynomial.coeff recurrence2Scalar2Left 366 = 5563236681362631 * 10 ^ 70 + 542266726839416510313928919648634932674885773980843614507261826583244
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_367 :
Polynomial.coeff recurrence2Scalar2Left 367 = 477844709148 * 10 ^ 70 + 1805014600880623918742962448513093763835015599248972871974634773596547
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_368 :
Polynomial.coeff recurrence2Scalar2Left 368 = -(168675303 * 10 ^ 70 + 2522715356130651820079075062823924418498948790867870770582464649298139)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_369 :
Polynomial.coeff recurrence2Scalar2Left 369 = 12369 * 10 ^ 70 + 3837428923292602925712172680413368041792537765336496475393651431245761
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_370 :
Polynomial.coeff recurrence2Scalar2Left 370 = -3024516181811578574208994770112130437187217941495641214476521933648312
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_371 :
Polynomial.coeff recurrence2Scalar2Left 371 = 5593358761912299372840248274854305808116493005983842481284199347
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_372 :
Polynomial.coeff recurrence2Scalar2Left 372 = 349903081699219370002257669547137221463936703025739577338281
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_373 :
Polynomial.coeff recurrence2Scalar2Left 373 = -2441355828325855674605786505737644789852349962246652922
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_374 :
Polynomial.coeff recurrence2Scalar2Left 374 = 3057882343441783644551122281669487336154913470265
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_375 :
Polynomial.coeff recurrence2Scalar2Left 375 = -964966229735737416297104475168744575522188
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_376 :
Polynomial.coeff recurrence2Scalar2Left 376 = -81304863666383514154862603906427012
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_377 :
Polynomial.coeff recurrence2Scalar2Left 377 = 1245463248866986683210561204
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_378 :
Polynomial.coeff recurrence2Scalar2Left 378 = -4412933304219039693