Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar4MainPart1.Coefficients332To371

Recurrence 2 lookup certificate: Scalar4Main 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.recurrence2Scalar4Main_coeff_332 :
Polynomial.coeff recurrence2Scalar4Main 332 = -((149674259055 * 10 ^ 70 + 6837132372323569187050579323740934512328060461047704849127805719009650) * 10 ^ 70 + 9212275501921088501564904554870624486082303355067150669952451969861863)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_333 :
Polynomial.coeff recurrence2Scalar4Main 333 = (2778826780 * 10 ^ 70 + 8269975314009219716930860566730614241076851812372285401559927465493407) * 10 ^ 70 + 8053045607798327698482664895390519443736466196366189273822378089124033
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_334 :
Polynomial.coeff recurrence2Scalar4Main 334 = -((10317356 * 10 ^ 70 + 220693548602020449969876738804150316334169010859477984848027335900875) * 10 ^ 70 + 825829699815110115548197092020113538943571447904807467640323466853824)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_335 :
Polynomial.coeff recurrence2Scalar4Main 335 = -((466168 * 10 ^ 70 + 592020954071259713624506023697179700968393337018327460125314315627783) * 10 ^ 70 + 3460374679281993814635908192608991518647106409794891839964022785445562)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_336 :
Polynomial.coeff recurrence2Scalar4Main 336 = (7672 * 10 ^ 70 + 8218894079877629693416872468432592603237888947879514609923207578777790) * 10 ^ 70 + 4494584904154253336647507836856894259269913000914854717344473882153104
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_337 :
Polynomial.coeff recurrence2Scalar4Main 337 = -((13 * 10 ^ 70 + 9279436753550193310022080342645460520700739277217312106640716756102310) * 10 ^ 70 + 6202001131364272250544137632032721118031177174215794930620854947317471)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_338 :
Polynomial.coeff recurrence2Scalar4Main 338 = -(6768901112796948330797364816067754188532295582035801020535642476213945 * 10 ^ 70 + 3463518671208485934256562951130370281985639053355478438782870494532804)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_339 :
Polynomial.coeff recurrence2Scalar4Main 339 = 50047998480221614142670129055170913048959860830186695623695658603553 * 10 ^ 70 + 3008989383834671762717490855283444131258367942248017998957973967776277
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_340 :
Polynomial.coeff recurrence2Scalar4Main 340 = 203238382400772743897243569845242412211683060419604913152000153464 * 10 ^ 70 + 747564446412864056635367728822597939645119075268417412471991558468102
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_341 :
Polynomial.coeff recurrence2Scalar4Main 341 = -(3161818840757676793503188423627757447001853830161005964664242692 * 10 ^ 70 + 4988100134336171079492513402165815892672471738776132086575902242560244)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_342 :
Polynomial.coeff recurrence2Scalar4Main 342 = 608641907750130987679017566128061465169305005824196896453586 * 10 ^ 70 + 1369633015939684980643063807154494206457580667730875773897909803580076
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_343 :
Polynomial.coeff recurrence2Scalar4Main 343 = 95174457914842574603775525304973426082444829424988714861235 * 10 ^ 70 + 7868791639805772105873029451879385561995216403925366543817779985529031
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_344 :
Polynomial.coeff recurrence2Scalar4Main 344 = -(187644952346744226541368696809696355057616735442224697855 * 10 ^ 70 + 182796013902788653070944896191259663269717981431486848587137595367218)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_345 :
Polynomial.coeff recurrence2Scalar4Main 345 = -(1501728935330941176331480042132382471071653744855757928 * 10 ^ 70 + 1063635831527891055082783630517633016674478752042495247253591014655046)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_346 :
Polynomial.coeff recurrence2Scalar4Main 346 = 4978473138228283607848265821256543165102011323715498 * 10 ^ 70 + 3532763147724641073706692085020083274389212168531233070020573451153762
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_347 :
Polynomial.coeff recurrence2Scalar4Main 347 = 10782825954559814152491654222237200769510731561315 * 10 ^ 70 + 3074961544216308119625323122573706059570416259568304419464522097845031
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_348 :
Polynomial.coeff recurrence2Scalar4Main 348 = -(60484886024567935011333062453894764355837110242 * 10 ^ 70 + 1281944126283898995771553853480706224833416397510387981566631979069603)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_349 :
Polynomial.coeff recurrence2Scalar4Main 349 = 2239761998168885905795736546945522933019215 * 10 ^ 70 + 9425849089505732770561719368181963757429868549681064870440899411525664
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_350 :
Polynomial.coeff recurrence2Scalar4Main 350 = 338008142964102138783900097877450502615595 * 10 ^ 70 + 9036882433461452293682954520803773661261083957710232864064157103693454
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_351 :
Polynomial.coeff recurrence2Scalar4Main 351 = -(460184617602511168694197846339400879945 * 10 ^ 70 + 9659641614347398656285451358836356205686076860419058845060605382703361)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_352 :
Polynomial.coeff recurrence2Scalar4Main 352 = -(486854329370610717393301034315004317 * 10 ^ 70 + 9472197179508159351327156926431611401194423563101334452012770787045702)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_353 :
Polynomial.coeff recurrence2Scalar4Main 353 = 1732227423464865457183261658892127 * 10 ^ 70 + 940259075485114255254075349954703798842411914377244017959111212815079
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_354 :
Polynomial.coeff recurrence2Scalar4Main 354 = -(1429458550822710305424495862725 * 10 ^ 70 + 8107677116858646672045485930020969755578052475563289170490236255830730)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_355 :
Polynomial.coeff recurrence2Scalar4Main 355 = -(38562479733890366927029680 * 10 ^ 70 + 1474873125368188037379622476358145628046575847395778584123031904457894)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_356 :
Polynomial.coeff recurrence2Scalar4Main 356 = 734047538805810172717340 * 10 ^ 70 + 5540368490600061551311631819586188274563785874661426940061201719702669
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_357 :
Polynomial.coeff recurrence2Scalar4Main 357 = -(438639267058510527736 * 10 ^ 70 + 1702399951526991322180180772658904217557268924622096558071761118395124)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_358 :
Polynomial.coeff recurrence2Scalar4Main 358 = 99227501656948566 * 10 ^ 70 + 1737315898521566094474859737354080885511086537264534434612901512215316
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_359 :
Polynomial.coeff recurrence2Scalar4Main 359 = -(4747341365349 * 10 ^ 70 + 5520043144077886441733598688614420192205479046223753563237582053500941)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_360 :
Polynomial.coeff recurrence2Scalar4Main 360 = -(1316674573 * 10 ^ 70 + 9665998426507440038218392018956230804629969401873793898302148231621339)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_361 :
Polynomial.coeff recurrence2Scalar4Main 361 = 185250 * 10 ^ 70 + 4049915846592588213863773271466526337372713361270009496420176218542802
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_362 :
Polynomial.coeff recurrence2Scalar4Main 362 = -(7 * 10 ^ 70 + 8319477727698935084646778029265032085700797311552944892273117685568066)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_363 :
Polynomial.coeff recurrence2Scalar4Main 363 = 1072590899515031018907349360100202923947214905133029305224169940628
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_364 :
Polynomial.coeff recurrence2Scalar4Main 364 = 792142129488169604722547024201125960536183086058333661577722
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_365 :
Polynomial.coeff recurrence2Scalar4Main 365 = -59479285883399135928086547514117232773062183002721438917
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_366 :
Polynomial.coeff recurrence2Scalar4Main 366 = 202120554071303608419766685783396308385373365315958
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_367 :
Polynomial.coeff recurrence2Scalar4Main 367 = -118239830108327367970173248835837267573366070
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_368 :
Polynomial.coeff recurrence2Scalar4Main 368 = 16947566945305068876048021264578210060
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_369 :
Polynomial.coeff recurrence2Scalar4Main 369 = 111104464423783079712050603284
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_370 :
Polynomial.coeff recurrence2Scalar4Main 370 = -672793960729382441168
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_371 :
Polynomial.coeff recurrence2Scalar4Main 371 = 631370089744