Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar1LeftPart1.Coefficients343To382

Recurrence 2 lookup certificate: Scalar1Left 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.recurrence2Scalar1Left_coeff_343 :
Polynomial.coeff recurrence2Scalar1Left 343 = (106264274480 * 10 ^ 70 + 6814571411831109442097630577851672612578973665324173530603072982484713) * 10 ^ 70 + 7033000864214577513421234083421666422936253552315035285686725316243046
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_344 :
Polynomial.coeff recurrence2Scalar1Left 344 = -((6773822134 * 10 ^ 70 + 1208055943011889721969979349929217521630699335378258079091890354113073) * 10 ^ 70 + 564275985053379270083922548192863272618229472416000878827773788759590)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_345 :
Polynomial.coeff recurrence2Scalar1Left 345 = (115204801 * 10 ^ 70 + 916750315939395323486123926520236980729331234154091860215923582694794) * 10 ^ 70 + 8314343038446995699386337480718303786899549240086030800334209859008054
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_346 :
Polynomial.coeff recurrence2Scalar1Left 346 = -((185168 * 10 ^ 70 + 7608737901709738504995726016344987255093541378586561074956636959409744) * 10 ^ 70 + 540831936404928181263316960635098852102467999617789081519417019205912)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_347 :
Polynomial.coeff recurrence2Scalar1Left 347 = -((22716 * 10 ^ 70 + 6520471649816162352469697509907477707299691745013470900811334146786833) * 10 ^ 70 + 8774129284505129237569060117821983399553750740480041381584495865192609)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_348 :
Polynomial.coeff recurrence2Scalar1Left 348 = (299 * 10 ^ 70 + 8046358907122865094747147574037631311535667934190232773611408904717691) * 10 ^ 70 + 6642446012654270393025534641472356023229090635782801743391414543124200
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_349 :
Polynomial.coeff recurrence2Scalar1Left 349 = 1661529392045342920589503043931423136736819798137077556374492459807848 * 10 ^ 70 + 2436113604810112537242192063866259839102645020323643872604848302930636
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_350 :
Polynomial.coeff recurrence2Scalar1Left 350 = -(306560041174230283385781006461806793795785011341724471632775664045835 * 10 ^ 70 + 4941204032364684524998292441000016278058282581446871340606580401195456)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_351 :
Polynomial.coeff recurrence2Scalar1Left 351 = 1483988204364485642267623385260842581020762459629617011966382624530 * 10 ^ 70 + 1940631115509578575991325943531757562035288423436844609918195778105300
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_352 :
Polynomial.coeff recurrence2Scalar1Left 352 = 12484784953844247101068443148451583988335020946150549824604400518 * 10 ^ 70 + 2272895139536038557851434021368729309922781731459253841768520976314171
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_353 :
Polynomial.coeff recurrence2Scalar1Left 353 = -(108444735861353135398573582447123053165023735362146350409398534 * 10 ^ 70 + 8850901514931400834545368418637371638593228018801958827264676764594276)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_354 :
Polynomial.coeff recurrence2Scalar1Left 354 = -(198546443330854306920608291977535714257656879950753619706609 * 10 ^ 70 + 3354785746679001002073996312016841069613250573316573803005617162703134)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_355 :
Polynomial.coeff recurrence2Scalar1Left 355 = 3533092496281111610530569492243224340236122323345857175653 * 10 ^ 70 + 791133485888543526732643720633571724967333533696035943014340214871653
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_356 :
Polynomial.coeff recurrence2Scalar1Left 356 = -(1334581073622290943019353046975195873992757145368687145 * 10 ^ 70 + 7621928043829566978061224151962610635138155030492842014438684488504129)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_357 :
Polynomial.coeff recurrence2Scalar1Left 357 = -(61178079857049879818727475619836345211050251990085862 * 10 ^ 70 + 6109772442298649455107713720051587628588915948204253015515804094736307)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_358 :
Polynomial.coeff recurrence2Scalar1Left 358 = 101863641604662185166095913114297738300073827341095 * 10 ^ 70 + 1929327895797719681069331902021818649665395202840210057646083687966445
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_359 :
Polynomial.coeff recurrence2Scalar1Left 359 = 543632657445540180848155799433408414098079799526 * 10 ^ 70 + 6039679593768246779986596967288036606666542132122838975862455258964776
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_360 :
Polynomial.coeff recurrence2Scalar1Left 360 = -(1581492731051800337945189574321481388688414195 * 10 ^ 70 + 9999135845263102378665107603779869105478027018729654117585646908579636)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_361 :
Polynomial.coeff recurrence2Scalar1Left 361 = -(1661591362279879300203042301222871157755761 * 10 ^ 70 + 8047718337245325620075630431010492644803556948769179328176288863624101)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_362 :
Polynomial.coeff recurrence2Scalar1Left 362 = 10451097340937136780988049522535958054789 * 10 ^ 70 + 2784015276771513116836523708815495841682574840814643236979912745420793
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_363 :
Polynomial.coeff recurrence2Scalar1Left 363 = -(6899419781331775984097392496405021761 * 10 ^ 70 + 4119269852094484666854185999283575629261995519270629855228936115830358)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_364 :
Polynomial.coeff recurrence2Scalar1Left 364 = -(22264049293086948498261270543406538 * 10 ^ 70 + 9054051603512060521914276982680991988628670736888599082972204676021499)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_365 :
Polynomial.coeff recurrence2Scalar1Left 365 = 43443752249319651849818465715779 * 10 ^ 70 + 6528461119203300032668445556118774772252035936757187477515868892222783
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_366 :
Polynomial.coeff recurrence2Scalar1Left 366 = -(22044493277373077708533220279 * 10 ^ 70 + 7094259472079768524471023760466546288148620670552616583573732002828730)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_367 :
Polynomial.coeff recurrence2Scalar1Left 367 = -(11417795327328533739765206 * 10 ^ 70 + 7435624760855465633179476002734039508497043571585100709247785421106418)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_368 :
Polynomial.coeff recurrence2Scalar1Left 368 = 17534494197285032405327 * 10 ^ 70 + 5850637300370924194983582853678949354808141236547493925312256191556762
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_369 :
Polynomial.coeff recurrence2Scalar1Left 369 = -(7227779281161761332 * 10 ^ 70 + 5416526989168185293702358306918043270733188202013245877059789911584265)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_370 :
Polynomial.coeff recurrence2Scalar1Left 370 = 1042365782994375 * 10 ^ 70 + 5013418936273119362540610719861773286020809191363839777044828746534485
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_371 :
Polynomial.coeff recurrence2Scalar1Left 371 = 37286950366 * 10 ^ 70 + 2916546670396859963575282653113955981342342874577625252099111045397863
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_372 :
Polynomial.coeff recurrence2Scalar1Left 372 = -(22598184 * 10 ^ 70 + 163097564421896482569356380841355470249147306567749162781343411235572)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_373 :
Polynomial.coeff recurrence2Scalar1Left 373 = 1788 * 10 ^ 70 + 23912892842298209354797097907871075162094997887473734715513562294960
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_374 :
Polynomial.coeff recurrence2Scalar1Left 374 = -478354278313389548554022920687404751858210225727591483780855293785114
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_375 :
Polynomial.coeff recurrence2Scalar1Left 375 = 2347267816208257567220119095299943492493239857106206617712059345
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_376 :
Polynomial.coeff recurrence2Scalar1Left 376 = 31585866679297875487463985494902096537277018173364795849734
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_377 :
Polynomial.coeff recurrence2Scalar1Left 377 = -267987244507918947146469427044684512830104417651449311
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_378 :
Polynomial.coeff recurrence2Scalar1Left 378 = 355161228661028715299657031966939635130671351374
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_379 :
Polynomial.coeff recurrence2Scalar1Left 379 = -126509314574720340110135742133306327146064
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_380 :
Polynomial.coeff recurrence2Scalar1Left 380 = -2566123251051757354072909453836390
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_381 :
Polynomial.coeff recurrence2Scalar1Left 381 = 52493199771550849605501044
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_382 :
Polynomial.coeff recurrence2Scalar1Left 382 = -199284929430635089