Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupB2Low

Recurrence 2 lookup certificate: B2 source coefficients, low half #

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.recurrence2B2_coeff_0 :
Polynomial.coeff remainder3Coefficient2 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_1 :
Polynomial.coeff remainder3Coefficient2 1 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_2 :
Polynomial.coeff remainder3Coefficient2 2 = 20566
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_3 :
Polynomial.coeff remainder3Coefficient2 3 = 467452502
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_4 :
Polynomial.coeff remainder3Coefficient2 4 = -248803518198
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_5 :
Polynomial.coeff remainder3Coefficient2 5 = 383227126470131
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_6 :
Polynomial.coeff remainder3Coefficient2 6 = -152822662923162884
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_7 :
Polynomial.coeff remainder3Coefficient2 7 = 42180852282813951032
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_8 :
Polynomial.coeff remainder3Coefficient2 8 = -7051644585908704055280
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_9 :
Polynomial.coeff remainder3Coefficient2 9 = 789505055030491628391075
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_10 :
Polynomial.coeff remainder3Coefficient2 10 = -59986525779113592452228114
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_11 :
Polynomial.coeff remainder3Coefficient2 11 = 3140523831275756399695569367
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_12 :
Polynomial.coeff remainder3Coefficient2 12 = -114649868328970443430888145935
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_13 :
Polynomial.coeff remainder3Coefficient2 13 = 3145208853554043704377412826823
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_14 :
Polynomial.coeff remainder3Coefficient2 14 = -95254075572483322850249961335294
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_15 :
Polynomial.coeff remainder3Coefficient2 15 = 4707286715224831131980976760272090
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_16 :
Polynomial.coeff remainder3Coefficient2 16 = -252119760709282965148060859490098674
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_17 :
Polynomial.coeff remainder3Coefficient2 17 = 10920773607153928613786783012238872921
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_18 :
Polynomial.coeff remainder3Coefficient2 18 = -374755433938771058464397696038142186056
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_19 :
Polynomial.coeff remainder3Coefficient2 19 = 10423139299556869835388904607584062679111
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_20 :
Polynomial.coeff remainder3Coefficient2 20 = -236508744925100315692077438653052297791806
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_21 :
Polynomial.coeff remainder3Coefficient2 21 = 4264782476520433050173386942964682535047038
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_22 :
Polynomial.coeff remainder3Coefficient2 22 = -55256619995110073203406178869402808396548740
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_23 :
Polynomial.coeff remainder3Coefficient2 23 = 285706806254928866062310198554674176338128828
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_24 :
Polynomial.coeff remainder3Coefficient2 24 = 9151218683896100753611859546553688315536346346
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_25 :
Polynomial.coeff remainder3Coefficient2 25 = -360723793542344848926346348860010605221468898151
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_26 :
Polynomial.coeff remainder3Coefficient2 26 = 7988566775046323816950452536667043821428643273571
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_27 :
Polynomial.coeff remainder3Coefficient2 27 = -135610457529676213927524080412967938276908000989499
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_28 :
Polynomial.coeff remainder3Coefficient2 28 = 1912098641510585058099084468722416136697822198628623
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_29 :
Polynomial.coeff remainder3Coefficient2 29 = -23183387137118427190312349102213378182877449677860270
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_30 :
Polynomial.coeff remainder3Coefficient2 30 = 246329617178149273935393622793688400091367824947689466
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_31 :
Polynomial.coeff remainder3Coefficient2 31 = -2321078854207125281928321165528633903884832772129450505
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_32 :
Polynomial.coeff remainder3Coefficient2 32 = 19554454400437866274729702375867507229487690725880338625
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_33 :
Polynomial.coeff remainder3Coefficient2 33 = -148173271675304899089185520264698955187655856836240781529
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_34 :
Polynomial.coeff remainder3Coefficient2 34 = 1014337899014932756179294601359552920296855999551578100641
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_35 :
Polynomial.coeff remainder3Coefficient2 35 = -6293016267641226930816983777632313952601640526445380151277
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_36 :
Polynomial.coeff remainder3Coefficient2 36 = 35453047198090537082304117523098262290953781713141305831790
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_37 :
Polynomial.coeff remainder3Coefficient2 37 = -181499756823876778304060593417382305756426614026496891389935
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_38 :
Polynomial.coeff remainder3Coefficient2 38 = 843755290301089933115552025148303090521645311900760275574478
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_39 :
Polynomial.coeff remainder3Coefficient2 39 = -3552824034029471684453840394271692866755848034950107359651480
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_40 :
Polynomial.coeff remainder3Coefficient2 40 = 13478123055651230228272777873715663363791103402982773920944516
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_41 :
Polynomial.coeff remainder3Coefficient2 41 = -45582171189210250545017707180304950371503361684194561569665487
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_42 :
Polynomial.coeff remainder3Coefficient2 42 = 134429195558020180454399136591174639861549207080127987930005697
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_43 :
Polynomial.coeff remainder3Coefficient2 43 = -328003938045700375173751495721136104332755576834768852631221653
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_44 :
Polynomial.coeff remainder3Coefficient2 44 = 557924028055441474238630776968822342538856427701636338978197629
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_45 :
Polynomial.coeff remainder3Coefficient2 45 = 4443215559487839326439914202816308765887547512828767566577894
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_46 :
Polynomial.coeff remainder3Coefficient2 46 = -5190470250224262508551271917117761513256090003934359515937713572
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_47 :
Polynomial.coeff remainder3Coefficient2 47 = 28122045346581622831222804024479730765729259546789372377157070970
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_48 :
Polynomial.coeff remainder3Coefficient2 48 = -106788653096648679148087335350647801913263895572835705266931236346
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_49 :
Polynomial.coeff remainder3Coefficient2 49 = 342145434390218184106531767714388496739031953827924299460661589676
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_50 :
Polynomial.coeff remainder3Coefficient2 50 = -987235433873104535656362726172641254794587115864251552945804076105
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_51 :
Polynomial.coeff remainder3Coefficient2 51 = 2561901456258136949894791767672983359060878522867259312939165863923
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_52 :
Polynomial.coeff remainder3Coefficient2 52 = -5457811960018399890535577784772290315877026020624914203761494109784
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_53 :
Polynomial.coeff remainder3Coefficient2 53 = 7209866222568054868512328548494855815959045172876543998169252113244
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_54 :
Polynomial.coeff remainder3Coefficient2 54 = 1724737831226548170000465792846091900982352387032329614998427719216
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_55 :
Polynomial.coeff remainder3Coefficient2 55 = -13372367869848666839347703572120985123394727185653966147681404955432
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_56 :
Polynomial.coeff remainder3Coefficient2 56 = -157339896768072354933942554862976313707979773239351019084456150604421
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_57 :
Polynomial.coeff remainder3Coefficient2 57 = 1159564890418055661323514297762148901433296114321838721244994297797577
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_58 :
Polynomial.coeff remainder3Coefficient2 58 = -3054243963534027327407222692196537649633065226852682894389216541526680
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_59 :
Polynomial.coeff remainder3Coefficient2 59 = -2858937352163103397112804505247217042729858885502902041365725400988923
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_60 :
Polynomial.coeff remainder3Coefficient2 60 = 5 * 10 ^ 70 + 4534678257021364220065665885601967779032608595213555231118776038064568
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_61 :
Polynomial.coeff remainder3Coefficient2 61 = -(20 * 10 ^ 70 + 5316457637001890020694013735680233966638042633322734632182196570211985)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_62 :
Polynomial.coeff remainder3Coefficient2 62 = 23 * 10 ^ 70 + 619480194053390530218647033603763596156082753043918233161797927318675
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_63 :
Polynomial.coeff remainder3Coefficient2 63 = 143 * 10 ^ 70 + 3322050784409541498630282889013093835565987124507123047930319437077533
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_64 :
Polynomial.coeff remainder3Coefficient2 64 = -(900 * 10 ^ 70 + 5447893521413281801840670945787098264834803571205293176637274299607663)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_65 :
Polynomial.coeff remainder3Coefficient2 65 = 2418 * 10 ^ 70 + 7446152476167709049666999809968464537768999676262503271693769681195773
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_66 :
Polynomial.coeff remainder3Coefficient2 66 = -(1219 * 10 ^ 70 + 1726704762365575889116972647849103155504577598226140509866060555820458)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_67 :
Polynomial.coeff remainder3Coefficient2 67 = -(19178 * 10 ^ 70 + 2875446448841531236806362122177755799580882564598469929967208992738766)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_68 :
Polynomial.coeff remainder3Coefficient2 68 = 97482 * 10 ^ 70 + 7413972977330840741571666419461094606328959665463097412149691014151041
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_69 :
Polynomial.coeff remainder3Coefficient2 69 = -(255535 * 10 ^ 70 + 2528096015106219807884752781334469308302588552952229209584596469340131)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_70 :
Polynomial.coeff remainder3Coefficient2 70 = 264267 * 10 ^ 70 + 9044419317102424322353002264157586752254742401646693919167246904528533
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_71 :
Polynomial.coeff remainder3Coefficient2 71 = 1029960 * 10 ^ 70 + 7772281310642717885390182951937129250880590873228342112801682245293
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_72 :
Polynomial.coeff remainder3Coefficient2 72 = -(6821433 * 10 ^ 70 + 578893228553685928493216088652583932457539998082710688173398952810092)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_73 :
Polynomial.coeff remainder3Coefficient2 73 = 22409306 * 10 ^ 70 + 9522919787142159639007142043033037572457611885946470063852114368708480