Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupB2A4Part1.Coefficients310To346

Recurrence 4 lookup certificate: B2A4 coefficient convolution #

This is a checked coefficient-lookup shard for the fourth pseudo-division recurrence in the order-seven certificate.

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_310 :
Polynomial.coeff recurrence4B2A4 310 = -((2426879 * 10 ^ 70 + 7005241794406031254001876774281616385355382098172599886296188015900363) * 10 ^ 70 + 7646088731700536798726260509619813173455968331016854581297898312641864)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_311 :
Polynomial.coeff recurrence4B2A4 311 = (953617 * 10 ^ 70 + 8645877872853929176137989013666584011019410402809075598280603733948241) * 10 ^ 70 + 1879080357353008548068499562444643369207029449219059514058519222562420
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_312 :
Polynomial.coeff recurrence4B2A4 312 = -((93203 * 10 ^ 70 + 2849279524029239157603389191220187307931978251671373989005803263603382) * 10 ^ 70 + 6422055436972905115337216294101584275959337619638337487362983821461378)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_313 :
Polynomial.coeff recurrence4B2A4 313 = (4843 * 10 ^ 70 + 3156732422056183609708259696817933235547458208570340891689383783366612) * 10 ^ 70 + 1330429343799815802372252422679826897527783810160774209003299553716813
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_314 :
Polynomial.coeff recurrence4B2A4 314 = -((68 * 10 ^ 70 + 4140051148764314415622918823790690603989639265264417063863540557702250) * 10 ^ 70 + 2078801828714260169753575420338647767947142327082457487619822451476529)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_315 :
Polynomial.coeff recurrence4B2A4 315 = -((9 * 10 ^ 70 + 2919673529546381730504313083152311422790624548799257258428519977148671) * 10 ^ 70 + 5415845829084746931045846917932197046391735237734454936997338088588322)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_316 :
Polynomial.coeff recurrence4B2A4 316 = 6981075558843972923959043129157107281919279637579487702009532194894696 * 10 ^ 70 + 2533221282039255847449706494749761800056403394164716970273343957060138
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_317 :
Polynomial.coeff recurrence4B2A4 317 = -(153260271017824119043491764829248609887315415097629977248135424067217 * 10 ^ 70 + 678000704885915716709846660457514496594338328278073901264226550170757)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_318 :
Polynomial.coeff recurrence4B2A4 318 = -(4312819256342646595360912549053798113015763832502801997501190209102 * 10 ^ 70 + 8897130006449086456967164584948130009691192753214252851971590646181685)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_319 :
Polynomial.coeff recurrence4B2A4 319 = 254628762576869696739118369269542170846058949328207630191638150747 * 10 ^ 70 + 7935939686383188159408617938650859429563848880606997840484357059333151
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_320 :
Polynomial.coeff recurrence4B2A4 320 = -(35651516526360356051641037949440855580479276500190432099966880 * 10 ^ 70 + 1070185375300751501271111839665228224321521443011378502226414183644586)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_321 :
Polynomial.coeff recurrence4B2A4 321 = -(130737908207730229776037945259429197231096328189770819789366746 * 10 ^ 70 + 9989082132834056188685270539237535300037143557945997454737822844589944)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_322 :
Polynomial.coeff recurrence4B2A4 322 = -(564440026347254940793009196366959802519537011901391133572922 * 10 ^ 70 + 499280432588684211684679188604222845612169213805900448980755355620947)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_323 :
Polynomial.coeff recurrence4B2A4 323 = 18788302206621630086648019558506813858382315252774485058652 * 10 ^ 70 + 7047650544165872695510848921211853781694422666819840797006182029334569
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_324 :
Polynomial.coeff recurrence4B2A4 324 = 187090783483944631357069287773962056234610439607932355652 * 10 ^ 70 + 2852085137750738813926655554596135642513001606373590079662527643836907
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_325 :
Polynomial.coeff recurrence4B2A4 325 = 124373934960997919063109968673268645696976391060340545 * 10 ^ 70 + 6118313469148574056292300211738784235458376610878514481069838471432465
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_326 :
Polynomial.coeff recurrence4B2A4 326 = -(4948528611825188672386914355707747553592431860564250 * 10 ^ 70 + 3499859765255646494014511700034599210999449909260596071061432154586320)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_327 :
Polynomial.coeff recurrence4B2A4 327 = -(17679679668544563604902579989534977432456270748474 * 10 ^ 70 + 3959799275897437590376029383667182896489173541390800311273989892847034)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_328 :
Polynomial.coeff recurrence4B2A4 328 = 18533514375464068808609940178496099773360282478 * 10 ^ 70 + 3153947049721735009560672353723236495123244828837827356219083977186960
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_329 :
Polynomial.coeff recurrence4B2A4 329 = 164709408490153736642074785526524898779350322 * 10 ^ 70 + 4951613071870204153034809560842782040788115498347130660719797456315211
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_330 :
Polynomial.coeff recurrence4B2A4 330 = 61057170048032934196926569993608743373440 * 10 ^ 70 + 1437626296383670928426018839504505620147841765784784443749177235351617
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_331 :
Polynomial.coeff recurrence4B2A4 331 = -(572242622251129708041069151467829450155 * 10 ^ 70 + 9756592586475286540963918760559596217884361544344479799388212414539761)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_332 :
Polynomial.coeff recurrence4B2A4 332 = -(377261593122582386554150624852513019 * 10 ^ 70 + 4898762851610150835869404058381015016498520644578598294835072188272599)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_333 :
Polynomial.coeff recurrence4B2A4 333 = 774017192556181594649884759250814 * 10 ^ 70 + 3536723498260231809130676252872744998696364719860609029849643820502627
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_334 :
Polynomial.coeff recurrence4B2A4 334 = 445254129689738669024291137074 * 10 ^ 70 + 4942055974573176741980757157998381958591022013603036725986252448234055
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_335 :
Polynomial.coeff recurrence4B2A4 335 = -(211020017000042375387498476 * 10 ^ 70 + 2718615325381931145053786548474051974892720556639475950110273719714352)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_336 :
Polynomial.coeff recurrence4B2A4 336 = -(73307669320134453506466 * 10 ^ 70 + 1238985107099445961648116298173093140312277404241953514443288013287510)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_337 :
Polynomial.coeff recurrence4B2A4 337 = 5594648076139424798 * 10 ^ 70 + 7958652502912171488851280403286461943252743796258086056742597433596462
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_338 :
Polynomial.coeff recurrence4B2A4 338 = 988142602102956 * 10 ^ 70 + 6441175207260761708862216806934574274019941627550929742044557509510339
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_339 :
Polynomial.coeff recurrence4B2A4 339 = -(8701298836 * 10 ^ 70 + 9830241641612214648367887198325367518288287661905002485961690601331236)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_340 :
Polynomial.coeff recurrence4B2A4 340 = -(728020 * 10 ^ 70 + 8867836846495308044276361987838315667169963267641876312853503563239516)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_341 :
Polynomial.coeff recurrence4B2A4 341 = 3185543875939114963364936652804658032464191347705789672736416071466453
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_342 :
Polynomial.coeff recurrence4B2A4 342 = 159440874692401052299120222210323802881303753869109880618637329801
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_343 :
Polynomial.coeff recurrence4B2A4 343 = 3892928270344226532973363258922245384633289925025687392201
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_344 :
Polynomial.coeff recurrence4B2A4 344 = -36545089356850225515065744663586451481290633989024751
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_345 :
Polynomial.coeff recurrence4B2A4 345 = 49421852271526131723191755307298837574818749
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_346 :
Polynomial.coeff recurrence4B2A4 346 = 8644687378941815133797349621600670141