Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar1LeftPart0.Coefficients0To40

Recurrence 4 lookup certificate: Scalar1Left 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.recurrence4Scalar1Left_coeff_0 :
Polynomial.coeff recurrence4Scalar1Left 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_1 :
Polynomial.coeff recurrence4Scalar1Left 1 = -99315933117299314134403723541286627756220416
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_2 :
Polynomial.coeff recurrence4Scalar1Left 2 = 733478399094153464288561736022755528725209251840
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_3 :
Polynomial.coeff recurrence4Scalar1Left 3 = -1498265309169662814642809029245769854881970893526528
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_4 :
Polynomial.coeff recurrence4Scalar1Left 4 = -753815074531733876920528261656772787411932682339518464
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_5 :
Polynomial.coeff recurrence4Scalar1Left 5 = 8515727816507089124145629256063472034584041436965337427808
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_6 :
Polynomial.coeff recurrence4Scalar1Left 6 = -16784324902503465892903450520340026793206451037199474341745328
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_7 :
Polynomial.coeff recurrence4Scalar1Left 7 = 17452452303134609742725667282368232718837598035417312767803431440
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_8 :
Polynomial.coeff recurrence4Scalar1Left 8 = -11092363346271294338983144153628813438350300602420714447124101089052
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_9 :
Polynomial.coeff recurrence4Scalar1Left 9 = 5007472240346861592806715407473327833885531584382254591860017598926248
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_10 :
Polynomial.coeff recurrence4Scalar1Left 10 = -(218 * 10 ^ 70 + 1950586782191303261305479848480916699471710730223417122123031698509208)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_11 :
Polynomial.coeff recurrence4Scalar1Left 11 = 92627 * 10 ^ 70 + 3046242656670227312552367090840187009906912575965939252470839523343300
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_12 :
Polynomial.coeff recurrence4Scalar1Left 12 = -(20946035 * 10 ^ 70 + 3205036313978438054484114138136796522942799807113920143169940847682748)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_13 :
Polynomial.coeff recurrence4Scalar1Left 13 = -(6465549589 * 10 ^ 70 + 4972365266738326457785023301598908396458894887131539891860586258567852)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_14 :
Polynomial.coeff recurrence4Scalar1Left 14 = 7969456870458 * 10 ^ 70 + 5432808864849330025725042880114869528564104716352435737631577229694948
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_15 :
Polynomial.coeff recurrence4Scalar1Left 15 = -(4069853363068965 * 10 ^ 70 + 498206078930994780633838862243877439284804958336784066203440812409056)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_16 :
Polynomial.coeff recurrence4Scalar1Left 16 = 1675027463587444949 * 10 ^ 70 + 9291062629028271432071332178670070640153244427576712151067063036137260
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_17 :
Polynomial.coeff recurrence4Scalar1Left 17 = -(629172661599693645957 * 10 ^ 70 + 9565317195665560982696212105898832086226612984352690409406545748497464)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_18 :
Polynomial.coeff recurrence4Scalar1Left 18 = 177467237012452387685301 * 10 ^ 70 + 9808960915946791564902535217270854490046057474514052239408703123819557
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_19 :
Polynomial.coeff recurrence4Scalar1Left 19 = -(14705129426543327020089251 * 10 ^ 70 + 7539033886093657919814384732516975022779496247462294740250062290125766)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_20 :
Polynomial.coeff recurrence4Scalar1Left 20 = -(16709842783333280897830127284 * 10 ^ 70 + 9840731317765515853802927055833734466175720397617859053191005942165000)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_21 :
Polynomial.coeff recurrence4Scalar1Left 21 = 10992260451616636513145676131225 * 10 ^ 70 + 6877199433317576896733918155383310855448127797387712726547744103878759
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_22 :
Polynomial.coeff recurrence4Scalar1Left 22 = -(3955411624033755179348072452215922 * 10 ^ 70 + 2127966492195027564280330625058516528220818151267301715538059298106368)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_23 :
Polynomial.coeff recurrence4Scalar1Left 23 = 985830500568056944420134865475079135 * 10 ^ 70 + 2484002289182763773394479827598310344072758897183841471635407084663408
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_24 :
Polynomial.coeff recurrence4Scalar1Left 24 = -(173194276210504783118178109210883219967 * 10 ^ 70 + 5971025799695322573401981438206996473678713565593302332067933611009326)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_25 :
Polynomial.coeff recurrence4Scalar1Left 25 = 17167362548421172705139828814289278610927 * 10 ^ 70 + 1469845955212189787664833072658393179577582413234752574554992772966886
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_26 :
Polynomial.coeff recurrence4Scalar1Left 26 = 1666521741794707344392985996496435930890514 * 10 ^ 70 + 3492907017598397559301086280750328542452638865409192556080368549037006
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_27 :
Polynomial.coeff recurrence4Scalar1Left 27 = -(1493838530461415026912767500722914411136644117 * 10 ^ 70 + 1222069756626056249339378349452634368093989826952550371122536817334212)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_28 :
Polynomial.coeff recurrence4Scalar1Left 28 = 540742949586439889367849200559674015178865630926 * 10 ^ 70 + 3330815758271553538868721218720122177029257181460505302741129031715050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_29 :
Polynomial.coeff recurrence4Scalar1Left 29 = -(154714906603283044196475614625334388989303423061677 * 10 ^ 70 + 2919835359488490127393336822996908203946388061306578767778256839986404)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_30 :
Polynomial.coeff recurrence4Scalar1Left 30 = 38279842410806734520404944715281743126624833214280536 * 10 ^ 70 + 3641733455765872660128854431118078295564350514790482455809517297404234
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_31 :
Polynomial.coeff recurrence4Scalar1Left 31 = -(8313500566436207906980073230737730148820438205970285128 * 10 ^ 70 + 7103739708128782398803416060536674517644459055965568496405943041127982)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_32 :
Polynomial.coeff recurrence4Scalar1Left 32 = 1583281894841204524512588254683629929442909339445844114376 * 10 ^ 70 + 3957593169130929874466564563484990795521287493518435926324614698997352
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_33 :
Polynomial.coeff recurrence4Scalar1Left 33 = -(263165464511140530947177917167356333231897235381288664689580 * 10 ^ 70 + 5099462856969823874535845717672956971459983423680393004038682929834377)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_34 :
Polynomial.coeff recurrence4Scalar1Left 34 = 37830812628647212455436772592675696145850601734906414147522102 * 10 ^ 70 + 1813436261986104203036108425382420487577375009202865670707421830335136
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_35 :
Polynomial.coeff recurrence4Scalar1Left 35 = -(4610273168351078482982374856854549770872881554269593852180628407 * 10 ^ 70 + 6942353006240364226086415778824153200709240831298862861909863875870908)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_36 :
Polynomial.coeff recurrence4Scalar1Left 36 = 452983993227737748731170738442723748081132658592020189736231179882 * 10 ^ 70 + 588724266403483041382874424061558094057790461782534598165047179807993
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_37 :
Polynomial.coeff recurrence4Scalar1Left 37 = -(30307912086844440078394090078971534368149492903178979281698358285923 * 10 ^ 70 + 9593478463845892780573147013006270899750399091971859818927173903946004)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_38 :
Polynomial.coeff recurrence4Scalar1Left 38 = -(21800842576280918363133335347365236331568191856252751784453210520362 * 10 ^ 70 + 6884657859565740672560316142691098407264989294604361100450762054727461)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_39 :
Polynomial.coeff recurrence4Scalar1Left 39 = (41 * 10 ^ 70 + 7189623283299405956587290229637541136991224504239021697389851155052880) * 10 ^ 70 + 8216985231481152095416515535402943502166084902646896584413846114338391
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_40 :
Polynomial.coeff recurrence4Scalar1Left 40 = -((8407 * 10 ^ 70 + 7014442074565049838349904743160421503967820551317042942288937986118340) * 10 ^ 70 + 4197816159802119225892267286704384893273592313828850238187933700509043)