Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupB0Low

Recurrence 2 lookup certificate: B0 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.recurrence2B0_coeff_0 :
Polynomial.coeff remainder3Coefficient0 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_1 :
Polynomial.coeff remainder3Coefficient0 1 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_2 :
Polynomial.coeff remainder3Coefficient0 2 = -8
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_3 :
Polynomial.coeff remainder3Coefficient0 3 = 179024
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_4 :
Polynomial.coeff remainder3Coefficient0 4 = 30754666
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_5 :
Polynomial.coeff remainder3Coefficient0 5 = 477021417487
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_6 :
Polynomial.coeff remainder3Coefficient0 6 = -232679923019180
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_7 :
Polynomial.coeff remainder3Coefficient0 7 = 101440949732911807
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_8 :
Polynomial.coeff remainder3Coefficient0 8 = -24730814056414366604
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_9 :
Polynomial.coeff remainder3Coefficient0 9 = 4024008953500262585477
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_10 :
Polynomial.coeff remainder3Coefficient0 10 = -453727011615361254128640
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_11 :
Polynomial.coeff remainder3Coefficient0 11 = 35773836854796317297182412
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_12 :
Polynomial.coeff remainder3Coefficient0 12 = -2034870664052154352728358965
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_13 :
Polynomial.coeff remainder3Coefficient0 13 = 83905281819788621191507714267
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_14 :
Polynomial.coeff remainder3Coefficient0 14 = -2629889589502770617695121931036
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_15 :
Polynomial.coeff remainder3Coefficient0 15 = 68870813236477147681526337937965
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_16 :
Polynomial.coeff remainder3Coefficient0 16 = -1742335801519438920177093336423298
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_17 :
Polynomial.coeff remainder3Coefficient0 17 = 38064345949383782936507754711195193
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_18 :
Polynomial.coeff remainder3Coefficient0 18 = -179204151669257402026118359209574838
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_19 :
Polynomial.coeff remainder3Coefficient0 19 = -36973979374681706412342359208334347420
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_20 :
Polynomial.coeff remainder3Coefficient0 20 = 2137363388566628284743357197726381838956
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_21 :
Polynomial.coeff remainder3Coefficient0 21 = -71911779643193959004534831480162841168816
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_22 :
Polynomial.coeff remainder3Coefficient0 22 = 1762597275403315276703628289405966746342987
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_23 :
Polynomial.coeff remainder3Coefficient0 23 = -34138692680849682446976950412851940339449937
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_24 :
Polynomial.coeff remainder3Coefficient0 24 = 552467363692672535803570517425603952564410700
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_25 :
Polynomial.coeff remainder3Coefficient0 25 = -7939075987439788713884785869012474294399561470
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_26 :
Polynomial.coeff remainder3Coefficient0 26 = 109349853254286577338279748981779958688710271384
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_27 :
Polynomial.coeff remainder3Coefficient0 27 = -1545880979781235721694231385301134279432156136508
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_28 :
Polynomial.coeff remainder3Coefficient0 28 = 22676504550839967189427936447813371811662024521348
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_29 :
Polynomial.coeff remainder3Coefficient0 29 = -328974304001526798795544959789385551647442053342118
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_30 :
Polynomial.coeff remainder3Coefficient0 30 = 4465286366450333486645924557987928865749063110891113
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_31 :
Polynomial.coeff remainder3Coefficient0 31 = -54858799736235509791029301212568734913907021329458784
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_32 :
Polynomial.coeff remainder3Coefficient0 32 = 602145153406959310447880262540369323094402427015474536
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_33 :
Polynomial.coeff remainder3Coefficient0 33 = -5892564198806635769120058488175133730683428849273203299
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_34 :
Polynomial.coeff remainder3Coefficient0 34 = 51545635611367479734117846407920081397724562865823431419
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_35 :
Polynomial.coeff remainder3Coefficient0 35 = -404733608756654388005937985259073789253768588125584448198
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_36 :
Polynomial.coeff remainder3Coefficient0 36 = 2864527516590043161232655711795302583444761115820971275073
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_37 :
Polynomial.coeff remainder3Coefficient0 37 = -18338507132563601942380943235856576917881771753697255182725
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_38 :
Polynomial.coeff remainder3Coefficient0 38 = 106463557541167214228442303735616701032671133924883061691086
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_39 :
Polynomial.coeff remainder3Coefficient0 39 = -561314278962909219698295422547172122011777036251181215870161
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_40 :
Polynomial.coeff remainder3Coefficient0 40 = 2688714399335101325596980661656839893849979702706195758065970
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_41 :
Polynomial.coeff remainder3Coefficient0 41 = -11689549642467735400408356871109602940443575954274571913303935
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_42 :
Polynomial.coeff remainder3Coefficient0 42 = 45985306071259975175409394912470024994236286701497963142226289
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_43 :
Polynomial.coeff remainder3Coefficient0 43 = -162524193462981449826461384091871109782767383312237911541949276
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_44 :
Polynomial.coeff remainder3Coefficient0 44 = 508227155293203124988320624447267957476766364183277258945266574
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_45 :
Polynomial.coeff remainder3Coefficient0 45 = -1359566889412032846429096507235445040180812639893288373562239901
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_46 :
Polynomial.coeff remainder3Coefficient0 46 = 2851082208712297703151714776027122850324020555819312143829871493
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_47 :
Polynomial.coeff remainder3Coefficient0 47 = -3190153207632062724964284287111805372054977741114378625081653140
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_48 :
Polynomial.coeff remainder3Coefficient0 48 = -8222234960983443522939973587058089086984514578165173608118869832
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_49 :
Polynomial.coeff remainder3Coefficient0 49 = 71950429460641988698423177959227678104989764102893748462736114766
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_50 :
Polynomial.coeff remainder3Coefficient0 50 = -318655852741105373388953630861154707199405529356719958730512207827
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_51 :
Polynomial.coeff remainder3Coefficient0 51 = 1138173346144201769318489239229936809648313545540220639990693475460
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_52 :
Polynomial.coeff remainder3Coefficient0 52 = -3582063774549879460130271415765521782441072173836308200276279318640
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_53 :
Polynomial.coeff remainder3Coefficient0 53 = 9726947810203285340886442629401443956236951259119670967933377171956
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_54 :
Polynomial.coeff remainder3Coefficient0 54 = -20245176225376080422475912791710571138087986505378621699306103086440
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_55 :
Polynomial.coeff remainder3Coefficient0 55 = 22607993508856402456617761214149894753738162723981498978965300550861
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_56 :
Polynomial.coeff remainder3Coefficient0 56 = 13846440143222403243857340271597973942352036638054698356320170152420
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_57 :
Polynomial.coeff remainder3Coefficient0 57 = 28554743406922175307074588179655867012406316324581886630530548415658
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_58 :
Polynomial.coeff remainder3Coefficient0 58 = -1182651282063552015081910611553092382095478983530767711217513298572824
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_59 :
Polynomial.coeff remainder3Coefficient0 59 = 6187143208974982925970866126985089225146046238944149450001511003299263
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_60 :
Polynomial.coeff remainder3Coefficient0 60 = -(1 * 10 ^ 70 + 2085970620285470392865219150601545691257864750607172538217681000660039)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_61 :
Polynomial.coeff remainder3Coefficient0 61 = -(3 * 10 ^ 70 + 1901383709098183409915792383015946630065796182777010317406901156610827)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_62 :
Polynomial.coeff remainder3Coefficient0 62 = 30 * 10 ^ 70 + 9561833262843952809262611815720791267176350825051048545067831418476941
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_63 :
Polynomial.coeff remainder3Coefficient0 63 = -(98 * 10 ^ 70 + 7677926928852386393594783917498824380279216660370137348055931732846692)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_64 :
Polynomial.coeff remainder3Coefficient0 64 = 58 * 10 ^ 70 + 8024880259329850641699607917506419856806472613989222099654546179168908
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_65 :
Polynomial.coeff remainder3Coefficient0 65 = 926 * 10 ^ 70 + 4145145529487333065545272393485536463105174908381470661656996415373733
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_66 :
Polynomial.coeff remainder3Coefficient0 66 = -(4885 * 10 ^ 70 + 4848455228927648187599058205666114899346301381293944978894488897400107)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_67 :
Polynomial.coeff remainder3Coefficient0 67 = 11836 * 10 ^ 70 + 3483970638617886026488422400632582889101072970288920770240460647017406
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_68 :
Polynomial.coeff remainder3Coefficient0 68 = -(1337 * 10 ^ 70 + 921428541403960987264206305331329502666685355146998744423451261826349)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_69 :
Polynomial.coeff remainder3Coefficient0 69 = -(116089 * 10 ^ 70 + 6702235321806926155180301241708749461687596901244528567903768516672786)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_70 :
Polynomial.coeff remainder3Coefficient0 70 = 541681 * 10 ^ 70 + 9534297521735342029738650870668182171078734748142411195867178458126851
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_71 :
Polynomial.coeff remainder3Coefficient0 71 = -(1359845 * 10 ^ 70 + 7153377359221241680560545494370786197657396585222808925930939766106640)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_72 :
Polynomial.coeff remainder3Coefficient0 72 = 1229382 * 10 ^ 70 + 1311286611871202468054543104929690652817501167700804438443144352646901
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_73 :
Polynomial.coeff remainder3Coefficient0 73 = 6389090 * 10 ^ 70 + 5636886912336226670298245357517314331241637596228909850780665834212548
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_74 :
Polynomial.coeff remainder3Coefficient0 74 = -(39604226 * 10 ^ 70 + 2259627221364964157794682836090253498123192830176801346768031823893364)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_75 :
Polynomial.coeff remainder3Coefficient0 75 = 128843926 * 10 ^ 70 + 6026287706649311815457268670346299060155594090441456218050598517348007
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_76 :
Polynomial.coeff remainder3Coefficient0 76 = -(278453357 * 10 ^ 70 + 1779230066412021845150390271391126105507858835292019039476615358329608)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B0_coeff_77 :
Polynomial.coeff remainder3Coefficient0 77 = 302102269 * 10 ^ 70 + 9295861798022802581679693657514244784648543256589748207996165763242506