Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupB5A6Part0

Recurrence 2 lookup certificate: B5A6 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.recurrence2B5A6_coeff_0 :
Polynomial.coeff recurrence2B5A6 0 = -38784
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_1 :
Polynomial.coeff recurrence2B5A6 1 = -9554040
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_2 :
Polynomial.coeff recurrence2B5A6 2 = -775611249548
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_3 :
Polynomial.coeff recurrence2B5A6 3 = -54761791975288
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_4 :
Polynomial.coeff recurrence2B5A6 4 = 671998376665411956
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_5 :
Polynomial.coeff recurrence2B5A6 5 = -458891331588737950804
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_6 :
Polynomial.coeff recurrence2B5A6 6 = 417202843530225184084702
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_7 :
Polynomial.coeff recurrence2B5A6 7 = -131042986046673025848100306
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_8 :
Polynomial.coeff recurrence2B5A6 8 = 25738914503343946042763378280
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_9 :
Polynomial.coeff recurrence2B5A6 9 = -3045413394047472082237257527604
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_10 :
Polynomial.coeff recurrence2B5A6 10 = 145189759210565985029649602088632
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_11 :
Polynomial.coeff recurrence2B5A6 11 = 7218716176449186645996165109537727
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_12 :
Polynomial.coeff recurrence2B5A6 12 = -1756345587377771328491190821512483117
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_13 :
Polynomial.coeff recurrence2B5A6 13 = 130920166036798931638893652742492404182
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_14 :
Polynomial.coeff recurrence2B5A6 14 = -5027754702255942062074150609405946227916
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_15 :
Polynomial.coeff recurrence2B5A6 15 = 99723248684694938604571484125414054689149
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_16 :
Polynomial.coeff recurrence2B5A6 16 = -560061588122533137554984691161946116577834
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_17 :
Polynomial.coeff recurrence2B5A6 17 = -51925565642336704706998342281132929545779273
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_18 :
Polynomial.coeff recurrence2B5A6 18 = 8451507781218615056302501601500508615923156461
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_19 :
Polynomial.coeff recurrence2B5A6 19 = -648575333057055657489243912496203991309704442923
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_20 :
Polynomial.coeff recurrence2B5A6 20 = 25311353116055407625806245894485680828353791437793
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_21 :
Polynomial.coeff recurrence2B5A6 21 = -434027262744381611712679130012364137908407996399406
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_22 :
Polynomial.coeff recurrence2B5A6 22 = -3388169497864445860243440423704843608128708269730719
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_23 :
Polynomial.coeff recurrence2B5A6 23 = 272702117880662339452946502977807531961850085423063582
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_24 :
Polynomial.coeff recurrence2B5A6 24 = -819729594946693267742823923408919503051814574129234282
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_25 :
Polynomial.coeff recurrence2B5A6 25 = -248625948881223657758933251248713935803906589499229518506
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_26 :
Polynomial.coeff recurrence2B5A6 26 = 9724860811484387472764468222604510827894093501392185137283
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_27 :
Polynomial.coeff recurrence2B5A6 27 = -215609852928463842160613069741620260846771591438452698527155
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_28 :
Polynomial.coeff recurrence2B5A6 28 = 3653963011629553778851149439276719487415789785902075694119236
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_29 :
Polynomial.coeff recurrence2B5A6 29 = -59702259728743277704955111731351365971952471375705556144610903
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_30 :
Polynomial.coeff recurrence2B5A6 30 = 1046228122117749584202212827173027149074034142978822137348909974
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_31 :
Polynomial.coeff recurrence2B5A6 31 = -17131946436112956899557809589131891169297049014501192697168788008
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_32 :
Polynomial.coeff recurrence2B5A6 32 = 212532766525866856145952914687292164538516884666381446667056896506
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_33 :
Polynomial.coeff recurrence2B5A6 33 = -1353939162632490856699811968178905835009737991024114247356822505565
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_34 :
Polynomial.coeff recurrence2B5A6 34 = -14125872334864864303032942414187426289960784928828482724740170689598
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_35 :
Polynomial.coeff recurrence2B5A6 35 = 629229390164346779378803412430118698889182362460713937905204020403351
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_36 :
Polynomial.coeff recurrence2B5A6 36 = -(1 * 10 ^ 70 + 2850173709505610543627702315559423313709243275661149556312169719514750)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_37 :
Polynomial.coeff recurrence2B5A6 37 = 20 * 10 ^ 70 + 7144335680817545303347206925567033152439652496238499625679140126907460
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_38 :
Polynomial.coeff recurrence2B5A6 38 = -(295 * 10 ^ 70 + 8288074964774824746952739382698447301666523384471557514784259912420176)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_39 :
Polynomial.coeff recurrence2B5A6 39 = 3839 * 10 ^ 70 + 2554974081308882542900288428299820358471051423206469163285336379695072
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_40 :
Polynomial.coeff recurrence2B5A6 40 = -(45026 * 10 ^ 70 + 2089210945820659467711790570437550030651442848334127054322443519717847)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_41 :
Polynomial.coeff recurrence2B5A6 41 = 475416 * 10 ^ 70 + 7323072393559174385681791739414177623611770439900184582919361402329105
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_42 :
Polynomial.coeff recurrence2B5A6 42 = -(4566774 * 10 ^ 70 + 413120235166560983961208905169658390966752472052683608883411744372292)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_43 :
Polynomial.coeff recurrence2B5A6 43 = 40717626 * 10 ^ 70 + 5355333304940436578101036270523659214125637840181524347629768707731624
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_44 :
Polynomial.coeff recurrence2B5A6 44 = -(342240809 * 10 ^ 70 + 3125862709346907423237947105377724365320289536508139406396320854826497)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_45 :
Polynomial.coeff recurrence2B5A6 45 = 2711826811 * 10 ^ 70 + 2870107661934895200144809478894502006756333313089619236019424514761084
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_46 :
Polynomial.coeff recurrence2B5A6 46 = -(20034710974 * 10 ^ 70 + 3386895313670888366429435510300761648923514450592293188341028360526093)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_47 :
Polynomial.coeff recurrence2B5A6 47 = 137025090621 * 10 ^ 70 + 5645029030403454986574972597427985761081720956979211563845300337553252
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_48 :
Polynomial.coeff recurrence2B5A6 48 = -(873422641013 * 10 ^ 70 + 828898073725481162371034463815140453621105272138822023322184654816913)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_49 :
Polynomial.coeff recurrence2B5A6 49 = 5275992517425 * 10 ^ 70 + 8665661690777834586349378464234913420370743588942476303983572520564504
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_50 :
Polynomial.coeff recurrence2B5A6 50 = -(30544397764441 * 10 ^ 70 + 3130403644057616742408264033894172044015822976064170954027006388586610)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_51 :
Polynomial.coeff recurrence2B5A6 51 = 168353756978784 * 10 ^ 70 + 524256981372877473655543970123135377344694452455367355636372517863413
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_52 :
Polynomial.coeff recurrence2B5A6 52 = -(865887436529464 * 10 ^ 70 + 9766108984917799149587362322276037277768678672733851758377954083379574)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_53 :
Polynomial.coeff recurrence2B5A6 53 = 4082120175438124 * 10 ^ 70 + 1870670741861117309845704478314019775365909018251174782499930164418570
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_54 :
Polynomial.coeff recurrence2B5A6 54 = -(17642206531469258 * 10 ^ 70 + 4629691714924157628307340776348932247574832662180690933152714835457195)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_55 :
Polynomial.coeff recurrence2B5A6 55 = 72476375771213164 * 10 ^ 70 + 3718279689081830629014806259795302093982170629353442469590962069554866
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_56 :
Polynomial.coeff recurrence2B5A6 56 = -(305030011094367821 * 10 ^ 70 + 3937617592548831669563790292613392676623906227601613100872780934029888)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_57 :
Polynomial.coeff recurrence2B5A6 57 = 1349156681612964641 * 10 ^ 70 + 3723430134239118290787511738937545407601788077646020239622169133758627
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_58 :
Polynomial.coeff recurrence2B5A6 58 = -(5419865047269667381 * 10 ^ 70 + 7293732058696238651708957554444465935340886029091044368663667317750549)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_59 :
Polynomial.coeff recurrence2B5A6 59 = 13933964984859365920 * 10 ^ 70 + 6205306244015636153505760594051402812449208061699689063780890020183301
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_60 :
Polynomial.coeff recurrence2B5A6 60 = 4723161816607433501 * 10 ^ 70 + 6875476980494928731393022104087098835202777601133565956129425288494384
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_61 :
Polynomial.coeff recurrence2B5A6 61 = -(145054629643307055065 * 10 ^ 70 + 3049888152975820155330356321144832196037635931104000287731274256010886)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_62 :
Polynomial.coeff recurrence2B5A6 62 = -(365600844222568606955 * 10 ^ 70 + 5948243904459683720412606288797675926575496892229568571948444490108782)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_63 :
Polynomial.coeff recurrence2B5A6 63 = 7827135948682625200184 * 10 ^ 70 + 3948139478133752792930090126353898193801339915636638170166907659455286
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_64 :
Polynomial.coeff recurrence2B5A6 64 = -(26831072876743093606702 * 10 ^ 70 + 9548193278148188602643939503975140094297999080911224192414087705835919)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_65 :
Polynomial.coeff recurrence2B5A6 65 = -(82698614986138283938673 * 10 ^ 70 + 7714806264530922146651437832753744964973487329816455025574987367305319)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_66 :
Polynomial.coeff recurrence2B5A6 66 = 940949275305094182600761 * 10 ^ 70 + 1504275469979386410615276370047256798664246941974485101455456485630542
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_67 :
Polynomial.coeff recurrence2B5A6 67 = -(1854253565410330450044076 * 10 ^ 70 + 7083413291459761231022563937787208449978442936112306079401536607492307)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_68 :
Polynomial.coeff recurrence2B5A6 68 = -(10020053534756363371535479 * 10 ^ 70 + 820189444446390244056167809269356179059635127167349626005462951641167)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_69 :
Polynomial.coeff recurrence2B5A6 69 = 55234172680815827978678854 * 10 ^ 70 + 6192548225367249199996515603711587460062796159883195231140244576033379
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_70 :
Polynomial.coeff recurrence2B5A6 70 = 648822825431784687383058 * 10 ^ 70 + 7284747970515532151780269701491950703507084562064054730941924459530458
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_71 :
Polynomial.coeff recurrence2B5A6 71 = -(497853787055094108373774414 * 10 ^ 70 + 7752499345475618732191373115912396227191097860299638434383547314314866)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_72 :
Polynomial.coeff recurrence2B5A6 72 = -(629478091693482204770533067 * 10 ^ 70 + 3369780158639009110456351139085642876173870549453156460547007041770530)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_73 :
Polynomial.coeff recurrence2B5A6 73 = 6503574031479910330778688207 * 10 ^ 70 + 1138082535351790390646306581726112085152434578952050861665381992002732
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_74 :
Polynomial.coeff recurrence2B5A6 74 = 62509599535327564196284526432 * 10 ^ 70 + 3989365432037486646569497699763957210734759419553786279807528033262938
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_75 :
Polynomial.coeff recurrence2B5A6 75 = -(516258249782494034504715459292 * 10 ^ 70 + 4367585762201113955561356284154302039125782913749043300524129498266031)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_76 :
Polynomial.coeff recurrence2B5A6 76 = 35877995915347627709310867923 * 10 ^ 70 + 6971194446395216373384250003801485457292948936311961829649039258694708
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_77 :
Polynomial.coeff recurrence2B5A6 77 = 13872279905335386121479694888642 * 10 ^ 70 + 7403789588892062931883427578705873108596361969084337660310691575427165
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_78 :
Polynomial.coeff recurrence2B5A6 78 = -(54898150027486896362061656598572 * 10 ^ 70 + 8718711831868152289484060344192558311246676011023548127428084965646692)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_79 :
Polynomial.coeff recurrence2B5A6 79 = -(87485120439113821565966518425420 * 10 ^ 70 + 9216853886651646182677079525661992638831874323824503537083330928105425)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_80 :
Polynomial.coeff recurrence2B5A6 80 = 1375368990497570517927063704147916 * 10 ^ 70 + 146594605576930079929138251749776405722629778002289656969207806277424
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_81 :
Polynomial.coeff recurrence2B5A6 81 = -(3199350001008490085151948905864516 * 10 ^ 70 + 3637723152351264540765778956459204190313949655335168129446543737794692)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_82 :
Polynomial.coeff recurrence2B5A6 82 = -(12323958033081917857652704457884656 * 10 ^ 70 + 9136969446475168635923531374474680312590409716679409673145044799891705)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_83 :
Polynomial.coeff recurrence2B5A6 83 = 89604393549559528617316178273785840 * 10 ^ 70 + 9907736239380774895542197681404605321616887052009456180441415382250826
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_84 :
Polynomial.coeff recurrence2B5A6 84 = -(88465184035476883841793600843188809 * 10 ^ 70 + 909148845743279853831617977431402250663916645139679220645524063245793)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_85 :
Polynomial.coeff recurrence2B5A6 85 = -(1039595670346308433351247073231710293 * 10 ^ 70 + 9483492132519939528916681124360782279232133081685642046086809640862555)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_86 :
Polynomial.coeff recurrence2B5A6 86 = 4231191002979017439312580626380009867 * 10 ^ 70 + 7251561268671653880887335027315785601178039816973249883563470884506213
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_87 :
Polynomial.coeff recurrence2B5A6 87 = 2596507612314067353629904197373429252 * 10 ^ 70 + 1421536852546729392879604693356191853947166560642304304314602641426276
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_88 :
Polynomial.coeff recurrence2B5A6 88 = -(66104339473407325387996381106785174005 * 10 ^ 70 + 6582560301685635697506702914872175351359557957904090198112058952893874)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_89 :
Polynomial.coeff recurrence2B5A6 89 = 153845563944043247019666783854624082686 * 10 ^ 70 + 4266035342931324643287020899603119395264010718211083621192354778869209
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_90 :
Polynomial.coeff recurrence2B5A6 90 = 451642209882154032714194057379926673847 * 10 ^ 70 + 3069284448505985141120073597225689390051687348755410658016947037969126
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_91 :
Polynomial.coeff recurrence2B5A6 91 = -(3432359112521979311837186332256155160110 * 10 ^ 70 + 9002586353146347952903703099612612675645578422066230126154709765113894)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_92 :
Polynomial.coeff recurrence2B5A6 92 = 4668109126527003541182616102254309511252 * 10 ^ 70 + 3831652521547210768845082428941014441022017299611150784478232850038158
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_93 :
Polynomial.coeff recurrence2B5A6 93 = 29111350330009184984308073430942352477373 * 10 ^ 70 + 9023288168353416764441671198171308664297824818555511865679640627185379
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_94 :
Polynomial.coeff recurrence2B5A6 94 = -(150181865322947720191958478623564716159471 * 10 ^ 70 + 4343371073527686027847854683562181772683501072554284161568126370287523)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_95 :
Polynomial.coeff recurrence2B5A6 95 = 133658377046658261138674563434078549981130 * 10 ^ 70 + 5688077376467456010005848503945535893849535169316611187508063501553402
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_96 :
Polynomial.coeff recurrence2B5A6 96 = 1300826843714002832992835626883081839829002 * 10 ^ 70 + 3901704557675136108158206374466926253232998758101677586284713180568335
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_97 :
Polynomial.coeff recurrence2B5A6 97 = -(5674793561351797410447286912198043361012901 * 10 ^ 70 + 7884157573995092183921129694206762394927457488427321174739177886461922)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_98 :
Polynomial.coeff recurrence2B5A6 98 = 4232665829662747373338043172000338399402871 * 10 ^ 70 + 3976485582272896809960716166090950258272755566939912658812689237138097
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_99 :
Polynomial.coeff recurrence2B5A6 99 = 45819813261561924693296391539944189829725702 * 10 ^ 70 + 4343489295546691394919736293053837593184986530525081334084286088741332
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_100 :
Polynomial.coeff recurrence2B5A6 100 = -(191299699078982713192746499316624265292679535 * 10 ^ 70 + 1288429330321875846060121359627449245592802121783857041232156185799724)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_101 :
Polynomial.coeff recurrence2B5A6 101 = 166798082896323668623583469010215268461065906 * 10 ^ 70 + 4214403998932860598698637008303027643250585451183823377480114629211772
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_102 :
Polynomial.coeff recurrence2B5A6 102 = 1300604364415596138552667170543730455190727395 * 10 ^ 70 + 9388982247017535546663838447543187610325304013510348344285407528570656
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_103 :
Polynomial.coeff recurrence2B5A6 103 = -(5820120222442588690656346697925296581063522281 * 10 ^ 70 + 3535385775131798853449962641073726025404767939332365717854047048351617)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_104 :
Polynomial.coeff recurrence2B5A6 104 = 7266514128117928314011078927730650361676573356 * 10 ^ 70 + 9257800800662282048164838482598833966668633017703106879787723642066990
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_105 :
Polynomial.coeff recurrence2B5A6 105 = 27620558069673078631758345828882143323551402740 * 10 ^ 70 + 6849407524026685473402669582322968731717150372414081816315842066024559
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_106 :
Polynomial.coeff recurrence2B5A6 106 = -(154106631817524535152665312398807982674196300292 * 10 ^ 70 + 8999456784410983511624098694947758297626358738207882993484726203814338)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_107 :
Polynomial.coeff recurrence2B5A6 107 = 281058920112652578895302184977082559896132171177 * 10 ^ 70 + 3712974591177079420354233346076315838321853517871352707600821800546334
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_108 :
Polynomial.coeff recurrence2B5A6 108 = 315919973144540254248006534188786162398218626057 * 10 ^ 70 + 9460809034724628797307823517614725592981389297212972165684980385793329
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_109 :
Polynomial.coeff recurrence2B5A6 109 = -(3276522501839849682143736862337717477105233237990 * 10 ^ 70 + 6210841020724366692382167954734110191252198603464447328411234757615131)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_110 :
Polynomial.coeff recurrence2B5A6 110 = 8565107966128855802693737810321846720251191039464 * 10 ^ 70 + 5114248608582477912450321757624735440232746296409944551734604798873628
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_111 :
Polynomial.coeff recurrence2B5A6 111 = -(4392448265973102728292502033319139424542855705619 * 10 ^ 70 + 7443130682325796686227345440298455651424554632692103707733529926578071)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_112 :
Polynomial.coeff recurrence2B5A6 112 = -(47139866491872913812875234324397532799122320528837 * 10 ^ 70 + 9262369894500814156310924048225343372593113784808625558970232037011461)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_113 :
Polynomial.coeff recurrence2B5A6 113 = 190080875587042055842930536032338051662684048308989 * 10 ^ 70 + 2483697202394919926631239893726917770000615813770555226533017285883117
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_114 :
Polynomial.coeff recurrence2B5A6 114 = -(322295819982687675798990632983381677946557567188469 * 10 ^ 70 + 704023665074631118533891695008293978006892710778048170976095941336174)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_115 :
Polynomial.coeff recurrence2B5A6 115 = -(163233485660436515250960397160895904933620214649650 * 10 ^ 70 + 953088284085711603216975310131841750565730797312762139860244633752945)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_116 :
Polynomial.coeff recurrence2B5A6 116 = 2620070916444834605964972834913641156089342332878378 * 10 ^ 70 + 4475572188660832797718956140995141590879167888393439235780660729678504
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_117 :
Polynomial.coeff recurrence2B5A6 117 = -(7897221511208887146898317543842705730849753992323790 * 10 ^ 70 + 6092431893926259796935746390733887656074602674561194740841598285583077)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_118 :
Polynomial.coeff recurrence2B5A6 118 = 11115548229114754464987797838211564480837627437195021 * 10 ^ 70 + 8565524307000796667477520912974231935161917439528809310107068474314649
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_119 :
Polynomial.coeff recurrence2B5A6 119 = 8168535559987283844595320080940391317022745723296985 * 10 ^ 70 + 9460207884898234279632431543490834506017417482434439855443808279963765
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_120 :
Polynomial.coeff recurrence2B5A6 120 = -(90581540945232280138396726740931046090679195520270275 * 10 ^ 70 + 3421086595763968017379954075077409981189523390569481016810592391299485)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_121 :
Polynomial.coeff recurrence2B5A6 121 = 264257601495413075921537504213113100848731245230050563 * 10 ^ 70 + 5723869865386810497615518873499777462642599836228062606565677629926880
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_122 :
Polynomial.coeff recurrence2B5A6 122 = -(422798613900964735722545287179832723262279438798982197 * 10 ^ 70 + 7145803513010991986413242214822925662213303710743688734362350295683879)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_123 :
Polynomial.coeff recurrence2B5A6 123 = 93475519161689878298855944290561527701628119017512611 * 10 ^ 70 + 2156218686571295284835200273937127689231274200278998547795199493096863
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_124 :
Polynomial.coeff recurrence2B5A6 124 = 1760817251812309100560836502740167595872085838745969137 * 10 ^ 70 + 2483660655330826767340270857131061484913515099936365114144118002026662
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_125 :
Polynomial.coeff recurrence2B5A6 125 = -(6422861857635189458716449909504445779239553115793606118 * 10 ^ 70 + 5325689073607060614895350185230384066314131237767776856192010306909073)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_126 :
Polynomial.coeff recurrence2B5A6 126 = 13729951126686308658255782353899224631812571335197864071 * 10 ^ 70 + 8242149564341649854621454376156245395315199369317548042974479253490298
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_127 :
Polynomial.coeff recurrence2B5A6 127 = -(18223651281204271788382796403127023368684892331942111194 * 10 ^ 70 + 9298574920696712420695571387927007359648261116208583572875119767629236)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_128 :
Polynomial.coeff recurrence2B5A6 128 = 3602586341296450051538626612423969138152560414318777463 * 10 ^ 70 + 9813493946004212650920640083477096690835713923741469132158667507034080
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_129 :
Polynomial.coeff recurrence2B5A6 129 = 61160450123225470416161657341872976648080983577828261536 * 10 ^ 70 + 4308258764722777457154890138900446104337741732271101581362171051723146
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_130 :
Polynomial.coeff recurrence2B5A6 130 = -(216881034753449729439713935575572469679360455244507024294 * 10 ^ 70 + 8076782877733719762950906170700513465106624197950914648797171231816810)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_131 :
Polynomial.coeff recurrence2B5A6 131 = 491312593213519588987547340607055225281853965460202187170 * 10 ^ 70 + 5947542327869007258605114126060745281534855110622856074092474604152303
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_132 :
Polynomial.coeff recurrence2B5A6 132 = -(853421894441487147152814212057186617934739302454403195290 * 10 ^ 70 + 3999206640819575180514119552720111999751102084973202689855201153428590)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_133 :
Polynomial.coeff recurrence2B5A6 133 = 1153004341719073497311889721875924040807455076652084714004 * 10 ^ 70 + 6410125115520059423478050290643193022725192219462588055195425128807698
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_134 :
Polynomial.coeff recurrence2B5A6 134 = -(1073685710136208461380453202928928373005331169603958096983 * 10 ^ 70 + 8504046050072934760095236837987987452753252099700136553255458156672651)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_135 :
Polynomial.coeff recurrence2B5A6 135 = 143468759218230389206430650930676558615963973155366997855 * 10 ^ 70 + 2908287664721236597501869905539684292382945383216604257068264494179798
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_136 :
Polynomial.coeff recurrence2B5A6 136 = 2156317743565859460232260469488089996969886054986203245047 * 10 ^ 70 + 3714296586961962652149389354304518148096870376120693448399682022097324
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_137 :
Polynomial.coeff recurrence2B5A6 137 = -(6177071406110897709340797059413051357693278160836354617362 * 10 ^ 70 + 6642984596289621510035704576904275043309163629283510868671419659265238)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_138 :
Polynomial.coeff recurrence2B5A6 138 = 11837818665488493448838851773938903682435865589844995405835 * 10 ^ 70 + 9405803002843559748812808612425364648681176900615726850759979553875518
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_139 :
Polynomial.coeff recurrence2B5A6 139 = -(18422537181938165192947293367212802951681544322312677423832 * 10 ^ 70 + 1817371382853910333788291908182282325675330611541560321199212493526337)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_140 :
Polynomial.coeff recurrence2B5A6 140 = 24572431035768422246264124040727766558683241163945594155956 * 10 ^ 70 + 971190094401412397581934691958357328468986977472992177175633357133019
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_141 :
Polynomial.coeff recurrence2B5A6 141 = -(28554231422681740996528568936397591015498733668005919010551 * 10 ^ 70 + 3506878682575682974071699490922726751121487559669058703353109874895083)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_142 :
Polynomial.coeff recurrence2B5A6 142 = 28769665994589121902594798490530601863748273725193955834350 * 10 ^ 70 + 3537183378553252587269682861174118586243994040246664519879421143057012
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_143 :
Polynomial.coeff recurrence2B5A6 143 = -(24340346603047287987313825623517592541991427726872544422554 * 10 ^ 70 + 5099057361230622257155461448375674981216732853071802131080482967504263)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_144 :
Polynomial.coeff recurrence2B5A6 144 = 15528663241256443393320915404635548653932759112064803853359 * 10 ^ 70 + 6922864337964232314203455391924513683391802465483180501545432262422413
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_145 :
Polynomial.coeff recurrence2B5A6 145 = -(3791874049045005077803638824392240419661530389959449240157 * 10 ^ 70 + 4047389487282513091192182515829941518576785837464516431060043868548203)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_146 :
Polynomial.coeff recurrence2B5A6 146 = -(8589915153084222358899569911085422179996482610427652718872 * 10 ^ 70 + 3333990676098169530046645075728172190892784652726078829792034839339079)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_147 :
Polynomial.coeff recurrence2B5A6 147 = 19186203676695045180161922533754933893294537290356138022865 * 10 ^ 70 + 4158405468866757637739934193207955709562881950998187632578000781157309
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_148 :
Polynomial.coeff recurrence2B5A6 148 = -(26130545538753442487972387761072156974866501836256819322244 * 10 ^ 70 + 1290803143962221317360796140474151010108347934179750536062354056123084)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_149 :
Polynomial.coeff recurrence2B5A6 149 = 28606159976423835619595431625225982641689695796304024265503 * 10 ^ 70 + 8388177555126969513846367162560698145261580482614366880679660440901955
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_150 :
Polynomial.coeff recurrence2B5A6 150 = -(26942859582643004968477672810553056988960046858646580054849 * 10 ^ 70 + 2510707770956105023496804251577112190718135896376055299811082060294918)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_151 :
Polynomial.coeff recurrence2B5A6 151 = 22338022591824665694075010471763333159430437738846221144442 * 10 ^ 70 + 2357096143804276536596348818330222069320073906667053558190960894873706
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_152 :
Polynomial.coeff recurrence2B5A6 152 = -(16360338360673668735657824186371217621510949997752307905757 * 10 ^ 70 + 4671908352282809227327664617779524597711573246860068255107440409583352)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_153 :
Polynomial.coeff recurrence2B5A6 153 = 10450434108008480708891714671552092775044306296809865082600 * 10 ^ 70 + 9699234406953846875111312849573924561718920294657429568653473840614375
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_154 :
Polynomial.coeff recurrence2B5A6 154 = -(5587906624862406401353012253271504211787737844374676170304 * 10 ^ 70 + 5726976230142180325253244332421016588707628178068007417781929803653363)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_155 :
Polynomial.coeff recurrence2B5A6 155 = 2190530029337243438149072222747813456100210108172318822034 * 10 ^ 70 + 3093138959642922381599474934387833551744996247056539142212472316851704
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_156 :
Polynomial.coeff recurrence2B5A6 156 = -(208293487410504682490436237340270878248850828576109700316 * 10 ^ 70 + 2124741426931850076693474252599669507546358648230512382690268768481174)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_157 :
Polynomial.coeff recurrence2B5A6 157 = -(683269246255285434533504978884653843284932920879269403270 * 10 ^ 70 + 6132406700203077381408118011304734692307447174233993371540432394516458)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_158 :
Polynomial.coeff recurrence2B5A6 158 = 888217143171099649387916922625681769505215265675226369101 * 10 ^ 70 + 8535987109907558884678685907071145078612543109546741975474498889093071
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_159 :
Polynomial.coeff recurrence2B5A6 159 = -(755533291351298597718891163441562557952851267183794347561 * 10 ^ 70 + 2856803945729201411607183928687648355467035936448123498106394889069661)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_160 :
Polynomial.coeff recurrence2B5A6 160 = 520767046583138081300293871662100806848417075684347277537 * 10 ^ 70 + 2572940043723122978483432138550322692201695447572055943211083810245884
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_161 :
Polynomial.coeff recurrence2B5A6 161 = -(307168500400924906746556667234979247733354713280913887159 * 10 ^ 70 + 709302317554714157556746244075224048078894664793914761513310706886311)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_162 :
Polynomial.coeff recurrence2B5A6 162 = 157162689700482792581269292935907768275034842606997202297 * 10 ^ 70 + 4146631701788964830753118806918297931589777990125503705918835603381559
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_163 :
Polynomial.coeff recurrence2B5A6 163 = -(69042369644045785568185346534032639399009216213763753468 * 10 ^ 70 + 9419223579125783232374694774354948783020274398237196937758054457460636)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_164 :
Polynomial.coeff recurrence2B5A6 164 = 24908192544710496233092172795309347369680829271167950030 * 10 ^ 70 + 7176788661057311035551202820900634623229674109365233946173771188095791
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_165 :
Polynomial.coeff recurrence2B5A6 165 = -(6311977307240465951205834311617631266889534277193947745 * 10 ^ 70 + 4355530723600114888821213866584199665498819536473346820670378512687097)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_166 :
Polynomial.coeff recurrence2B5A6 166 = 122520971693433166718603503821170235981432232769347873 * 10 ^ 70 + 1670964145179527964887146532952005884295029584750646030374738250142346
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_167 :
Polynomial.coeff recurrence2B5A6 167 = 1120241249634827447695471733162118258917227557572746691 * 10 ^ 70 + 7541834596164274601010981194662404238234846094678430946375368344329231
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_168 :
Polynomial.coeff recurrence2B5A6 168 = -(891715695625811432431483935562263580223899413209988982 * 10 ^ 70 + 5614479202507224664521245260277354226338756359291107526672333588697930)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_169 :
Polynomial.coeff recurrence2B5A6 169 = 479153845674924322536683071286811466255982410353663282 * 10 ^ 70 + 7026701177069466746359724880923889569048553345118977862466940095611901
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_170 :
Polynomial.coeff recurrence2B5A6 170 = -(206235833317602416685596746723470711882588807359233284 * 10 ^ 70 + 561481815909494665253922858452520297514427361079780179175259416644521)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_171 :
Polynomial.coeff recurrence2B5A6 171 = 73804134542800090405423702245237875628766995415821580 * 10 ^ 70 + 8063894252254607810565424143013895588432578011975454088777419773530803
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_172 :
Polynomial.coeff recurrence2B5A6 172 = -(21707745651788686657493789569536690353546960667732890 * 10 ^ 70 + 2297034975459372995345987834371964799717988354278626542342007244613569)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_173 :
Polynomial.coeff recurrence2B5A6 173 = 4860184785282559133287938746409535094505588662012754 * 10 ^ 70 + 9626355488049212473184857520456301910919108464469019990049182265878338
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_174 :
Polynomial.coeff recurrence2B5A6 174 = -(562208379012828988172393319399882964092857774612970 * 10 ^ 70 + 6634559073963576265896021995583413778793875063513077315372152799381214)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_175 :
Polynomial.coeff recurrence2B5A6 175 = -(154412297419670876431387381566375899592038321330392 * 10 ^ 70 + 7307563770286921474952331708883358656073013152619784829315130701055860)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_176 :
Polynomial.coeff recurrence2B5A6 176 = 131502936900234025172193508256449059122428964587862 * 10 ^ 70 + 4534028652187925475183960369081561003787318170997104180122138286707514
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_177 :
Polynomial.coeff recurrence2B5A6 177 = -(54013815206540870754159365354752165397121472420438 * 10 ^ 70 + 1554583315324996039730079204968070332388147063700992084293877285484521)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_178 :
Polynomial.coeff recurrence2B5A6 178 = 16293090375914160093864086556986711585048019915436 * 10 ^ 70 + 1729134864447877590064676113960173084899599085898035605048345656041281
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_179 :
Polynomial.coeff recurrence2B5A6 179 = -(3825161769058816263098103900963431382173392794092 * 10 ^ 70 + 8324400496787751379597888787752362254269344895051304625919113791641885)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_180 :
Polynomial.coeff recurrence2B5A6 180 = 667929722383432105648171243313851300643370433704 * 10 ^ 70 + 6338787025526484817396651660958396626070863949359256692471441368724543
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_181 :
Polynomial.coeff recurrence2B5A6 181 = -(64377891752151302333859506806071388983520111556 * 10 ^ 70 + 6978521057436618895924055086461499208048927533095718431700276177858121)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_182 :
Polynomial.coeff recurrence2B5A6 182 = -(7813261889507937113842875614988552612854110866 * 10 ^ 70 + 5741374039493513695771312525629134782019256541212048835943524492898971)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_183 :
Polynomial.coeff recurrence2B5A6 183 = 5597441094407044582119292741379008637303156451 * 10 ^ 70 + 2835005001558599613227254917539271362389195477239919977009301056750471
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_184 :
Polynomial.coeff recurrence2B5A6 184 = -(1576897651833143222450795635519530309815810716 * 10 ^ 70 + 2123237850704447416338202722461186974922164275912429693937743387100795)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_185 :
Polynomial.coeff recurrence2B5A6 185 = 301481699130115216274336614218152019058761888 * 10 ^ 70 + 570751968659522406734490170403825354729721662092854947171190141483297
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_186 :
Polynomial.coeff recurrence2B5A6 186 = -(39767300556200834787151499444798353542057085 * 10 ^ 70 + 3756587419712965796151928569973437409900549624352932716880083049927106)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_187 :
Polynomial.coeff recurrence2B5A6 187 = 2604747321226694304942050504226166530440640 * 10 ^ 70 + 3551920125117519691580797220709481951588036657427933617148583771214377
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_188 :
Polynomial.coeff recurrence2B5A6 188 = 302221171343532743121979638714362520264833 * 10 ^ 70 + 3200363844491636568134322025383050309220501427363654177293105846121254
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_189 :
Polynomial.coeff recurrence2B5A6 189 = -(126341740952666921184752762969476454869110 * 10 ^ 70 + 8924821917899642804678016656157066640306079409736458957310809075282107)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_190 :
Polynomial.coeff recurrence2B5A6 190 = 21655948538343665712073709124632053302532 * 10 ^ 70 + 3639756893814728776314476050882614354741701987912069916353002586546190
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_191 :
Polynomial.coeff recurrence2B5A6 191 = -(2238399925325495193109752483226732225559 * 10 ^ 70 + 5242804064696556816811844139792077580077080098320038324401245920123611)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_192 :
Polynomial.coeff recurrence2B5A6 192 = 100192504675072601022132672261941272153 * 10 ^ 70 + 4421470773431346123137221128823525061006796366924939108488900520445131
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_193 :
Polynomial.coeff recurrence2B5A6 193 = 10612341784811957542948807966871792189 * 10 ^ 70 + 7050788433393927137913623167808975825091400254437121937637500651232184
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_194 :
Polynomial.coeff recurrence2B5A6 194 = -(2596436452403114198079693668671127128 * 10 ^ 70 + 2959574556605831401555165645035917485808615396201044064817106488100468)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_195 :
Polynomial.coeff recurrence2B5A6 195 = 249419936435603285284791281921477055 * 10 ^ 70 + 2664697717367407211153150220465211173271409072171422237724728480659541
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_196 :
Polynomial.coeff recurrence2B5A6 196 = -(10091192818589072600418706025916823 * 10 ^ 70 + 5372289023217327855403494060603398574893058836639574030845371311072859)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_197 :
Polynomial.coeff recurrence2B5A6 197 = -(483516215683355745789656674320164 * 10 ^ 70 + 4625711777377109375726139007373555362255102931524781934496147137127159)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_198 :
Polynomial.coeff recurrence2B5A6 198 = 92896189412938660772686693766652 * 10 ^ 70 + 3417968821828964046790311059453167260877197917875845205395329183310470
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_199 :
Polynomial.coeff recurrence2B5A6 199 = -(5034629359224923274264301358832 * 10 ^ 70 + 7347784534501821216660526403741648557632034474512252211043230426929362)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_200 :
Polynomial.coeff recurrence2B5A6 200 = 18826644932617963824146300896 * 10 ^ 70 + 6499985828457793275235487730435160641030347011880488977002768418457409
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_201 :
Polynomial.coeff recurrence2B5A6 201 = 11586179749058206792664801765 * 10 ^ 70 + 2731760035672117407057117608946356915606382168513324677808564650556073
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_202 :
Polynomial.coeff recurrence2B5A6 202 = -(505044280677479482679271208 * 10 ^ 70 + 9615585669799697301975902311518637001554577432122449583801577522908950)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_203 :
Polynomial.coeff recurrence2B5A6 203 = -(719450407007150669698726 * 10 ^ 70 + 4365020648602119052299435707906110399733277693674203748467510145028637)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_204 :
Polynomial.coeff recurrence2B5A6 204 = 528046615729000389457662 * 10 ^ 70 + 5755622265240973861502531425861923442913083002434536629600851713535166
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_205 :
Polynomial.coeff recurrence2B5A6 205 = -(7617586486932188576880 * 10 ^ 70 + 948874366480435363255027821537952867865037581736626782555249107542385)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_206 :
Polynomial.coeff recurrence2B5A6 206 = -(175926196577227049959 * 10 ^ 70 + 8671893781778350890669632836629414418581573713778416350129747808018787)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_207 :
Polynomial.coeff recurrence2B5A6 207 = 3290419657336534073 * 10 ^ 70 + 1257958659154329208253443992529517706711345785926722253505669671992716
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_208 :
Polynomial.coeff recurrence2B5A6 208 = 26525765013690811 * 10 ^ 70 + 5633923113597357439146771189607236055117268228034813049384872630548752
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_209 :
Polynomial.coeff recurrence2B5A6 209 = -(413208691665808 * 10 ^ 70 + 9834987160521264234161963816095081993483784027231427844009162996844332)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_210 :
Polynomial.coeff recurrence2B5A6 210 = -(2308775710790 * 10 ^ 70 + 3787076629380299654538445120040204682614022434483132768223910443566492)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_211 :
Polynomial.coeff recurrence2B5A6 211 = 17669729934 * 10 ^ 70 + 5826829448701052860196770326475099334448476155324106825205089624743924
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_212 :
Polynomial.coeff recurrence2B5A6 212 = 89921022 * 10 ^ 70 + 732987870823816054371313625342272042158706106881973138687886112439212
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_213 :
Polynomial.coeff recurrence2B5A6 213 = -(287146 * 10 ^ 70 + 5579345454568344355515567261703240265030372260390051779332915585468812)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_214 :
Polynomial.coeff recurrence2B5A6 214 = -(1314 * 10 ^ 70 + 4073973700480964046569418925398588319943153247395331554220214235216825)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_215 :
Polynomial.coeff recurrence2B5A6 215 = 2 * 10 ^ 70 + 4654137165483896561600070961803398528392126344112076430343097412079616
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_216 :
Polynomial.coeff recurrence2B5A6 216 = 76009889025658934244292396766375998545648963184867802738203436007732
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_217 :
Polynomial.coeff recurrence2B5A6 217 = -126514700701944697320757962662840619824600259027243913635868449596
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_218 :
Polynomial.coeff recurrence2B5A6 218 = -132827894524043477466213019899594939341439474931724564246045460
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_219 :
Polynomial.coeff recurrence2B5A6 219 = 247903174913007753342138830410187476382045041194203116007127
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_220 :
Polynomial.coeff recurrence2B5A6 220 = -13574613626135994902360235302546928417931660176350449347
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_221 :
Polynomial.coeff recurrence2B5A6 221 = -57563639112097116561954567451077295652677154996655375
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_222 :
Polynomial.coeff recurrence2B5A6 222 = 9068578571047909891010716792409519624685283159228
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A6_coeff_223 :
Polynomial.coeff recurrence2B5A6 223 = 395517672689918353189157199637154378164600507