Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar1ShiftPart0.Coefficients0To91

Recurrence 2 lookup certificate: Scalar1Shift coefficient convolution #

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.recurrence2Scalar1Shift_coeff_0 :
Polynomial.coeff recurrence2Scalar1Shift 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_1 :
Polynomial.coeff recurrence2Scalar1Shift 1 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_2 :
Polynomial.coeff recurrence2Scalar1Shift 2 = 310272
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_3 :
Polynomial.coeff recurrence2Scalar1Shift 3 = -6866834496
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_4 :
Polynomial.coeff recurrence2Scalar1Shift 4 = 3301698573280
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_5 :
Polynomial.coeff recurrence2Scalar1Shift 5 = -157209563968245296
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_6 :
Polynomial.coeff recurrence2Scalar1Shift 6 = -34566550554750265888
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_7 :
Polynomial.coeff recurrence2Scalar1Shift 7 = -249403642765872182157796
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_8 :
Polynomial.coeff recurrence2Scalar1Shift 8 = 89513508338739205290862424
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_9 :
Polynomial.coeff recurrence2Scalar1Shift 9 = 316325674088117056455931867200
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_10 :
Polynomial.coeff recurrence2Scalar1Shift 10 = -372490779550000886685339682747424
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_11 :
Polynomial.coeff recurrence2Scalar1Shift 11 = 372795893081886650774080689901566990
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_12 :
Polynomial.coeff recurrence2Scalar1Shift 12 = -222377956789602437579628603374495212282
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_13 :
Polynomial.coeff recurrence2Scalar1Shift 13 = 99072812274473847370415218597039746529486
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_14 :
Polynomial.coeff recurrence2Scalar1Shift 14 = -33198643442823568803678315832753725913884842
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_15 :
Polynomial.coeff recurrence2Scalar1Shift 15 = 8540677074655333025373585360047698552893321976
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_16 :
Polynomial.coeff recurrence2Scalar1Shift 16 = -1710244370752074889351392740020446233616941350651
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_17 :
Polynomial.coeff recurrence2Scalar1Shift 17 = 266475970836653330278873331416923010225479565615929
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_18 :
Polynomial.coeff recurrence2Scalar1Shift 18 = -31897755067622523273779025332598011049108736249168391
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_19 :
Polynomial.coeff recurrence2Scalar1Shift 19 = 2800177202746573673417872620170003096390316349650946475
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_20 :
Polynomial.coeff recurrence2Scalar1Shift 20 = -152341070862629074652108250356021926048215302748603238234
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_21 :
Polynomial.coeff recurrence2Scalar1Shift 21 = -189295366011196310703322064060571596507865186739543371019
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_22 :
Polynomial.coeff recurrence2Scalar1Shift 22 = 1088100020612692787628393358779132340220145897181105822060314
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_23 :
Polynomial.coeff recurrence2Scalar1Shift 23 = -137452864656509020609995123083424574956280481926876498927786434
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_24 :
Polynomial.coeff recurrence2Scalar1Shift 24 = 10910501380298811619547857112509382305333785793948384239497132443
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_25 :
Polynomial.coeff recurrence2Scalar1Shift 25 = -641522909976205280116565258503107046061775566874221906111459382189
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_26 :
Polynomial.coeff recurrence2Scalar1Shift 26 = 29295893435972361988600906025709009428130261093895160524565063184551
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_27 :
Polynomial.coeff recurrence2Scalar1Shift 27 = -1041573125066530888870503038547401171107579240330131698895596635717477
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_28 :
Polynomial.coeff recurrence2Scalar1Shift 28 = 2 * 10 ^ 70 + 6261461370089742043635113773989539527411889514403019027918930382386887
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_29 :
Polynomial.coeff recurrence2Scalar1Shift 29 = -(15 * 10 ^ 70 + 1287054266642265859348991329016441618509637402882256524586201100554610)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_30 :
Polynomial.coeff recurrence2Scalar1Shift 30 = -(3516 * 10 ^ 70 + 4440875009044024215913698170125293867901983766510207191896457897482197)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_31 :
Polynomial.coeff recurrence2Scalar1Shift 31 = 288390 * 10 ^ 70 + 8880027394503544831645826681843079584897983058530796230034166915221128
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_32 :
Polynomial.coeff recurrence2Scalar1Shift 32 = -(14769219 * 10 ^ 70 + 3561945119309785318835171320727241615311189126782062987280282195958143)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_33 :
Polynomial.coeff recurrence2Scalar1Shift 33 = 570280754 * 10 ^ 70 + 2895547748191864917367320239815505911029582714161000289179597400269294
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_34 :
Polynomial.coeff recurrence2Scalar1Shift 34 = -(17557712891 * 10 ^ 70 + 2369612584485065888352434869254849795328003331712360790430078852089391)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_35 :
Polynomial.coeff recurrence2Scalar1Shift 35 = 452342013583 * 10 ^ 70 + 5733308910892091662080742162611341349659145502917429997442374360670395
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_36 :
Polynomial.coeff recurrence2Scalar1Shift 36 = -(10179235767776 * 10 ^ 70 + 5391936638865779556377009200855764563555130948941493692598739915577051)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_37 :
Polynomial.coeff recurrence2Scalar1Shift 37 = 183552008339327 * 10 ^ 70 + 3321316601135416532763268374626392220219616865934823500389349613808069
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_38 :
Polynomial.coeff recurrence2Scalar1Shift 38 = -(713440619932174 * 10 ^ 70 + 6268391268645163137678554374960931064512005679238930410978223194810538)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_39 :
Polynomial.coeff recurrence2Scalar1Shift 39 = -(140188660480466882 * 10 ^ 70 + 8198495878332298428091514052519511506114338982364369974825332194236112)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_40 :
Polynomial.coeff recurrence2Scalar1Shift 40 = 7306839524128138168 * 10 ^ 70 + 3037094584868156125203113939858931704764563247057941326589966659819363
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_41 :
Polynomial.coeff recurrence2Scalar1Shift 41 = -(199221138055599059482 * 10 ^ 70 + 7728630948956195278623636556164724747521849069444177385734570479153437)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_42 :
Polynomial.coeff recurrence2Scalar1Shift 42 = 2677086746877060489470 * 10 ^ 70 + 3026650683325077984735989127845025554272834482972376592340660517059271
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_43 :
Polynomial.coeff recurrence2Scalar1Shift 43 = 13192405069247114415627 * 10 ^ 70 + 1648517202744194544594004479764640018611760299491922499534737263155468
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_44 :
Polynomial.coeff recurrence2Scalar1Shift 44 = -(835223600526687886668425 * 10 ^ 70 + 6822687802852614930121246273588543037203284071133188320166623593506131)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_45 :
Polynomial.coeff recurrence2Scalar1Shift 45 = -(34200012386365938633505959 * 10 ^ 70 + 6457251568159248705688947860740498644469880234946669986993232163918306)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_46 :
Polynomial.coeff recurrence2Scalar1Shift 46 = 3487865850356737376224311507 * 10 ^ 70 + 3690758043909801650095672804948389266301460395401778549289123068197318
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_47 :
Polynomial.coeff recurrence2Scalar1Shift 47 = -(153659779165619195206424596542 * 10 ^ 70 + 6899598411917749053791055239225363169872415710855504996740770938978496)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_48 :
Polynomial.coeff recurrence2Scalar1Shift 48 = 4848206478995394982977548089404 * 10 ^ 70 + 3449361556525779753821851434716882305192009700052207700504056194369286
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_49 :
Polynomial.coeff recurrence2Scalar1Shift 49 = -(124915378857288797755717459933772 * 10 ^ 70 + 6145990706121762393921508076072630782667253338953394318584114266906575)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_50 :
Polynomial.coeff recurrence2Scalar1Shift 50 = 2805631168687125232365121677499277 * 10 ^ 70 + 6434758887385890302338705033731794676104083585937605454581187369473133
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_51 :
Polynomial.coeff recurrence2Scalar1Shift 51 = -(57156429309304650295068094085245047 * 10 ^ 70 + 3532373628157559210224386330251159957048561917965734984371658402019377)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_52 :
Polynomial.coeff recurrence2Scalar1Shift 52 = 1079188566744736918577494474254051127 * 10 ^ 70 + 3619215521474620637285441381494246027250774188039699663635557507322354
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_53 :
Polynomial.coeff recurrence2Scalar1Shift 53 = -(18990079485225826434322841613952727548 * 10 ^ 70 + 6270918870252177856306772192540389706033894342726442649061759960425548)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_54 :
Polynomial.coeff recurrence2Scalar1Shift 54 = 309371884823064943751440417842198606756 * 10 ^ 70 + 2755491489631419157448613059413587878956658401845132436107511034847794
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_55 :
Polynomial.coeff recurrence2Scalar1Shift 55 = -(4602327557933323746287277946055904408226 * 10 ^ 70 + 816670028153416408218242610329845208274780963621994769061317986584041)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_56 :
Polynomial.coeff recurrence2Scalar1Shift 56 = 61318116980479740961055042524447734701806 * 10 ^ 70 + 6011812801788875210430964775210577054329341058991694287904034432764405
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_57 :
Polynomial.coeff recurrence2Scalar1Shift 57 = -(707877594219969798667355657598150304434817 * 10 ^ 70 + 8679915615843288267764092378577811654440248531885520550950158725296430)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_58 :
Polynomial.coeff recurrence2Scalar1Shift 58 = 6495991853711933893039540561304751079042835 * 10 ^ 70 + 8782422695153023815920226217462531273968598740604944172529023756009038
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_59 :
Polynomial.coeff recurrence2Scalar1Shift 59 = -(30376236357116347703393674023759593653040195 * 10 ^ 70 + 9077028013270051298877696543826897221093644473261781361120383914034705)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_60 :
Polynomial.coeff recurrence2Scalar1Shift 60 = -(523160304047700903141563236460864604811177103 * 10 ^ 70 + 7820371325069923599757495817755669523599872338571749496671213785169425)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_61 :
Polynomial.coeff recurrence2Scalar1Shift 61 = 21201267895698468152471958909260270472966212445 * 10 ^ 70 + 8659253776492061737073564725562329411581866787302770412147883745917308
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_62 :
Polynomial.coeff recurrence2Scalar1Shift 62 = -(490999208553871705280071135488820063119923352284 * 10 ^ 70 + 7569133155027765721521190272474755147765061869338192423987735000813603)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_63 :
Polynomial.coeff recurrence2Scalar1Shift 63 = 9458139530926474129365397973780746754247129735638 * 10 ^ 70 + 8557956510765371469076122914583427617611691323130853472125069942344114
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_64 :
Polynomial.coeff recurrence2Scalar1Shift 64 = -(164213972132964289993249183450770054941261534740500 * 10 ^ 70 + 3661776946926935292020440390447166652785112139768339105260831291018676)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_65 :
Polynomial.coeff recurrence2Scalar1Shift 65 = 2642814419557762756884623856162312561639794218237905 * 10 ^ 70 + 4116574624389366037444714988091312650786402991121598370303546272853580
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_66 :
Polynomial.coeff recurrence2Scalar1Shift 66 = -(39905269450141166163421522087843003726836431005362728 * 10 ^ 70 + 3695364205920454998286722979376675825636617113674491307796897462230084)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_67 :
Polynomial.coeff recurrence2Scalar1Shift 67 = 568835666743448699532174744424211010955463291139786377 * 10 ^ 70 + 7628142440464721832462072196362698177512111061890426579268282124058532
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_68 :
Polynomial.coeff recurrence2Scalar1Shift 68 = -(7682314737165241710988684850950495368197309015458386288 * 10 ^ 70 + 4650561220690328476814718682706895486721264444364199347033987639863961)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_69 :
Polynomial.coeff recurrence2Scalar1Shift 69 = 98513563814887818235877280781885739299025388504505517063 * 10 ^ 70 + 1978149499379589725158273376249061374441825333148318264270956734861338
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_70 :
Polynomial.coeff recurrence2Scalar1Shift 70 = -(1201128939228146987605110369842390756856409098838420195641 * 10 ^ 70 + 1982781463159673907578266453225603986459548864757820702567039791883760)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_71 :
Polynomial.coeff recurrence2Scalar1Shift 71 = 13937141619163117337225821840652100031839282686700825912169 * 10 ^ 70 + 5021828651037300688476982435571359061619953324208567921371275445514735
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_72 :
Polynomial.coeff recurrence2Scalar1Shift 72 = -(154024007754331658633161706356742072797665376906763152072855 * 10 ^ 70 + 1999046455958316796728330058702162114528616157664056397145972335972476)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_73 :
Polynomial.coeff recurrence2Scalar1Shift 73 = 1622542674366702412967520443906098599153676137414703656322803 * 10 ^ 70 + 9240066266458848257618691133410396591156423544993188546351718371090331
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_74 :
Polynomial.coeff recurrence2Scalar1Shift 74 = -(16308434271361053750318107751008868888638622146319240153840685 * 10 ^ 70 + 6671931033312019544869430521397611888923915597613122855085559596736497)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_75 :
Polynomial.coeff recurrence2Scalar1Shift 75 = 156564523123171634046093697860308613227269468503735395528144565 * 10 ^ 70 + 4564442054791121112067911488261716278313552433968242025997884219595299
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_76 :
Polynomial.coeff recurrence2Scalar1Shift 76 = -(1437151280980505771464293743749454552692909285217545768661034003 * 10 ^ 70 + 3073003551053707246872046796536705098000584372131757385185950654063964)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_77 :
Polynomial.coeff recurrence2Scalar1Shift 77 = 12626243658982935853367534969424024919397700939916055350369077950 * 10 ^ 70 + 8053276391910442901051577959912161592869226066836109364035328301336187
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_78 :
Polynomial.coeff recurrence2Scalar1Shift 78 = -(106265957145959510785128762301524213476504073102585083889201221895 * 10 ^ 70 + 9108697304233680162054571739292583322840246905541858655294869481250160)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_79 :
Polynomial.coeff recurrence2Scalar1Shift 79 = 857430627240706556484671389161169950045554040399604208704149832814 * 10 ^ 70 + 361290687820909652960185820389069156733406084448128777330476607317696
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_80 :
Polynomial.coeff recurrence2Scalar1Shift 80 = -(6637275967864751432642307909390076953443586525517241237693484488539 * 10 ^ 70 + 5225971741128473253119893504853305658654827474509217433799255453107689)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_81 :
Polynomial.coeff recurrence2Scalar1Shift 81 = 49323065680198931510216066423162911361932253647007125635483547310022 * 10 ^ 70 + 6079699374049331387272611679530558785341007258493118151547942925974374
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_82 :
Polynomial.coeff recurrence2Scalar1Shift 82 = -(352091177717691747367356570624584762267847265398291957597876910273265 * 10 ^ 70 + 6517975709224833825584647941944289661604386042687140881661042163526437)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_83 :
Polynomial.coeff recurrence2Scalar1Shift 83 = 2415854132369087613604366291870847022470528178110128730987110502540403 * 10 ^ 70 + 1806020926554379316727145591370056908409266919296076925097812725192158
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_84 :
Polynomial.coeff recurrence2Scalar1Shift 84 = -((1 * 10 ^ 70 + 5941847075750540278461636292256730854945145385998618644752971366397957) * 10 ^ 70 + 6854821059568194919604490855840371591263601399775204624269500018343917)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_85 :
Polynomial.coeff recurrence2Scalar1Shift 85 = (10 * 10 ^ 70 + 1218259132280503187157427037842149549240012813504479607716564333991609) * 10 ^ 70 + 1456722631946566106081084150439551575216749690264426391963388057149072
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_86 :
Polynomial.coeff recurrence2Scalar1Shift 86 = -((61 * 10 ^ 70 + 8551348818087722419334777507516637704071295493471744877255328654439906) * 10 ^ 70 + 4495330997879716947839192813184721780417591026811148062355106876969372)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_87 :
Polynomial.coeff recurrence2Scalar1Shift 87 = (363 * 10 ^ 70 + 8953460982193594361496166857536094865232481802817417927668217567487496) * 10 ^ 70 + 5116010387689510562166121752294014851155635908431062138003116635984065
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_88 :
Polynomial.coeff recurrence2Scalar1Shift 88 = -((2061 * 10 ^ 70 + 1190641101727948108027794663826591442480565346681503476110783444296133) * 10 ^ 70 + 4686986289786672600976517605001199423759893554356132364590787637974382)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_89 :
Polynomial.coeff recurrence2Scalar1Shift 89 = (11240 * 10 ^ 70 + 1468903513908936368985292179390482346732652821021776792482059093216484) * 10 ^ 70 + 3363079492988062225346696415878577286416736551052747812338928798350025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_90 :
Polynomial.coeff recurrence2Scalar1Shift 90 = -((59018 * 10 ^ 70 + 5849668081271386330558822756784665164369460421017975925744361140284291) * 10 ^ 70 + 9011821135683726481977910690702346038801568924514457785799036598093793)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_91 :
Polynomial.coeff recurrence2Scalar1Shift 91 = (298361 * 10 ^ 70 + 374117681494643982844778200168321202032206578622106728527494174395824) * 10 ^ 70 + 7049493312145709565653917184495782462391211283236724558605895521915851