Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupA4SquarePart0.Coefficients0To69

Recurrence 4 lookup certificate: A4Square 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.recurrence4A4Square_coeff_0 :
Polynomial.coeff recurrence4A4Square 0 = 148021789696
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_1 :
Polynomial.coeff recurrence4A4Square 1 = -427842316979968
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_2 :
Polynomial.coeff recurrence4A4Square 2 = -353249410707235440
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_3 :
Polynomial.coeff recurrence4A4Square 3 = 1717494371245297057808
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_4 :
Polynomial.coeff recurrence4A4Square 4 = -465779060122729549493484
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_5 :
Polynomial.coeff recurrence4A4Square 5 = -1560002716544997716614732768
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_6 :
Polynomial.coeff recurrence4A4Square 6 = 1242487726523214483709488418128
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_7 :
Polynomial.coeff recurrence4A4Square 7 = -245545287342814637297941293063716
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_8 :
Polynomial.coeff recurrence4A4Square 8 = -25033201182462074600222702570656635
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_9 :
Polynomial.coeff recurrence4A4Square 9 = 9875920664515501296764794605564444276
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_10 :
Polynomial.coeff recurrence4A4Square 10 = 1138854270323942327991259036836003404790
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_11 :
Polynomial.coeff recurrence4A4Square 11 = -863335021728656556914413624207044082999714
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_12 :
Polynomial.coeff recurrence4A4Square 12 = 244887380994046862782991058113134748681098341
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_13 :
Polynomial.coeff recurrence4A4Square 13 = -56131203277605832225004761397076172069752040616
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_14 :
Polynomial.coeff recurrence4A4Square 14 = 10199383750323007119229822233373139521144275025377
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_15 :
Polynomial.coeff recurrence4A4Square 15 = -1493854885895251672689070305521876408946782439072336
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_16 :
Polynomial.coeff recurrence4A4Square 16 = 235209385074561622161184413127582273796747881946364034
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_17 :
Polynomial.coeff recurrence4A4Square 17 = -59227865196703722859695512602528279601299001257326887312
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_18 :
Polynomial.coeff recurrence4A4Square 18 = 18933797018402706125356206926955818920370344009859550870075
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_19 :
Polynomial.coeff recurrence4A4Square 19 = -5551668634933289647327646217118214927980128300983897577418350
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_20 :
Polynomial.coeff recurrence4A4Square 20 = 1392609293560938537857287271891678525528422403968573418287992164
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_21 :
Polynomial.coeff recurrence4A4Square 21 = -301638371394444593681176886553808242419191059534352301611500363648
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_22 :
Polynomial.coeff recurrence4A4Square 22 = 57382130648246866423856034797781051913838093079916165684127820533189
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_23 :
Polynomial.coeff recurrence4A4Square 23 = -9713982829728277004411482616930182093497888081399146977061925841588034
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_24 :
Polynomial.coeff recurrence4A4Square 24 = 147 * 10 ^ 70 + 7017000926830094692229373155863887566820430088532905173988562594999912
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_25 :
Polynomial.coeff recurrence4A4Square 25 = -(20309 * 10 ^ 70 + 7849183642375218788034362208002162491602850001694756625906705506434512)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_26 :
Polynomial.coeff recurrence4A4Square 26 = 2539088 * 10 ^ 70 + 9009997303745238112724744858113596553829144982383195424053784060107489
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_27 :
Polynomial.coeff recurrence4A4Square 27 = -(289886787 * 10 ^ 70 + 602300892307490562533511076040499452691536153497868992963703015372382)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_28 :
Polynomial.coeff recurrence4A4Square 28 = 30340296299 * 10 ^ 70 + 4882729650832885454318576382522755121504573411809160189324127898062454
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_29 :
Polynomial.coeff recurrence4A4Square 29 = -(2920965414513 * 10 ^ 70 + 8410934306655376159706497270634007568374222643820503127110839018674444)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_30 :
Polynomial.coeff recurrence4A4Square 30 = 259464097037638 * 10 ^ 70 + 4487772532528686041354574186957395327153248693310629773846771920989422
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_31 :
Polynomial.coeff recurrence4A4Square 31 = -(21324759644101472 * 10 ^ 70 + 8677778227570543161056149267121702578574968321968230955346716508986348)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_32 :
Polynomial.coeff recurrence4A4Square 32 = 1625777228509233192 * 10 ^ 70 + 6038549779397216238995111369557329488093692056900051697177340171286884
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_33 :
Polynomial.coeff recurrence4A4Square 33 = -(115249412387239811156 * 10 ^ 70 + 9037210462540109531265675683582498209457475573126305758442885079106356)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_34 :
Polynomial.coeff recurrence4A4Square 34 = 7613353584507259401596 * 10 ^ 70 + 815720072740956389793506350801768981721039042535617640806868594592354
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_35 :
Polynomial.coeff recurrence4A4Square 35 = -(469643906547481079272137 * 10 ^ 70 + 9418757231359737992635439107297405676116618199689502291051562830989778)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_36 :
Polynomial.coeff recurrence4A4Square 36 = 27105469302631421718053607 * 10 ^ 70 + 7162928852849461948666327618660079404111785567159711227213102542483661
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_37 :
Polynomial.coeff recurrence4A4Square 37 = -(1466328321360141764395649601 * 10 ^ 70 + 4459370821130360792026505169127695117925665445574561618580703058666954)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_38 :
Polynomial.coeff recurrence4A4Square 38 = 74479630122057456978616370466 * 10 ^ 70 + 3846858126340372002442941338620944194145195258521545102793006461111323
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_39 :
Polynomial.coeff recurrence4A4Square 39 = -(3557799527185097731456903473552 * 10 ^ 70 + 3611844819964928888993134613613994070661053461299874234945394175469444)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_40 :
Polynomial.coeff recurrence4A4Square 40 = 160078199682722428824306228042319 * 10 ^ 70 + 7737756941569643900751472203794618741519819836873930463413612070523774
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_41 :
Polynomial.coeff recurrence4A4Square 41 = -(6793996579071508496319421801096998 * 10 ^ 70 + 1551545952674333786083661803128278825848799350026617317535832668712984)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_42 :
Polynomial.coeff recurrence4A4Square 42 = 272374131273721250962843206531366645 * 10 ^ 70 + 3181329799922082674382183641837120241722781022586140702245882736859168
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_43 :
Polynomial.coeff recurrence4A4Square 43 = -(10328339949399742381899780985751487069 * 10 ^ 70 + 6552187892705033642499997641615064384879215729782279986650652461107894)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_44 :
Polynomial.coeff recurrence4A4Square 44 = 370911176667840646023232464891821982419 * 10 ^ 70 + 6002071065371414596091819190451196174561435932041597793921081493911447
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_45 :
Polynomial.coeff recurrence4A4Square 45 = -(12630204996011675801023260050384737844591 * 10 ^ 70 + 4846981639645300106124522716314981844015207227574541480016320020451430)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_46 :
Polynomial.coeff recurrence4A4Square 46 = 408277785254794470004959699552044491715921 * 10 ^ 70 + 1232069212363050207559963206747288316285436368959381069112578457425972
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_47 :
Polynomial.coeff recurrence4A4Square 47 = -(12542632629347184338850945998043163122049698 * 10 ^ 70 + 6825895969008644618165647691349337050635294754247911817819246678359978)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_48 :
Polynomial.coeff recurrence4A4Square 48 = 366582967070363032684901213150133775225179737 * 10 ^ 70 + 1384082717788593379289789561489459130613080131668606169020528983399561
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_49 :
Polynomial.coeff recurrence4A4Square 49 = -(10203543958520269722840532366009829883595844611 * 10 ^ 70 + 3949627617522550524434051446533800159798947493673815985304269343510560)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_50 :
Polynomial.coeff recurrence4A4Square 50 = 270739835162477625835079457627396391622318530169 * 10 ^ 70 + 7447679192116595282060049221565039873119732956427584082248665039660634
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_51 :
Polynomial.coeff recurrence4A4Square 51 = -(6854668792789353363395305116685895312322153449916 * 10 ^ 70 + 1213910996263740111291752677441133269267423313349793589848235978169440)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_52 :
Polynomial.coeff recurrence4A4Square 52 = 165748417232311440666361105755242829044255099679294 * 10 ^ 70 + 387959936514862049974045308037242155398536885812478431756447915089235
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_53 :
Polynomial.coeff recurrence4A4Square 53 = -(3831084493525834812356134488719970922878491271205216 * 10 ^ 70 + 7584656381691800048802569887671756512448518571769384189064647212682742)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_54 :
Polynomial.coeff recurrence4A4Square 54 = 84716991153909739769616233711226865709116498715325313 * 10 ^ 70 + 1023065714074220345718803240864515291977267267147575582734017519561683
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_55 :
Polynomial.coeff recurrence4A4Square 55 = -(1793699604822201842055250885099432653994234740726682017 * 10 ^ 70 + 5139460181796902905654617563994911282020923019490502544614254200666768)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_56 :
Polynomial.coeff recurrence4A4Square 56 = 36391572929052260425590291732395312128123606997799557035 * 10 ^ 70 + 3700408283222129665778396327040316532996273115174179895900589717055890
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_57 :
Polynomial.coeff recurrence4A4Square 57 = -(708033150896997253111034356288370945466612875849831324414 * 10 ^ 70 + 6800715305862908962304867287794536760547562253095607205397649696701974)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_58 :
Polynomial.coeff recurrence4A4Square 58 = 13219849198314152028171966646026919303420467811657699754834 * 10 ^ 70 + 7789949738338298857152030054816522542960326565012600105498627749162488
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_59 :
Polynomial.coeff recurrence4A4Square 59 = -(237043115080937333902329900530653874348089649965888194334927 * 10 ^ 70 + 7724800731831219392536295393746696227895044596667582158260778881375324)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_60 :
Polynomial.coeff recurrence4A4Square 60 = 4084639305529518431310446317258505967130873012223247152549601 * 10 ^ 70 + 2247184839184923819887123294754979329289858658782664139827026371656984
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_61 :
Polynomial.coeff recurrence4A4Square 61 = -(67685157165518814365387468355101383529038602436771377007415138 * 10 ^ 70 + 4306664081582345004633150374781230344720785652149427047963825335647138)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_62 :
Polynomial.coeff recurrence4A4Square 62 = 1079257470601903701166049031511599603767791742023164010946516745 * 10 ^ 70 + 1831309709753616778367182456537881709054680558039619373262179437096462
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_63 :
Polynomial.coeff recurrence4A4Square 63 = -(16569835596491028330801188210732357536976914292817159357955116623 * 10 ^ 70 + 1997688710234508517243725268071750761661735042091370942144487071571326)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_64 :
Polynomial.coeff recurrence4A4Square 64 = 245094713463240100157587165525978555659034467846150956310784611052 * 10 ^ 70 + 2565916812960176191817897787050932763055071809365892606475415848705663
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_65 :
Polynomial.coeff recurrence4A4Square 65 = -(3494823289923488114607545549469021063172124353023269416553158598233 * 10 ^ 70 + 3988009861982323367156686066610954407646959749909971273539936526557676)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_66 :
Polynomial.coeff recurrence4A4Square 66 = 48065904791604830108226159563794406806421576834032565584998256551283 * 10 ^ 70 + 5347218432521577878716214059762603131477626149990304798412105564518288
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_67 :
Polynomial.coeff recurrence4A4Square 67 = -(637980227623373249007430717357007768914547219291287917986037926550053 * 10 ^ 70 + 1961889156427101711829020557460243918240765147547597765941134570762534)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_68 :
Polynomial.coeff recurrence4A4Square 68 = 8176470397405672397196695480831887877738050544873382220373544589702747 * 10 ^ 70 + 8392821774945171780722738098709213982665340903855614248422374885903085
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_69 :
Polynomial.coeff recurrence4A4Square 69 = -((10 * 10 ^ 70 + 1236352808806093239817300900527607061422973765681655840163764008283830) * 10 ^ 70 + 5005118230504138906945922463309078182054937958457308248845237612360854)