Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar1MainPart1.Coefficients340To380

Recurrence 2 lookup certificate: Scalar1Main 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.recurrence2Scalar1Main_coeff_340 :
Polynomial.coeff recurrence2Scalar1Main 340 = (16154575075469365 * 10 ^ 70 + 2228682994987135847944285400966312830082717888924584770544885523542532) * 10 ^ 70 + 6631576097808685093232751989779412271728578154236717476722185171187422
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_341 :
Polynomial.coeff recurrence2Scalar1Main 341 = -((552125512152198 * 10 ^ 70 + 6828820917938830733347366309051706973636324520926287369373836536677723) * 10 ^ 70 + 7425956892736931283297490866174833231883994130086010613883094429152166)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_342 :
Polynomial.coeff recurrence2Scalar1Main 342 = (7998929798936 * 10 ^ 70 + 2524725959550727756273989685947478394325490081250532286585730582422724) * 10 ^ 70 + 7710498554034662541223639863663337474839996311505638577313859743842960
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_343 :
Polynomial.coeff recurrence2Scalar1Main 343 = (92716453860 * 10 ^ 70 + 6992172571158352268101914206185175833002624392450396335916917816096830) * 10 ^ 70 + 7802852383615195284179027213981968318584849339393464789089977114200152
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_344 :
Polynomial.coeff recurrence2Scalar1Main 344 = -((6594252969 * 10 ^ 70 + 2216330010067704917700606199570515634832734475427076637151608351255612) * 10 ^ 70 + 221679668780823104016343794705205830671124678634719314287675065062241)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_345 :
Polynomial.coeff recurrence2Scalar1Main 345 = (116913337 * 10 ^ 70 + 7430987339465572828146556615369847657037042834573213915605770684407981) * 10 ^ 70 + 4893304609478257444858399544171137427262514385342593641927718635723381
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_346 :
Polynomial.coeff recurrence2Scalar1Main 346 = -((277613 * 10 ^ 70 + 4289575186621364036903975412626874430117967108040097601326946040588895) * 10 ^ 70 + 7180662390707937610061674275453688339996065784108715116653969555142948)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_347 :
Polynomial.coeff recurrence2Scalar1Main 347 = -((21726 * 10 ^ 70 + 4500067162658006953240212662583719943152870625018446763880003191690086) * 10 ^ 70 + 8205421186641873738385901997200806067918050315470664246706108292313476)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_348 :
Polynomial.coeff recurrence2Scalar1Main 348 = (305 * 10 ^ 70 + 3285976192977904300165054967579245300920150102144102160418249779142034) * 10 ^ 70 + 5981868798345560033861522135672042578464622260214900621860965441052939
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_349 :
Polynomial.coeff recurrence2Scalar1Main 349 = -(255023266462677687949570533108224831433359340567343516724690958280458 * 10 ^ 70 + 501692446628863974561248068471376409520406390648765141364615653803564)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_350 :
Polynomial.coeff recurrence2Scalar1Main 350 = -(299304685398778295525225438762974471459629214395928440869661364241656 * 10 ^ 70 + 8837975700467144115851499940305453607984085061141144145097173347842733)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_351 :
Polynomial.coeff recurrence2Scalar1Main 351 = 1607212397546147470277788975821157583447943226946169064288850895769 * 10 ^ 70 + 3150609636485080074440558144045711475798200163920292707800797951284393
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_352 :
Polynomial.coeff recurrence2Scalar1Main 352 = 11532797458167162029950568694302783251446793038655386277153441426 * 10 ^ 70 + 8243928610604246836844156406693159650618174140219949167514507100756040
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_353 :
Polynomial.coeff recurrence2Scalar1Main 353 = -(111921552642742853904359172789813822888825730909825745820892112 * 10 ^ 70 + 6578904562340013700008481459594040907359746494392871473143715315805234)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_354 :
Polynomial.coeff recurrence2Scalar1Main 354 = -(153276986337063196275532505656109961948938233999288230872568 * 10 ^ 70 + 2542983311637004514584377648345849766729737831804470686208559313750161)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_355 :
Polynomial.coeff recurrence2Scalar1Main 355 = 3558662190064658618160194758910578976744361229343438657262 * 10 ^ 70 + 2563258465426575088084156715024279927997483246423985115924995481787132
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_356 :
Polynomial.coeff recurrence2Scalar1Main 356 = -(2468590183060302174674969455162366468680161395885404269 * 10 ^ 70 + 4234955954580544312370749889911665660849827216188559269378285888227479)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_357 :
Polynomial.coeff recurrence2Scalar1Main 357 = -(60204690331842834994209773787725476393871423790111855 * 10 ^ 70 + 3985099978084661859588765477417015370495342924707826389143195883482637)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_358 :
Polynomial.coeff recurrence2Scalar1Main 358 = 117392116005878349529302266062121015888140109148494 * 10 ^ 70 + 7055470987409052949433853256871688485155665203848211975063122826277902
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_359 :
Polynomial.coeff recurrence2Scalar1Main 359 = 514021931773066408557419041919426281797503412351 * 10 ^ 70 + 4463339835268052188805937361325208477632930418349155352034599891665059
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_360 :
Polynomial.coeff recurrence2Scalar1Main 360 = -(1688319288914077861132209179289751178695044690 * 10 ^ 70 + 9209085032029179976703412396123178384606214812306845697959499849222874)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_361 :
Polynomial.coeff recurrence2Scalar1Main 361 = -(1324371976306264655164873305221428035148249 * 10 ^ 70 + 7404923124811930019725713068494866019129331433321020147256721786059729)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_362 :
Polynomial.coeff recurrence2Scalar1Main 362 = 10636030761453979689212503384152804234955 * 10 ^ 70 + 1854415116944574989769725640984161092963918075211170545258342029886627
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_363 :
Polynomial.coeff recurrence2Scalar1Main 363 = -(8537176014618503039291488575504032301 * 10 ^ 70 + 5124643929346089275027784188248228410358163040784307271925987716495935)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_364 :
Polynomial.coeff recurrence2Scalar1Main 364 = -(20833364884807867081566465475813569 * 10 ^ 70 + 5502539424804837572628025700237095345319074065533007791695181376533682)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_365 :
Polynomial.coeff recurrence2Scalar1Main 365 = 45344066302479503706069207564273 * 10 ^ 70 + 5938408589883540422755543450498130755547636781994440523780186208360983
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_366 :
Polynomial.coeff recurrence2Scalar1Main 366 = -(26348654263148535796765589022 * 10 ^ 70 + 8596372241128746551227296579203451412166228351078043082486294803759525)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_367 :
Polynomial.coeff recurrence2Scalar1Main 367 = -(8794114326128746361480533 * 10 ^ 70 + 9636358131368919596620743056425236604937436377444990320864026851288284)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_368 :
Polynomial.coeff recurrence2Scalar1Main 368 = 17524038748515487788193 * 10 ^ 70 + 9950650506267910206229009464758802755798660615509707504223275025334442
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_369 :
Polynomial.coeff recurrence2Scalar1Main 369 = -(7820265960553442480 * 10 ^ 70 + 8147063015890297590954470001783686516431444126262720346787777153371130)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_370 :
Polynomial.coeff recurrence2Scalar1Main 370 = 1284062138148437 * 10 ^ 70 + 2937172338891122596482251604224861175591479805839106153108802119817096
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_371 :
Polynomial.coeff recurrence2Scalar1Main 371 = 6056773305 * 10 ^ 70 + 4376143428844497661836083984271269543245720365111271753577841060401837
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_372 :
Polynomial.coeff recurrence2Scalar1Main 372 = -(21730737 * 10 ^ 70 + 8368203681559182759958593108605614464334983719335070636208312972429622)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_373 :
Polynomial.coeff recurrence2Scalar1Main 373 = 1971 * 10 ^ 70 + 6412474866066035204641552036575141170616240814378935948130652802991478
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_374 :
Polynomial.coeff recurrence2Scalar1Main 374 = -572606090269610926200079869496753797698513187349143131732852629980405
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_375 :
Polynomial.coeff recurrence2Scalar1Main 375 = 4538895923742927442863247914666917054513848007748787677190147260
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_376 :
Polynomial.coeff recurrence2Scalar1Main 376 = 27254968769581522096998684086205648522251257357628257996792
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_377 :
Polynomial.coeff recurrence2Scalar1Main 377 = -265319237024263686274044497625793639446160394747550923
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_378 :
Polynomial.coeff recurrence2Scalar1Main 378 = 500649091397656411914350428601274543111479793877
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_379 :
Polynomial.coeff recurrence2Scalar1Main 379 = -137363268378719150678779313362487539087671
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_380 :
Polynomial.coeff recurrence2Scalar1Main 380 = 7643129673958697547995641780269088