Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar2MainPart1.Coefficients338To379

Recurrence 2 lookup certificate: Scalar2Main 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.recurrence2Scalar2Main_coeff_338 :
Polynomial.coeff recurrence2Scalar2Main 338 = (42749094092037 * 10 ^ 70 + 7349261696630370478484113023172077119798433567073471976497752897805366) * 10 ^ 70 + 3040694971606177036461271217995487404859270440095414708300093950149754
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_339 :
Polynomial.coeff recurrence2Scalar2Main 339 = (605219502443 * 10 ^ 70 + 8062606134850276551226079072138662613227451230151612766269800078727252) * 10 ^ 70 + 1771289853334110269480421119672266835015369419686841732230380070139370
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_340 :
Polynomial.coeff recurrence2Scalar2Main 340 = -((38281771593 * 10 ^ 70 + 8222816862748036095594504127342120226611063719499301117352703924469305) * 10 ^ 70 + 7510246432130502696826153772915537128206019036584982296081959570555769)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_341 :
Polynomial.coeff recurrence2Scalar2Main 341 = (663021303 * 10 ^ 70 + 9748615241039257352026470910976966690151525520885629980949499453449036) * 10 ^ 70 + 8208343072554892410768474559387757285850644943310317436836182871925528
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_342 :
Polynomial.coeff recurrence2Scalar2Main 342 = -((1494056 * 10 ^ 70 + 7365298637413364192025636794011435075582701756270118905580927205792429) * 10 ^ 70 + 2787278540758064467596584690870669888190079986295138246341636948136052)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_343 :
Polynomial.coeff recurrence2Scalar2Main 343 = -((123981 * 10 ^ 70 + 1569494618721921909263768837740908527507473866440412162763175324796806) * 10 ^ 70 + 1566881402019436089572503327967703564884882710202427580745474883728932)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_344 :
Polynomial.coeff recurrence2Scalar2Main 344 = (1750 * 10 ^ 70 + 659305172265827826654960018506642769151622325639083524269068719769816) * 10 ^ 70 + 738814636327312967556254934093623186442486121192588879099437551886688
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_345 :
Polynomial.coeff recurrence2Scalar2Main 345 = -(4582067153741661154198370094156679588145839382290741915415605322238610 * 10 ^ 70 + 279821981209881534869166573736503437259515537122763343289875715682159)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_346 :
Polynomial.coeff recurrence2Scalar2Main 346 = -(1699928389991809944570681786482199317010522823889880844807933320933648 * 10 ^ 70 + 8151711812058491794675217296377519304482006188413197985181531592129466)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_347 :
Polynomial.coeff recurrence2Scalar2Main 347 = 9568797926171031490751121382228950088351393623306119393532339064460 * 10 ^ 70 + 5091421296747403896849086108238623889012397759998895056944755336975574
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_348 :
Polynomial.coeff recurrence2Scalar2Main 348 = 63482887981909753055418875846658849208472659939121243189559946854 * 10 ^ 70 + 8354352363536294558728287480449725021959591054502918814191302156889239
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_349 :
Polynomial.coeff recurrence2Scalar2Main 349 = -(658708750352099042077652902079075640717754004868983678274081398 * 10 ^ 70 + 592003779160617919119608231187762648767654617911886133839456612037362)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_350 :
Polynomial.coeff recurrence2Scalar2Main 350 = -(718610922935368930255760548893339138488142314564871344831922 * 10 ^ 70 + 2835539268720972558599025246439049172579075562539265143436862198241346)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_351 :
Polynomial.coeff recurrence2Scalar2Main 351 = 20801340065707979632504181495534192444946793376123281695882 * 10 ^ 70 + 8256524976152564332633482556875073344509137908825400037071271054367560
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_352 :
Polynomial.coeff recurrence2Scalar2Main 352 = -(19108656801445271136296517028763780604967525751014623195 * 10 ^ 70 + 874719077182893297602704816241399429896147991685338739348059826241168)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_353 :
Polynomial.coeff recurrence2Scalar2Main 353 = -(348475338041420902186173018141948862051051829879406377 * 10 ^ 70 + 2104061311576601032751930376920358986985953441929214990994594455182534)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_354 :
Polynomial.coeff recurrence2Scalar2Main 354 = 758651038459824977928643864555364521840211724364823 * 10 ^ 70 + 8166219520955626778721399757935022660080965759393945789536104480055205
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_355 :
Polynomial.coeff recurrence2Scalar2Main 355 = 2903525564102000211346089595576848807594022556931 * 10 ^ 70 + 9934021674515728750804223471736876301266523253373131462147472344883723
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_356 :
Polynomial.coeff recurrence2Scalar2Main 356 = -(10493511107294004193121499609540970450252531840 * 10 ^ 70 + 5397483772281406603460579183414271886264897117993891235707974987027814)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_357 :
Polynomial.coeff recurrence2Scalar2Main 357 = -(6383671674769245183443374984942631284840361 * 10 ^ 70 + 6894408667366659775361387118945913992092378260025735864075137633864524)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_358 :
Polynomial.coeff recurrence2Scalar2Main 358 = 64547624422058934119922521924432086024769 * 10 ^ 70 + 3917627655681924089440899830619229710755721178901421295677298080939521
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_359 :
Polynomial.coeff recurrence2Scalar2Main 359 = -(58635413568582134532486342604533092501 * 10 ^ 70 + 5975782201520571813273061086633679797181674927034534622381951380257122)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_360 :
Polynomial.coeff recurrence2Scalar2Main 360 = -(120396854680381786529443252712262867 * 10 ^ 70 + 6614917101736909736279792751894888373791120381206832063635398823874201)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_361 :
Polynomial.coeff recurrence2Scalar2Main 361 = 285650490443634016221650512667481 * 10 ^ 70 + 9212468555916688018224096354782420757048989499509761910087917273665430
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_362 :
Polynomial.coeff recurrence2Scalar2Main 362 = -(179899022256247105065369197532 * 10 ^ 70 + 3939860258294187887595173047953275666569026442140167035878950989955348)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_363 :
Polynomial.coeff recurrence2Scalar2Main 363 = -(46212236993502372905608775 * 10 ^ 70 + 1560944387032471545635261273953876539695391879036680781408342274919757)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_364 :
Polynomial.coeff recurrence2Scalar2Main 364 = 112774955298695335734638 * 10 ^ 70 + 4370962314920122341198235747776186017737073512333143548508083757073381
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_365 :
Polynomial.coeff recurrence2Scalar2Main 365 = -(53553483768967696044 * 10 ^ 70 + 8123357039964095564269792865224808010253904993891644009361400282293093)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_366 :
Polynomial.coeff recurrence2Scalar2Main 366 = 9496272400873665 * 10 ^ 70 + 1414932051215604017837861682346463975271057420728255736086477001483127
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_367 :
Polynomial.coeff recurrence2Scalar2Main 367 = -(76487871421 * 10 ^ 70 + 2366312323490153684099904590439724990542255361184021835999051289197600)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_368 :
Polynomial.coeff recurrence2Scalar2Main 368 = -(152740990 * 10 ^ 70 + 6516013435785885931879464744645842366354508688492464266899716933083109)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_369 :
Polynomial.coeff recurrence2Scalar2Main 369 = 15249 * 10 ^ 70 + 4633668897125039491675253057536378732479819568076575598313429673864825
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_370 :
Polynomial.coeff recurrence2Scalar2Main 370 = -4852891461631037485158354673243426376137614182082606129331967617673851
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_371 :
Polynomial.coeff recurrence2Scalar2Main 371 = 45016138001732307997056916346578126364754345055308768370937396834
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_372 :
Polynomial.coeff recurrence2Scalar2Main 372 = 201812463031397670734903090380708852211071786471815315834222
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_373 :
Polynomial.coeff recurrence2Scalar2Main 373 = -2556965889336893754564636540364248929695291549037498306
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_374 :
Polynomial.coeff recurrence2Scalar2Main 374 = 5696097295261880468386722689248325961965216045943
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_375 :
Polynomial.coeff recurrence2Scalar2Main 375 = -1894078624154296784583223519827014096385232
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_376 :
Polynomial.coeff recurrence2Scalar2Main 376 = 156951811428646099285082056055836978
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_377 :
Polynomial.coeff recurrence2Scalar2Main 377 = 1419194059250961434935930168
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_378 :
Polynomial.coeff recurrence2Scalar2Main 378 = -3539242852643699596
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_379 :
Polynomial.coeff recurrence2Scalar2Main 379 = 1911778728