Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar0LeftPart1.Coefficients346To386

Recurrence 2 lookup certificate: Scalar0Left 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.recurrence2Scalar0Left_coeff_346 :
Polynomial.coeff recurrence2Scalar0Left 346 = (602726364144 * 10 ^ 70 + 7720596109527255269028869902579108772043132088795189005292200594474130) * 10 ^ 70 + 9254159739036816547418072272234188452875779364151862871220027863386091
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_347 :
Polynomial.coeff recurrence2Scalar0Left 347 = (4818180112 * 10 ^ 70 + 7552807916779010608223894719688312284532503553551434503618973124024772) * 10 ^ 70 + 3421247249922822632825636787795228223625085900719836507464713770389989
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_348 :
Polynomial.coeff recurrence2Scalar0Left 348 = -((438609173 * 10 ^ 70 + 1917369725048479067322702343016266965065566800160853603760558462847693) * 10 ^ 70 + 4553344931418517145193815478687348128752591973100435277925219237175270)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_349 :
Polynomial.coeff recurrence2Scalar0Left 349 = (8172799 * 10 ^ 70 + 4966861413061417102450245583892166020421242790048688349769234698879584) * 10 ^ 70 + 5691736476195777064115557423715968669701550468363181010122560231802032
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_350 :
Polynomial.coeff recurrence2Scalar0Left 350 = -((23267 * 10 ^ 70 + 4610725156070776877087913982061843420586398264151109810030638503645306) * 10 ^ 70 + 2102758995459976005525701568659903724251604636096050056450884891570837)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_351 :
Polynomial.coeff recurrence2Scalar0Left 351 = -((1474 * 10 ^ 70 + 3436109901348210540877611100133878851643481777005778413100108684952535) * 10 ^ 70 + 2209940461431872960391627647023338577078118232920920056019500918996762)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_352 :
Polynomial.coeff recurrence2Scalar0Left 352 = (21 * 10 ^ 70 + 2320141916145840777933148322479745870666262126663741602044120865134071) * 10 ^ 70 + 2756837302400232102474323094393494043750974296301523884839639353433186
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_353 :
Polynomial.coeff recurrence2Scalar0Left 353 = -(31283622737869721844428422430697049791768818395365787944783458900813 * 10 ^ 70 + 1826977566619105078481075960256247184138828739085993962592914877077956)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_354 :
Polynomial.coeff recurrence2Scalar0Left 354 = -(20712939699920919781161904580841409585186214742908383244391213202834 * 10 ^ 70 + 4349277687707931919276718895802870175982910560794187991608672431490785)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_355 :
Polynomial.coeff recurrence2Scalar0Left 355 = 110119853462536740682318063962785199840063861765040551608059583076 * 10 ^ 70 + 8911580530512556496186425808727783278895720009010472069513919959690098
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_356 :
Polynomial.coeff recurrence2Scalar0Left 356 = 807866841954856872055661297878613716565879991085462955111547901 * 10 ^ 70 + 6023383611677053093222952290931366223347628057077416254885046917625331
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_357 :
Polynomial.coeff recurrence2Scalar0Left 357 = -(7641448080099108419549230501588343722359547364155662770373031 * 10 ^ 70 + 8950547462165429426748128321467116883397297119634000701275192155569383)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_358 :
Polynomial.coeff recurrence2Scalar0Left 358 = -(11478910450598998111811123740405834717185190256699555068733 * 10 ^ 70 + 9406996855655098609148495801152657332884586295451465272688789649783802)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_359 :
Polynomial.coeff recurrence2Scalar0Left 359 = 243120966036029580436782480625446491485763241173482593616 * 10 ^ 70 + 974544207310745696570709975777179663530498924492866533263150767641625
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_360 :
Polynomial.coeff recurrence2Scalar0Left 360 = -(138613397412489368589896817523413887254907015326079947 * 10 ^ 70 + 3278113333142488945808007631593838422492583509681729720255575186435681)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_361 :
Polynomial.coeff recurrence2Scalar0Left 361 = -(4127276135491631994824318902095658493529341322923568 * 10 ^ 70 + 4026692610149340294734435618819408165072105914044194070983723501549825)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_362 :
Polynomial.coeff recurrence2Scalar0Left 362 = 7517651384548606338218616520240456823526742125129 * 10 ^ 70 + 2729362270244790677934882111570574297083646447425599479788383085771604
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_363 :
Polynomial.coeff recurrence2Scalar0Left 363 = 35692804540470748533763939623158935657105382080 * 10 ^ 70 + 6601961465084447637946952634488573682500057632789685671616609138689168
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_364 :
Polynomial.coeff recurrence2Scalar0Left 364 = -(110673247875388126254444989626750632948448759 * 10 ^ 70 + 6533233184045514480554877577709476519744041029607514264675089310516604)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_365 :
Polynomial.coeff recurrence2Scalar0Left 365 = -(99476313832032804741351098359958755125651 * 10 ^ 70 + 9046536496211635913688463598185621647716888278367326277903318813010717)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_366 :
Polynomial.coeff recurrence2Scalar0Left 366 = 706970114857671076175737342246765459703 * 10 ^ 70 + 3623799852255835175440437290002835084505296085700537874029173956619767
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_367 :
Polynomial.coeff recurrence2Scalar0Left 367 = -(520170693036158563920977141204687180 * 10 ^ 70 + 2556349387547009422925617259160668948627071414394403057371076976017369)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_368 :
Polynomial.coeff recurrence2Scalar0Left 368 = -(1424947581553036619557858093853271 * 10 ^ 70 + 1501623529243635306028101762068622348294819716961703590663843333759496)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_369 :
Polynomial.coeff recurrence2Scalar0Left 369 = 2939394726691927269541260224317 * 10 ^ 70 + 6368771181641950845109764546405520789387130265460418427297109691441104
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_370 :
Polynomial.coeff recurrence2Scalar0Left 370 = -(1613487975609704182780794678 * 10 ^ 70 + 77770061524046726943080484031467854678257680800763140434873415704311)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_371 :
Polynomial.coeff recurrence2Scalar0Left 371 = -(631026964657470926901793 * 10 ^ 70 + 7211935126102909438307112977834321918308233337979550144027038865918835)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_372 :
Polynomial.coeff recurrence2Scalar0Left 372 = 1118107532394298380736 * 10 ^ 70 + 962160936849959688682661646046476558981865364658835613652418092859138
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_373 :
Polynomial.coeff recurrence2Scalar0Left 373 = -(479171976249628930 * 10 ^ 70 + 8060246407546055881077186596629329305094786395931786149297290244422616)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_374 :
Polynomial.coeff recurrence2Scalar0Left 374 = 74066801879720 * 10 ^ 70 + 5393913089967303228004112804203056973705485873499681212000017186691903
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_375 :
Polynomial.coeff recurrence2Scalar0Left 375 = 970864945 * 10 ^ 70 + 3009424948101878061726687189685969866900168829174656100113647963500142
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_376 :
Polynomial.coeff recurrence2Scalar0Left 376 = -(1314719 * 10 ^ 70 + 1616093944301141621699451930411492863398999175263717420162632617754145)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_377 :
Polynomial.coeff recurrence2Scalar0Left 377 = 109 * 10 ^ 70 + 5153536682224712461555173334163008397292481860953190654714748253647229
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_378 :
Polynomial.coeff recurrence2Scalar0Left 378 = -30702924267016725490650486023379308864570185634675172082413865355289
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_379 :
Polynomial.coeff recurrence2Scalar0Left 379 = 193637924496439561704066822450592910243002054890567563833694657
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_380 :
Polynomial.coeff recurrence2Scalar0Left 380 = 1331078207138453835966744528248787424416136493715184769404
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_381 :
Polynomial.coeff recurrence2Scalar0Left 381 = -13708128010898880438623614707092479808719596666307193
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_382 :
Polynomial.coeff recurrence2Scalar0Left 382 = 18751414389841545523553731614982178201543911010
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_383 :
Polynomial.coeff recurrence2Scalar0Left 383 = -6968666422007133725421629603848396585859
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_384 :
Polynomial.coeff recurrence2Scalar0Left 384 = -11169886686358548984931405851122
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_385 :
Polynomial.coeff recurrence2Scalar0Left 385 = 1109519187941616171668366
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_386 :
Polynomial.coeff recurrence2Scalar0Left 386 = -4877303983489137