Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupB4A6Part0

Recurrence 2 lookup certificate: B4A6 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.recurrence2B4A6_coeff_0 :
Polynomial.coeff recurrence2B4A6 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_1 :
Polynomial.coeff recurrence2B4A6 1 = 295728
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_2 :
Polynomial.coeff recurrence2B4A6 2 = -48295795824
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_3 :
Polynomial.coeff recurrence2B4A6 3 = 11380898154160
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_4 :
Polynomial.coeff recurrence2B4A6 4 = 21598233311031824
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_5 :
Polynomial.coeff recurrence2B4A6 5 = -41194443091183345662
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_6 :
Polynomial.coeff recurrence2B4A6 6 = 53663840590700019297070
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_7 :
Polynomial.coeff recurrence2B4A6 7 = -23201524811652649489317600
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_8 :
Polynomial.coeff recurrence2B4A6 8 = 6098384957416218257344594398
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_9 :
Polynomial.coeff recurrence2B4A6 9 = -967953883078739939065921892155
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_10 :
Polynomial.coeff recurrence2B4A6 10 = 82892725783670667050666120873497
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_11 :
Polynomial.coeff recurrence2B4A6 11 = -1856144981353864917369446457650050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_12 :
Polynomial.coeff recurrence2B4A6 12 = -418701722368172578450414016960435205
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_13 :
Polynomial.coeff recurrence2B4A6 13 = 53611332834662267149424948994957601241
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_14 :
Polynomial.coeff recurrence2B4A6 14 = -3185093436539119316315991098271185135461
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_15 :
Polynomial.coeff recurrence2B4A6 15 = 112451180904710347015447621732166949269575
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_16 :
Polynomial.coeff recurrence2B4A6 16 = -2536287263410646068245888271242111311817062
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_17 :
Polynomial.coeff recurrence2B4A6 17 = 15464610791107382615882761952051314700221623
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_18 :
Polynomial.coeff recurrence2B4A6 18 = 5041024901670907908739882386076868523552568090
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_19 :
Polynomial.coeff recurrence2B4A6 19 = -514545343892590812237813661860878863893958931013
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_20 :
Polynomial.coeff recurrence2B4A6 20 = 26135766769116887304174423662302095000898932627535
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_21 :
Polynomial.coeff recurrence2B4A6 21 = -713975941654232862247491182844984579150037390972059
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_22 :
Polynomial.coeff recurrence2B4A6 22 = 6364516141121975508613822390095566667933740711341968
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_23 :
Polynomial.coeff recurrence2B4A6 23 = 211606907927080171452140608897258356426137927726270856
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_24 :
Polynomial.coeff recurrence2B4A6 24 = -5726442534940814527079383005217419683906698480954774156
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_25 :
Polynomial.coeff recurrence2B4A6 25 = -110654624884211810069518631625534659370814452741843849159
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_26 :
Polynomial.coeff recurrence2B4A6 26 = 9688211259847801047412255167794589521267234038737742147557
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_27 :
Polynomial.coeff recurrence2B4A6 27 = -293939945456433595613613137081695957143817080647288067092396
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_28 :
Polynomial.coeff recurrence2B4A6 28 = 5893091686577840561127797707023068209825249876914095050328484
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_29 :
Polynomial.coeff recurrence2B4A6 29 = -97012077887686224003577964860533861189828907690353098810986885
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_30 :
Polynomial.coeff recurrence2B4A6 30 = 1584039089259065660967448053901442453566192953046119703156479092
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_31 :
Polynomial.coeff recurrence2B4A6 31 = -26680850485154536731846652686473466498860477993982791939292269636
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_32 :
Polynomial.coeff recurrence2B4A6 32 = 393937779483486943736014890483418792425527482303210872400867641202
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_33 :
Polynomial.coeff recurrence2B4A6 33 = -3926449751156599965407807304831634326923457929780200060774221978630
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_34 :
Polynomial.coeff recurrence2B4A6 34 = 3089325876132521739556067881023944132187159886464478242182263545851
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_35 :
Polynomial.coeff recurrence2B4A6 35 = 860324505091281878683508810819303258149306430595689417024321225655268
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_36 :
Polynomial.coeff recurrence2B4A6 36 = -(2 * 10 ^ 70 + 2799397858270844487058443609146349430045707223163289756417522725013962)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_37 :
Polynomial.coeff recurrence2B4A6 37 = 41 * 10 ^ 70 + 2242881961742226547995794359975724593305217207610837303130504233105905
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_38 :
Polynomial.coeff recurrence2B4A6 38 = -(629 * 10 ^ 70 + 6184155950720443271770505796746843230518910392448592222420320574362853)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_39 :
Polynomial.coeff recurrence2B4A6 39 = 8667 * 10 ^ 70 + 8251042864695491368250257557711508754581580301680174604782554788184390
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_40 :
Polynomial.coeff recurrence2B4A6 40 = -(108874 * 10 ^ 70 + 7370810659229774481908346542081046482383265783613196278293657588556749)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_41 :
Polynomial.coeff recurrence2B4A6 41 = 1241927 * 10 ^ 70 + 7973259527099598261338955714172557095541836132167726741383418848106750
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_42 :
Polynomial.coeff recurrence2B4A6 42 = -(12865757 * 10 ^ 70 + 7721239414684442454660171834934652366231794121689630685353983586296209)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_43 :
Polynomial.coeff recurrence2B4A6 43 = 122356386 * 10 ^ 70 + 2090247725801623005294125394712216025673987307507814678026343351117576
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_44 :
Polynomial.coeff recurrence2B4A6 44 = -(1085302177 * 10 ^ 70 + 63430485144682885490348489986098615883508380234307859241339807723043)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_45 :
Polynomial.coeff recurrence2B4A6 45 = 9072560584 * 10 ^ 70 + 8597391108321619552676219120839218295243529026565019007124345114018226
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_46 :
Polynomial.coeff recurrence2B4A6 46 = -(71417844344 * 10 ^ 70 + 5835489196391255323745921427788325602388782404494510781704101443492398)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_47 :
Polynomial.coeff recurrence2B4A6 47 = 525513909879 * 10 ^ 70 + 4378660265969109729680764698281784187784728660960962677841329613043670
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_48 :
Polynomial.coeff recurrence2B4A6 48 = -(3600763800428 * 10 ^ 70 + 7438602102700346942624773929516319985308690755053007655162361253183451)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_49 :
Polynomial.coeff recurrence2B4A6 49 = 23103734982856 * 10 ^ 70 + 2817806246617596524784561521306848041181672740722565509695052902074401
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_50 :
Polynomial.coeff recurrence2B4A6 50 = -(140520440861794 * 10 ^ 70 + 3319987983862194669949699332810436335745672530270690034934535187610322)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_51 :
Polynomial.coeff recurrence2B4A6 51 = 817174537752128 * 10 ^ 70 + 6497546327858875879410202282329090289995185331786819647423456095298515
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_52 :
Polynomial.coeff recurrence2B4A6 52 = -(4525639111771692 * 10 ^ 70 + 6872406728001613611727152803169700532861403666625708758609607211234438)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_53 :
Polynomial.coeff recurrence2B4A6 53 = 23505188955751254 * 10 ^ 70 + 3611451464977859484497198525337474278982700599169984985621445467797302
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_54 :
Polynomial.coeff recurrence2B4A6 54 = -(112774123996845342 * 10 ^ 70 + 1043927183275366996227370211576402007123576507730529289181129147900351)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_55 :
Polynomial.coeff recurrence2B4A6 55 = 500629990657554129 * 10 ^ 70 + 8038268813136479582166895581089241230386899823743523527016427443305263
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_56 :
Polynomial.coeff recurrence2B4A6 56 = -(2126742139868856210 * 10 ^ 70 + 3550027762967170800824148945422387610020451569185202057922674656290636)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_57 :
Polynomial.coeff recurrence2B4A6 57 = 9126029833500678955 * 10 ^ 70 + 5765451004936134831494805217748463932515677136123577672357356176692013
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_58 :
Polynomial.coeff recurrence2B4A6 58 = -(39557438081517777246 * 10 ^ 70 + 335160837136247849721560610895067515364918785462236216089039368754825)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_59 :
Polynomial.coeff recurrence2B4A6 59 = 154286354705978429373 * 10 ^ 70 + 2887607242931700339502122418500673163430437506706198559786979669172681
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_60 :
Polynomial.coeff recurrence2B4A6 60 = -(436686485481088901672 * 10 ^ 70 + 6058203440820528492598879993294272877811894946865626095699649873859017)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_61 :
Polynomial.coeff recurrence2B4A6 61 = 545579647747844217739 * 10 ^ 70 + 7084788746906813391362741216768202785835537843135968054717230762667949
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_62 :
Polynomial.coeff recurrence2B4A6 62 = 262691054373412947278 * 10 ^ 70 + 3527379802046587344343518720309071519336679647729606033811913335217431
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_63 :
Polynomial.coeff recurrence2B4A6 63 = 12792376864242954440474 * 10 ^ 70 + 9452452838425535214234968302015243037054807521218127728636369566307643
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_64 :
Polynomial.coeff recurrence2B4A6 64 = -(142909730821755173766422 * 10 ^ 70 + 7645808963798339918623537521150685340404843757728746958176308606589110)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_65 :
Polynomial.coeff recurrence2B4A6 65 = 498767023213036882633033 * 10 ^ 70 + 6882757081864799127589947339284825600071445499258515029410219676825347
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_66 :
Polynomial.coeff recurrence2B4A6 66 = 785795622913982209925333 * 10 ^ 70 + 3686207655711903207291297524110070389724972072911605091031805580731064
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_67 :
Polynomial.coeff recurrence2B4A6 67 = -(13699759313921626456394043 * 10 ^ 70 + 1026631486277096696901218333041267273719256404261638721988837159136731)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_68 :
Polynomial.coeff recurrence2B4A6 68 = 44977805553541830882610995 * 10 ^ 70 + 3735758806983638212564946345314201472704865225974512091769294834517535
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_69 :
Polynomial.coeff recurrence2B4A6 69 = 30213848453671358819491298 * 10 ^ 70 + 2594217574227325791657856307298337710262109383948444249126973026548776
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_70 :
Polynomial.coeff recurrence2B4A6 70 = -(747472894894980569019983906 * 10 ^ 70 + 4740409312617299556398216428234550806606266236288138943739096948077154)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_71 :
Polynomial.coeff recurrence2B4A6 71 = 2932628451714858762804814554 * 10 ^ 70 + 3284151188594087695780838887909524366059881296754919882291415374285531
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_72 :
Polynomial.coeff recurrence2B4A6 72 = -(6785287170195378224069793135 * 10 ^ 70 + 1726927665929918630687757484075108146734378295568958197639315073063262)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_73 :
Polynomial.coeff recurrence2B4A6 73 = -(2738509023999403695534031985 * 10 ^ 70 + 7514172592205333805006851391743571001871224453070120210618008290662677)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_74 :
Polynomial.coeff recurrence2B4A6 74 = 249560477544070574237608388252 * 10 ^ 70 + 5986627043733134479214682116033842626560540874832081513847603470783215
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_75 :
Polynomial.coeff recurrence2B4A6 75 = -(1916709751470019726696406990424 * 10 ^ 70 + 7196854050999853931431949317757255516517708802685453642259833509507164)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_76 :
Polynomial.coeff recurrence2B4A6 76 = 4828230528881993466518401307409 * 10 ^ 70 + 9505470983133813108496416479311754814567826771653886069672444301005854
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_77 :
Polynomial.coeff recurrence2B4A6 77 = 23519749310731000592021220841822 * 10 ^ 70 + 4106484428518246456663636453781330157683206343758917925538538532577454
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_78 :
Polynomial.coeff recurrence2B4A6 78 = -(225344506257172816340046025854638 * 10 ^ 70 + 2190142372721398959335885529037527379490930297072153656899159352760023)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_79 :
Polynomial.coeff recurrence2B4A6 79 = 518670615659708372924880108339835 * 10 ^ 70 + 3833369443583498217991503771490694716694410333730356832907334883547337
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_80 :
Polynomial.coeff recurrence2B4A6 80 = 2069266604077174817655299808944178 * 10 ^ 70 + 1964404323376386679350658336460211554345438723053151489570221632885969
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_81 :
Polynomial.coeff recurrence2B4A6 81 = -(16864867846872618670090197051940232 * 10 ^ 70 + 5618942971528122126822783362016835640174693954867670488088267075997186)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_82 :
Polynomial.coeff recurrence2B4A6 82 = 28331904815606710647614414477111370 * 10 ^ 70 + 5625444480584716318233455109660116683979256979599477377170140257172667
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_83 :
Polynomial.coeff recurrence2B4A6 83 = 150740363344684817034991380065717440 * 10 ^ 70 + 9808400276021747393499444915917080159992005142423207162987092745519673
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_84 :
Polynomial.coeff recurrence2B4A6 84 = -(855757421945388756733040797839952951 * 10 ^ 70 + 4304672364506487668050031126830524690564204820642432841985641377453282)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_85 :
Polynomial.coeff recurrence2B4A6 85 = 491481778600053349061153605587800743 * 10 ^ 70 + 4449669442316463206375760096652164439639035010082703788748223971928245
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_86 :
Polynomial.coeff recurrence2B4A6 86 = 9497343440883987218903146892122662845 * 10 ^ 70 + 3986295753714733239135781766695468381494173450845389566808587132691167
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_87 :
Polynomial.coeff recurrence2B4A6 87 = -(29157942109679306806608973608780490376 * 10 ^ 70 + 1877825311225945931567441904073338646737130929696608434293956427625564)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_88 :
Polynomial.coeff recurrence2B4A6 88 = -(57501949268763857598733470289844671022 * 10 ^ 70 + 6665608527798553671387130488376103174120094182038026714964266326310114)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_89 :
Polynomial.coeff recurrence2B4A6 89 = 548786269470432385451233403232636596123 * 10 ^ 70 + 1162876867326974816952916190144472442252073198924152500709442875555951
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_90 :
Polynomial.coeff recurrence2B4A6 90 = -(626591355730027641659098108204590279779 * 10 ^ 70 + 3466297668747282286621774548873636048027372138309053219606337888102621)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_91 :
Polynomial.coeff recurrence2B4A6 91 = -(6223531260094756896647297251109688446350 * 10 ^ 70 + 2156345435574995796501469790282090709770778311125594020101739521198250)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_92 :
Polynomial.coeff recurrence2B4A6 92 = 28511152883231126187190207407854396899129 * 10 ^ 70 + 5539522100451039915601520146055505632787040435695348156916556340867000
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_93 :
Polynomial.coeff recurrence2B4A6 93 = -(7302393996706513440756597861882250478873 * 10 ^ 70 + 2695120974098481996719612738223889394070725340541250821256749223135699)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_94 :
Polynomial.coeff recurrence2B4A6 94 = -(349162565332286461443857099414542656095823 * 10 ^ 70 + 1986923808776978729755371474770291345333088217512462919215531890949087)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_95 :
Polynomial.coeff recurrence2B4A6 95 = 1252333982703520639331779985691691500533862 * 10 ^ 70 + 497270855858671983826415451364611751931853073645351340248633878274692
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_96 :
Polynomial.coeff recurrence2B4A6 96 = -(4091006489272142110232111228995174235196 * 10 ^ 70 + 7628156919512961119702734456871355529604284933674716934484419967504009)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_97 :
Polynomial.coeff recurrence2B4A6 97 = -(14208516035599124162632954863327328301529827 * 10 ^ 70 + 7547034064733587888352382837699780153011597510224976876478359163224756)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_98 :
Polynomial.coeff recurrence2B4A6 98 = 46273581685451388067239302181670332683039091 * 10 ^ 70 + 8984471049490948887230041776455879404025110694221476583470365202160248
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_99 :
Polynomial.coeff recurrence2B4A6 99 = 936442084416790838860116518933150802277568 * 10 ^ 70 + 3984689653217668425498184960561650791407984482168574932631558621354891
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_100 :
Polynomial.coeff recurrence2B4A6 100 = -(480206722237731905778177035325657916000444510 * 10 ^ 70 + 4458462757423212045183062186924149434377166727694156664369342800715543)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_101 :
Polynomial.coeff recurrence2B4A6 101 = 1541836724068147627997844549260490258959164544 * 10 ^ 70 + 9223331678857781731647579538126954512039641331449874329043589599310774
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_102 :
Polynomial.coeff recurrence2B4A6 102 = -(283187357193795881091752199314032986328824892 * 10 ^ 70 + 6877342002341374026755746935446261402917778582639989942386565374782883)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_103 :
Polynomial.coeff recurrence2B4A6 103 = -(13869751646016820276979631724657316459889086206 * 10 ^ 70 + 8781517271466444166627934652293443149487788232072960633427778766601340)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_104 :
Polynomial.coeff recurrence2B4A6 104 = 48237594011882485375717821931071921228776330989 * 10 ^ 70 + 2325103756826172327442481741918590598718016450535770935302113712381663
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_105 :
Polynomial.coeff recurrence2B4A6 105 = -(33237380507910022865996851526963937409186781731 * 10 ^ 70 + 4309823830773572348052542065124818459790833219327894107446805744346553)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_106 :
Polynomial.coeff recurrence2B4A6 106 = -(316446014474861743030751793998826600879539047875 * 10 ^ 70 + 5319500907515132362019470633999636601219141441946665917162654992806116)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_107 :
Polynomial.coeff recurrence2B4A6 107 = 1341622699958988104215666394285125004556735049004 * 10 ^ 70 + 1699497549605809592884784563747584308421619590418741429695713164926285
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_108 :
Polynomial.coeff recurrence2B4A6 108 = -(1849653720704085674789149527146714113213758799258 * 10 ^ 70 + 6776875915483198623192674206936156618744717365160602975763070461026087)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_109 :
Polynomial.coeff recurrence2B4A6 109 = -(4665790845714757253314670025778807758023528653320 * 10 ^ 70 + 2657515607950682379196824298674573563384047202715554284814597785408980)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_110 :
Polynomial.coeff recurrence2B4A6 110 = 30263288033908214649740984042162215887944201460072 * 10 ^ 70 + 1396844241734397174543869788212977879419890285361178578725120958347289
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_111 :
Polynomial.coeff recurrence2B4A6 111 = -(66431252268844708278058708078653744674956726013624 * 10 ^ 70 + 8711695676496518092629605207485632222889213912008420750494098702106245)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_112 :
Polynomial.coeff recurrence2B4A6 112 = -(58043069279496532433944186290514076430532774629 * 10 ^ 70 + 9972001319498707490447403688301253991491757320082641533403106526800802)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_113 :
Polynomial.coeff recurrence2B4A6 113 = 479291015088781095543929569547729210354963882557689 * 10 ^ 70 + 5732730600346603837749591729511294524414604480078883090172912989561740
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_114 :
Polynomial.coeff recurrence2B4A6 114 = -(1628152787962784808597520191863964245821143599234050 * 10 ^ 70 + 1883442827068387652679944760238308837075600445717992172110672936688663)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_115 :
Polynomial.coeff recurrence2B4A6 115 = 2286124645237824962292926193822128769763450740521096 * 10 ^ 70 + 1290737863323534318943876931785701493293448054328158791329981081175317
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_116 :
Polynomial.coeff recurrence2B4A6 116 = 2938713030256383452097861961693993582164588507756100 * 10 ^ 70 + 6264064713298302647500430428343391385839822165433854360831147898570123
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_117 :
Polynomial.coeff recurrence2B4A6 117 = -(24661809258350110407640602365997854601208123035110356 * 10 ^ 70 + 5488671716698842513779369432361343402527343446865557195292641177432461)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_118 :
Polynomial.coeff recurrence2B4A6 118 = 66137808891070856570939241102379885385255787474084119 * 10 ^ 70 + 1331078411765369141580882332823443916012479762231743690670814754312867
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_119 :
Polynomial.coeff recurrence2B4A6 119 = -(78253973920687122587679791955631066874300210382208583 * 10 ^ 70 + 6161866050575282623357054977902513285757547038305755538489146338171345)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_120 :
Polynomial.coeff recurrence2B4A6 120 = -(116899185588875985526674703988212017820232390778764557 * 10 ^ 70 + 4341500338443759490739938370214968119072242076685145032073472440623533)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_121 :
Polynomial.coeff recurrence2B4A6 121 = 841955462512583362077249673905653553001679923716591338 * 10 ^ 70 + 4740526859466181092899640203803515655371934741722112776318425651837134
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_122 :
Polynomial.coeff recurrence2B4A6 122 = -(2249689796650576332954110756516242429091980206988307756 * 10 ^ 70 + 6967653556960327977660064785061271894833614993916396696653433022937152)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_123 :
Polynomial.coeff recurrence2B4A6 123 = 3272856280808246190816976947937703604934841554956323057 * 10 ^ 70 + 5862945219945461792661848404335571267586144781285710385089600733381095
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_124 :
Polynomial.coeff recurrence2B4A6 124 = 247617301164659908992288030994746537477318538834656114 * 10 ^ 70 + 6820615750080845004517966552928366920087636915339435163210189668850096
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_125 :
Polynomial.coeff recurrence2B4A6 125 = -(16938217750021426737492787501831237387116356384461482995 * 10 ^ 70 + 1283103108429710964252476739734658333160511239423790322515791473552252)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_126 :
Polynomial.coeff recurrence2B4A6 126 = 56687677161632542737863572565711410550741951525974646743 * 10 ^ 70 + 6624360989859245869469486616201446495867218575217264678303268896079362
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_127 :
Polynomial.coeff recurrence2B4A6 127 = -(115896538163683368182430900256094045667024723932690450859 * 10 ^ 70 + 3386278479460963919866011847844028175911135739374241402497224565276687)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_128 :
Polynomial.coeff recurrence2B4A6 128 = 145096836085661228127510526508000167537478937867566824724 * 10 ^ 70 + 8500726033365095712504691058326586148792141786626107064577057798460507
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_129 :
Polynomial.coeff recurrence2B4A6 129 = -(3327407575963962141784554815796641284598954399171350813 * 10 ^ 70 + 1878012981855150046792977904267471768793557812459694094046927418795121)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_130 :
Polynomial.coeff recurrence2B4A6 130 = -(572738612237464139608726372141331893301014184606707212406 * 10 ^ 70 + 2424326725532068131347149588026285914966692294833917370351314882510335)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_131 :
Polynomial.coeff recurrence2B4A6 131 = 1926355789995242331041031493210298764049374098796908851363 * 10 ^ 70 + 2876046356619050399054965727384956060545077703560427051999612114963108
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_132 :
Polynomial.coeff recurrence2B4A6 132 = -(4290698486450707061837586842325248685694971681771475880713 * 10 ^ 70 + 3883004854067759822487939887555807937862884800097914843746871142340622)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_133 :
Polynomial.coeff recurrence2B4A6 133 = 7409342268432273632867778666644326419204353653855750411384 * 10 ^ 70 + 4670092978537278711400287072993435832540446906370017630884135047153656
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_134 :
Polynomial.coeff recurrence2B4A6 134 = -(10029448182175576844759189453905648682604853602538547236581 * 10 ^ 70 + 3166450826051710194375593821258381047525261647120207445468470648948045)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_135 :
Polynomial.coeff recurrence2B4A6 135 = 9488668145653268777547403245145464054886262039140556338586 * 10 ^ 70 + 5127117973568357904543658306802753307115022193624411753373738907145248
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_136 :
Polynomial.coeff recurrence2B4A6 136 = -(1751256684582361390301270317327095921694012915976841197716 * 10 ^ 70 + 2707756241334163894520927103778232000112891116387012658076862000832664)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_137 :
Polynomial.coeff recurrence2B4A6 137 = -(17762977438755128966583041210464321078210240956886453818091 * 10 ^ 70 + 5863568144404664798879720823413660527739733667690802035806303224646173)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_138 :
Polynomial.coeff recurrence2B4A6 138 = 52466297211583512021956729823253949825801768493286385524103 * 10 ^ 70 + 9750695526171895792103681282954579898394809616019985071425147499193934
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_139 :
Polynomial.coeff recurrence2B4A6 139 = -(102385849725043060596874165671446841760423006647201650146099 * 10 ^ 70 + 4779573053278174070169020798111416034204235558238495519466178512748318)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_140 :
Polynomial.coeff recurrence2B4A6 140 = 162311373217987086600844083338047816972745225702149228632809 * 10 ^ 70 + 8001559342729716996815057705047280952930559685509500483737428780729217
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_141 :
Polynomial.coeff recurrence2B4A6 141 = -(221385396803681970442694132009581343262712117888184627931012 * 10 ^ 70 + 7202642497553652647583211839215766186387680220306736593475631799483497)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_142 :
Polynomial.coeff recurrence2B4A6 142 = 264891143332765045421595708991625957367310060087824460499792 * 10 ^ 70 + 9027144181679300936402599735641237506452625095654786380199814732745794
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_143 :
Polynomial.coeff recurrence2B4A6 143 = -(278144444657295157814887423971666465303336857207244437882053 * 10 ^ 70 + 9518807201812387517068825733215532167882435263085010768041029269860370)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_144 :
Polynomial.coeff recurrence2B4A6 144 = 251354075746961811485569417229410511398873056752531421694666 * 10 ^ 70 + 1405840111140732187380137970927955351480209269493249751561306792585590
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_145 :
Polynomial.coeff recurrence2B4A6 145 = -(183616099415499125271866327725354363169356592005167491831557 * 10 ^ 70 + 1740974002875037999068996564164848299245207280431276684084278429896915)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_146 :
Polynomial.coeff recurrence2B4A6 146 = 84297208580639382260173466627945108823920617096857633005832 * 10 ^ 70 + 5350910363761789004305619671718556344797913778788606008604181890461195
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_147 :
Polynomial.coeff recurrence2B4A6 147 = 28994877370663785501474380358496271798771498506065663036826 * 10 ^ 70 + 5435713414812222377754890407135648391743554614005763230390321648179683
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_148 :
Polynomial.coeff recurrence2B4A6 148 = -(135260200148949165665853186647744065382652272322099516090587 * 10 ^ 70 + 734084497299002495596708640759532519242516279198388866413394856917050)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_149 :
Polynomial.coeff recurrence2B4A6 149 = 216004807477974304310426526706881430259461929040300352231050 * 10 ^ 70 + 6314107521278387789556342032491498751303642207499470140814495592339442
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_150 :
Polynomial.coeff recurrence2B4A6 150 = -(260035568648240052822578865024593666543526046226653255065800 * 10 ^ 70 + 8072154874487309737352478133468668039303197427806517097557124750319066)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_151 :
Polynomial.coeff recurrence2B4A6 151 = 265564916752566275636315711306033552060343160497966617200133 * 10 ^ 70 + 7608980127655713166890608928084853134044441304428423350775142348109767
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_152 :
Polynomial.coeff recurrence2B4A6 152 = -(239226374289538883599289178688455186002253477541323489741906 * 10 ^ 70 + 9628352668151073589418245429295934358154692753361195492814579325025525)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_153 :
Polynomial.coeff recurrence2B4A6 153 = 192807974560344901344399669890589668052163052018888698365268 * 10 ^ 70 + 5579239222870089587082064598909364200039555445374209183031306734591181
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_154 :
Polynomial.coeff recurrence2B4A6 154 = -(139200832440863768258754210250756981202473928830790748204487 * 10 ^ 70 + 2758775750087276250985094531181380402546428936939221678600079459390762)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_155 :
Polynomial.coeff recurrence2B4A6 155 = 89027435149548123494983580776040949561121153281819073458799 * 10 ^ 70 + 9561867225029146355386639466966437351559351389264461761598563092998539
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_156 :
Polynomial.coeff recurrence2B4A6 156 = -(48823788338325376421894512612574394941750515618432368559439 * 10 ^ 70 + 2937909117218347970728716364451456007514327078067005497351340638429057)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_157 :
Polynomial.coeff recurrence2B4A6 157 = 20879954461356406143546039659635541507456914957904206974231 * 10 ^ 70 + 8043960693624704584616064576169437115708800039402247755590205567181689
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_158 :
Polynomial.coeff recurrence2B4A6 158 = -(4255539984411748005757113954732477502436230116867693938160 * 10 ^ 70 + 7720214685880256569271958369930518782802228695268212388517604424630339)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_159 :
Polynomial.coeff recurrence2B4A6 159 = -(3740037666814230517958744670247617770574048801688729206966 * 10 ^ 70 + 5139455310314050132715924310819125942623920121038644480652679402362935)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_160 :
Polynomial.coeff recurrence2B4A6 160 = 6207820623704780986750904206664088486765994241615759832256 * 10 ^ 70 + 8485554799979476857275365689649908431558517927845143933146217046001999
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_161 :
Polynomial.coeff recurrence2B4A6 161 = -(5786670345705142171951532029389288196038136299526568440570 * 10 ^ 70 + 9641430502795753951424383520021060972627789016646777557835698628123764)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_162 :
Polynomial.coeff recurrence2B4A6 162 = 4292842837602658560497531543696641141657786491973485247750 * 10 ^ 70 + 6795372306066073164895201473224223315271176443181806099308876095663990
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_163 :
Polynomial.coeff recurrence2B4A6 163 = -(2738387609970292815896437723476113731749784804194003562131 * 10 ^ 70 + 2418085759593434222294834261408066141061288249051629404473748595151855)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_164 :
Polynomial.coeff recurrence2B4A6 164 = 1540559524265072987931990961875684702070250851806561341302 * 10 ^ 70 + 3130455838889850016771173029106326339309964033487370456096904628009880
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_165 :
Polynomial.coeff recurrence2B4A6 165 = -(767720026190140699794025545558522474398809321849657134138 * 10 ^ 70 + 8452895950914467152755695394971350888954336913392741971830015371109888)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_166 :
Polynomial.coeff recurrence2B4A6 166 = 334838603885975198110959054846390029302834260781931817150 * 10 ^ 70 + 2874282595970941285934533786021518078542614073989872700973068318905193
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_167 :
Polynomial.coeff recurrence2B4A6 167 = -(122932229463956391801055569194755858770172229158860210723 * 10 ^ 70 + 3105189035014745196796635115464196906231634994038222217578059764493221)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_168 :
Polynomial.coeff recurrence2B4A6 168 = 33630067516803103889392081504532269600533764454382736990 * 10 ^ 70 + 2194074522049202994175111167514568678423355669814727410460448635608347
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_169 :
Polynomial.coeff recurrence2B4A6 169 = -(2902087210883775847595577315817317751170886456279706655 * 10 ^ 70 + 2279575615857408964859862720747877678858983755757399304187152379584808)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_170 :
Polynomial.coeff recurrence2B4A6 170 = -(4210884402935127287451854223987233315583143233549158517 * 10 ^ 70 + 9946594131612401978441742432500416686201930353990488558178477513804515)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_171 :
Polynomial.coeff recurrence2B4A6 171 = 3875892886302227381020103923544121325743335345285797683 * 10 ^ 70 + 1090427784229989561458405224186259697173073801042204171533706838046818
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_172 :
Polynomial.coeff recurrence2B4A6 172 = -(2246235212903088815096278494205337737222961918763712179 * 10 ^ 70 + 8717381337095174227151065839860645492981488316651445494876646506080618)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_173 :
Polynomial.coeff recurrence2B4A6 173 = 1038477056627288769159761358646455784480585759416106689 * 10 ^ 70 + 3678257369583196447250057744344381358287921598461185204403227934665818
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_174 :
Polynomial.coeff recurrence2B4A6 174 = -(404211156623766720101241094474959126169940895757600881 * 10 ^ 70 + 5822074205260847503694405245867555851603246146874976032575635742556668)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_175 :
Polynomial.coeff recurrence2B4A6 175 = 133201596250581812292239290915284964719661330341779712 * 10 ^ 70 + 6492831659074114102251837828460219306575925947376409143725908204193158
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_176 :
Polynomial.coeff recurrence2B4A6 176 = -(36003545529197795331768076335998456305349002080129846 * 10 ^ 70 + 8995011678050907579779225609604124835337735606900040503885411078051227)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_177 :
Polynomial.coeff recurrence2B4A6 177 = 7084272224417020540693394849512262889899178474801788 * 10 ^ 70 + 2061788882154680207782929237508432318329741076504472953464810359728923
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_178 :
Polynomial.coeff recurrence2B4A6 178 = -(427299017218612613218493918899670573303062773701236 * 10 ^ 70 + 3711360924451444889191929423064281716843746067906163450195795660022047)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_179 :
Polynomial.coeff recurrence2B4A6 179 = -(431174287544332595187564746825933712475903012064248 * 10 ^ 70 + 6593200402107591335972791058344337450157946305892755434463977225206056)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_180 :
Polynomial.coeff recurrence2B4A6 180 = 265401557599305710444160011180470018310722529008862 * 10 ^ 70 + 5577011377208768847084029751807324333700099501550105109254953606123403
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_181 :
Polynomial.coeff recurrence2B4A6 181 = -(99706198399161697508604003201607493314225234835339 * 10 ^ 70 + 665080378033798440823084276461382277487488158598304191303261712095825)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_182 :
Polynomial.coeff recurrence2B4A6 182 = 28622444203060660198459258037090480543210719923275 * 10 ^ 70 + 8816121597595905114205873734832894313497914444956808554425279964235786
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_183 :
Polynomial.coeff recurrence2B4A6 183 = -(6467113770502028500965715480413948883929052425269 * 10 ^ 70 + 3802436474377654362467727362533948933928554742058089489293619463361077)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_184 :
Polynomial.coeff recurrence2B4A6 184 = 1080691813158337491748641964225757395765489450335 * 10 ^ 70 + 5032762419579884089553293824776937509086940301889174533771988599262022
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_185 :
Polynomial.coeff recurrence2B4A6 185 = -(92003625266852612624244317825457898162277066552 * 10 ^ 70 + 7196355568046833361390646996795600629123231320527654989567964750795590)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_186 :
Polynomial.coeff recurrence2B4A6 186 = -(16931611041064095463860079931195314392373191824 * 10 ^ 70 + 7763301130278843406071424780410407006586430031027572297982598507776588)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_187 :
Polynomial.coeff recurrence2B4A6 187 = 10053275997593281270235204114145997176783664905 * 10 ^ 70 + 3578933857242825490347483219855599780156277204494560287384379388926004
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_188 :
Polynomial.coeff recurrence2B4A6 188 = -(2726453162919423712006796300182256992266538169 * 10 ^ 70 + 1064388172119798416320065933298201540844022997493157202055806350468217)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_189 :
Polynomial.coeff recurrence2B4A6 189 = 510450992336669931287061822011032650820603142 * 10 ^ 70 + 8476264938161940676407103548523803465344247843493176812295739782119284
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_190 :
Polynomial.coeff recurrence2B4A6 190 = -(65976039530229589612123890978323434233640897 * 10 ^ 70 + 3009722628749590005208916937799647296399319255530539131847892397730721)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_191 :
Polynomial.coeff recurrence2B4A6 191 = 4084835895762713647185028542674425434405462 * 10 ^ 70 + 478425017852626823925008909052347390866033050797196997661751442114074
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_192 :
Polynomial.coeff recurrence2B4A6 192 = 558646861600331953408277701076803469929465 * 10 ^ 70 + 2449239095064778098288097034220118475535751526742225411729067933086225
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_193 :
Polynomial.coeff recurrence2B4A6 193 = -(218091098568696144382483205051620521175890 * 10 ^ 70 + 1719113096860951056103916043790094280884123030859400891936763960549402)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_194 :
Polynomial.coeff recurrence2B4A6 194 = 36732469329750563972554297050343706813643 * 10 ^ 70 + 5495573089974223180615989300451725108174203344620365719535219647370044
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_195 :
Polynomial.coeff recurrence2B4A6 195 = -(3738256938564991059777260265262822572210 * 10 ^ 70 + 1168667304031869151339843170059769608630399980279719379488169356152508)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_196 :
Polynomial.coeff recurrence2B4A6 196 = 159337179189674278587181002205452310197 * 10 ^ 70 + 9178228012918053200278220256832018176399577604008407718635691046535024
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_197 :
Polynomial.coeff recurrence2B4A6 197 = 19040588325392159163955419118885456019 * 10 ^ 70 + 1159634983248316085863521664853438509341771609086249919114504557984063
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_198 :
Polynomial.coeff recurrence2B4A6 198 = -(4442324225233604435103908309888329470 * 10 ^ 70 + 1697302017729714813579860061382153066295961971759035411664446368182710)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_199 :
Polynomial.coeff recurrence2B4A6 199 = 417568244400505373169370164418529914 * 10 ^ 70 + 7839396074240981421989199282850188810795832779405028869869109996828712
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_200 :
Polynomial.coeff recurrence2B4A6 200 = -(16045873083399463708608136035034207 * 10 ^ 70 + 3317096197762901147376656379591737425930699086067703824631987677186523)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_201 :
Polynomial.coeff recurrence2B4A6 201 = -(899768636556865638765587998017211 * 10 ^ 70 + 9535114661842661135351594776781974576008059839176063547647778528108526)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_202 :
Polynomial.coeff recurrence2B4A6 202 = 158381719240183922906243739189536 * 10 ^ 70 + 2278382021834237034239619052340729806675766666006421880465887323227595
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_203 :
Polynomial.coeff recurrence2B4A6 203 = -(8170128133431341637746849975263 * 10 ^ 70 + 4938628921543539754475807564401070501557153661252186778968318302707184)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_204 :
Polynomial.coeff recurrence2B4A6 204 = 2013320173130418668493844286 * 10 ^ 70 + 7798303097879185250523855652640585851674279729526310744413353020990841
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_205 :
Polynomial.coeff recurrence2B4A6 205 = 20088012667847254219191451930 * 10 ^ 70 + 2043953472740931714209846075482873199643269380138042105257394773216778
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_206 :
Polynomial.coeff recurrence2B4A6 206 = -(796190698150313273273635799 * 10 ^ 70 + 4820510990585963445550610786069904573534183971738730016643961691637554)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_207 :
Polynomial.coeff recurrence2B4A6 207 = -(4132909773687588518644312 * 10 ^ 70 + 2817641671968739826390053631909030025193599756542174909494735784584930)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_208 :
Polynomial.coeff recurrence2B4A6 208 = 878416612234912446638150 * 10 ^ 70 + 4776340106438848442131954198970449943752001377825666074254161099716612
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_209 :
Polynomial.coeff recurrence2B4A6 209 = -(9763908348540467902400 * 10 ^ 70 + 7446531902193598015226326565440832640984369578709640236390979002072111)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_210 :
Polynomial.coeff recurrence2B4A6 210 = -(315359622212257371827 * 10 ^ 70 + 534281624616388531181042320613158891357330190081304186458142137573332)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_211 :
Polynomial.coeff recurrence2B4A6 211 = 4326486560217567664 * 10 ^ 70 + 9290289517376472940693759204032581547284930969500471265712485856777409
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_212 :
Polynomial.coeff recurrence2B4A6 212 = 50742717958089572 * 10 ^ 70 + 404429493081662716054724510769658766485975100382280267575249237003137
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_213 :
Polynomial.coeff recurrence2B4A6 213 = -(498666921118902 * 10 ^ 70 + 7253399929312113001314706264967528933973453651794059787427420336869479)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_214 :
Polynomial.coeff recurrence2B4A6 214 = -(4118809097180 * 10 ^ 70 + 9437183865555306705897987046519738124376938413259654703310955303846152)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_215 :
Polynomial.coeff recurrence2B4A6 215 = 17783411926 * 10 ^ 70 + 2815556000611328189798109759885664944454724997048384528327048554042180
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_216 :
Polynomial.coeff recurrence2B4A6 216 = 138667632 * 10 ^ 70 + 3550345628038888053737410836687532761290250365168091783509037634922402
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_217 :
Polynomial.coeff recurrence2B4A6 217 = -(227824 * 10 ^ 70 + 1406987048251226705454829928429286213976626352852178542989321643719482)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_218 :
Polynomial.coeff recurrence2B4A6 218 = -(1812 * 10 ^ 70 + 8781872071220237726585419056007659446267220642018337415303002352145799)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_219 :
Polynomial.coeff recurrence2B4A6 219 = 1 * 10 ^ 70 + 7970301362802963577579432435703810551799215401776589836049980782449907
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_220 :
Polynomial.coeff recurrence2B4A6 220 = 99991111620497825997282022565416250318154286653733808264363934627809
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_221 :
Polynomial.coeff recurrence2B4A6 221 = -103549026305853853491964020802027163510391556225093978322807143735
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_222 :
Polynomial.coeff recurrence2B4A6 222 = -182735127921126109049827826220209876853659389351823153114958373
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4A6_coeff_223 :
Polynomial.coeff recurrence2B4A6 223 = 221004684282954498531389502610718726903526347183169015695618