Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar2ExceptionalPart1.Coefficients344To377

Recurrence 2 lookup certificate: Scalar2Exceptional 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.recurrence2Scalar2Exceptional_coeff_344 :
Polynomial.coeff recurrence2Scalar2Exceptional 344 = 12387351213659236688827127381171112846799816621661115770639299111840 * 10 ^ 70 + 5902240693279949211476556074035446755235851460301672558579320349859255
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_345 :
Polynomial.coeff recurrence2Scalar2Exceptional 345 = 494548013231565395394107373421615793511138909707598009537089575921 * 10 ^ 70 + 3034748068525241023522940557143326569051333117318741115595084901659581
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_346 :
Polynomial.coeff recurrence2Scalar2Exceptional 346 = 13365873373330739878179506549138585973177428841577903932735929243 * 10 ^ 70 + 2666511819353181512383642559429154305734432958482323157590951673630501
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_347 :
Polynomial.coeff recurrence2Scalar2Exceptional 347 = 264160985651744138756551342727776215151358686633982823516423887 * 10 ^ 70 + 5579500358120864219861411287218573380822193671604203952192937935085763
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_348 :
Polynomial.coeff recurrence2Scalar2Exceptional 348 = 3948995606126024970098649907620749511263851955910272821226198 * 10 ^ 70 + 9355177002011220713850889559874921706773609028049948168606566272191974
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_349 :
Polynomial.coeff recurrence2Scalar2Exceptional 349 = 45339652873347273149867910428040122752534126599380971127560 * 10 ^ 70 + 8653719969580976206665364906459004592575218925569135949224779488289980
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_350 :
Polynomial.coeff recurrence2Scalar2Exceptional 350 = 401307901716500964548974295605753104973619798333321795107 * 10 ^ 70 + 8242097586250307910562702375286408114539165670721226853587148958777407
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_351 :
Polynomial.coeff recurrence2Scalar2Exceptional 351 = 2719335999002904031005162749530880496401404482726734535 * 10 ^ 70 + 4993840098068632215930929389097336697496227500927478679652414130364459
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_352 :
Polynomial.coeff recurrence2Scalar2Exceptional 352 = 13795034372967129382657265828146525930857481106554678 * 10 ^ 70 + 5716063097865545784239903109754676841996864905055431331443050187237221
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_353 :
Polynomial.coeff recurrence2Scalar2Exceptional 353 = 49553170761641731863484230696599034569939122930788 * 10 ^ 70 + 7781818893157203091564039291023351765722657532902138818823503415218158
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_354 :
Polynomial.coeff recurrence2Scalar2Exceptional 354 = 105955811055547107893414390342643991025155706551 * 10 ^ 70 + 7244763397927060737108464853793426419393748196308448367556021958801914
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_355 :
Polynomial.coeff recurrence2Scalar2Exceptional 355 = 7779002332430986798519543214975032154800212 * 10 ^ 70 + 847884125149123577925845305778401845553841375813171038872049539711815
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_356 :
Polynomial.coeff recurrence2Scalar2Exceptional 356 = -(808551181130801562239590434121771772549477 * 10 ^ 70 + 5749003002019338954653013782067216339100296379665933870167525091491949)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_357 :
Polynomial.coeff recurrence2Scalar2Exceptional 357 = -(2754251321055780819019260661329039268617 * 10 ^ 70 + 210473544075210447684945372960852010129717301192866515659086881729078)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_358 :
Polynomial.coeff recurrence2Scalar2Exceptional 358 = -(3640057198288236179019275002568996126 * 10 ^ 70 + 1196357439218105547322658464425099995672100146339681821695956651339275)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_359 :
Polynomial.coeff recurrence2Scalar2Exceptional 359 = 2824238433225707664744922431106061 * 10 ^ 70 + 5734950421248152638906169625188004212011211753931374525279979169487106
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_360 :
Polynomial.coeff recurrence2Scalar2Exceptional 360 = 18994595696398195247723682660733 * 10 ^ 70 + 928873038737495368147183637558106952681297415601571134311113643941804
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_361 :
Polynomial.coeff recurrence2Scalar2Exceptional 361 = 29144579970527653714923396134 * 10 ^ 70 + 4130665300809468579287338449034406691646287766139051989645968266154668
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_362 :
Polynomial.coeff recurrence2Scalar2Exceptional 362 = 9053918625925141626809973 * 10 ^ 70 + 7135055268818391812362177671830363951676131520446059596989151666573241
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_363 :
Polynomial.coeff recurrence2Scalar2Exceptional 363 = -(35280548029742859454540 * 10 ^ 70 + 6358957843728032318865852295968139734841458333820183245904106306173142)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_364 :
Polynomial.coeff recurrence2Scalar2Exceptional 364 = -(63156253612457086367 * 10 ^ 70 + 8161120249499894513630170248451432351253829142799837560657556445338579)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_365 :
Polynomial.coeff recurrence2Scalar2Exceptional 365 = -(52829565754715974 * 10 ^ 70 + 9019211172547558201740171096710915743539120006494875860121405615200455)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_366 :
Polynomial.coeff recurrence2Scalar2Exceptional 366 = -(25842362623700 * 10 ^ 70 + 7036621456356761267183215270050486679792628521864636900469230871580923)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_367 :
Polynomial.coeff recurrence2Scalar2Exceptional 367 = -(7665325702 * 10 ^ 70 + 1323102776661730666047519427909966123087642633989179362324275719891139)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_368 :
Polynomial.coeff recurrence2Scalar2Exceptional 368 = -(1361718 * 10 ^ 70 + 2111718329293120772884893782566007878961251386021098287957266254066632)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_369 :
Polynomial.coeff recurrence2Scalar2Exceptional 369 = -(140 * 10 ^ 70 + 7225299108895109598663058466640247395724471499732668118017745440542151)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_370 :
Polynomial.coeff recurrence2Scalar2Exceptional 370 = -81868686228454203299039834674591618851832451577061332668030070126200
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_371 :
Polynomial.coeff recurrence2Scalar2Exceptional 371 = -2505467286567715828679445105200296487845655259314399725987942672
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_372 :
Polynomial.coeff recurrence2Scalar2Exceptional 372 = -35272625218556995847679522300422653934473812817667793754774
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_373 :
Polynomial.coeff recurrence2Scalar2Exceptional 373 = -210015516513919244718194431875260172136175321293110433
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_374 :
Polynomial.coeff recurrence2Scalar2Exceptional 374 = -558380106899000772440910619237484769080014123044
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_375 :
Polynomial.coeff recurrence2Scalar2Exceptional 375 = -589884556831854449741078234015576543128996
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_376 :
Polynomial.coeff recurrence2Scalar2Exceptional 376 = -111005000805264452755470793520906832
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_377 :
Polynomial.coeff recurrence2Scalar2Exceptional 377 = -845310990356491934016919003