Recurrence 2 lookup certificate: Scalar0Left coefficient convolution #
This is a checked coefficient-lookup shard for the second pseudo-division recurrence in the order-seven certificate.
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_234 :
Polynomial.coeff recurrence2Scalar0Left 234 = ((4929 * 10 ^ 70 + 4368763111948477564623652883427472539906252987824530197655159639292167) * 10 ^ 70 + 4723347423850374756525799724198083278380204323390561374079328792415556) * 10 ^ 70 + 462834058432437692870061017674433994485750282708389222249437167571895
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_235 :
Polynomial.coeff recurrence2Scalar0Left 235 = -(((5996 * 10 ^ 70 + 6977061973196494020648598631760716219647648148910832325458377760899128) * 10 ^ 70 + 3321120918098098170785333525028586722865637600667054874053298466307762) * 10 ^ 70 + 1446605391774386324176876098003674756168190973018421466158022504206776)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_236 :
Polynomial.coeff recurrence2Scalar0Left 236 = ((6930 * 10 ^ 70 + 4173725644434093377934984218387992518864583682475455347452554240647595) * 10 ^ 70 + 2913875908556347629190531978811799354851121672774922709218433480660274) * 10 ^ 70 + 9797892035643644368341904718171804639373514315984916341111702913728630
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_237 :
Polynomial.coeff recurrence2Scalar0Left 237 = -(((7619 * 10 ^ 70 + 3156750022859454028617423486426721573657186802557410683278606324095371) * 10 ^ 70 + 5025454469250983337675775842195528943834569898994658123691077754163785) * 10 ^ 70 + 7447546369082922804303657028114412417126034065870118149154359129547633)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_238 :
Polynomial.coeff recurrence2Scalar0Left 238 = ((7968 * 10 ^ 70 + 1880087458833251933434356029990104579277964385354813921781316390738492) * 10 ^ 70 + 7117899063197885782105513261951522763992900222450550748242227358562108) * 10 ^ 70 + 8601214842977552720241830451836479820200358214318623386678929888183408
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_239 :
Polynomial.coeff recurrence2Scalar0Left 239 = -(((7914 * 10 ^ 70 + 4579601491536353690409402823522031065878216343945021978828615497878893) * 10 ^ 70 + 2628611319015013767805694155581592416371323457386518194582916828540507) * 10 ^ 70 + 1679674180242769779594549038556518788625117037592438274515011294646467)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_240 :
Polynomial.coeff recurrence2Scalar0Left 240 = ((7440 * 10 ^ 70 + 1531600140252977098672524225268933895009020988902382617439820787588005) * 10 ^ 70 + 3515258234629813572894824042965365478687499315605340575971802438230340) * 10 ^ 70 + 9926165485786480292809286836978751248520824599297184513659226923539722
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_241 :
Polynomial.coeff recurrence2Scalar0Left 241 = -(((6576 * 10 ^ 70 + 5596743072319112132491041451353012326602805927834141194797709853327611) * 10 ^ 70 + 1588595755590083957037339667442774388004397702234824140724959073222047) * 10 ^ 70 + 7056522979514152532995187857767416501351861492865749998208869540139834)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_242 :
Polynomial.coeff recurrence2Scalar0Left 242 = ((5400 * 10 ^ 70 + 3974574837296978424173052948150174477223275689647975110079880506033330) * 10 ^ 70 + 4469320854423448871944680671115300796585549521839774065418887044419813) * 10 ^ 70 + 6289271501175365561626957049857954772305399635348568786881019395244174
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_243 :
Polynomial.coeff recurrence2Scalar0Left 243 = -(((4022 * 10 ^ 70 + 2649343519677550496215520520209674807662439199579509090647415843502804) * 10 ^ 70 + 3676448424698232334008444029110742958437766135747329418121331561153532) * 10 ^ 70 + 9392581476192792520441575114266330889383843207066988403996445854046548)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_244 :
Polynomial.coeff recurrence2Scalar0Left 244 = ((2569 * 10 ^ 70 + 7987712086342863312884243597302523586715564044056913162084207072657530) * 10 ^ 70 + 666446821642581490865721055327707300953334460661771889130048931473876) * 10 ^ 70 + 1738157900982976726242063969344055721401935199216281957842552573077768
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_245 :
Polynomial.coeff recurrence2Scalar0Left 245 = -(((1169 * 10 ^ 70 + 326239843355881961925454284948122198179318509435574286421753069268158) * 10 ^ 70 + 2178546857498607332730402565177283245745933980412824501988486086345676) * 10 ^ 70 + 6502704478585565570078608176464366073668701370100040259403801854599156)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_246 :
Polynomial.coeff recurrence2Scalar0Left 246 = -(((72 * 10 ^ 70 + 4224285428885341381177490558898948948915691092422610677696234848279942) * 10 ^ 70 + 5735699427828694211258876787636862270030227824870592881396070259864853) * 10 ^ 70 + 3799100277314282122316486693995192474098420055691159253353293945585865)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_247 :
Polynomial.coeff recurrence2Scalar0Left 247 = ((1077 * 10 ^ 70 + 4765492552742860857687453463160184464018618692603795749458808157619809) * 10 ^ 70 + 5168240644855686682478618867366746178292005923929688963987780456600181) * 10 ^ 70 + 646333358105099612415691258591062445145225439481690099544699527374861
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_248 :
Polynomial.coeff recurrence2Scalar0Left 248 = -(((1805 * 10 ^ 70 + 3499657765882533444209160655476484984619606495038735408437333918098099) * 10 ^ 70 + 1541870550590704141966572971945054852283473460740573805631442884734219) * 10 ^ 70 + 3462371448782739772040217203354104521953466454993513976566376486433329)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_249 :
Polynomial.coeff recurrence2Scalar0Left 249 = ((2250 * 10 ^ 70 + 9556144096365727931409585298052971477010557761417048160895646982048251) * 10 ^ 70 + 9536359394334644311292356309843160540934793395759993048667461857649275) * 10 ^ 70 + 5801382343625894976464857131595435720597407453153222143117520183192471
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_250 :
Polynomial.coeff recurrence2Scalar0Left 250 = -(((2439 * 10 ^ 70 + 586590698320063724990476570895130252117377226030756509158230879132800) * 10 ^ 70 + 3445975190824361941313549963371333859505907174757644415181500221606938) * 10 ^ 70 + 4031991205993291450699301696695800747998397000580407276074293246014821)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_251 :
Polynomial.coeff recurrence2Scalar0Left 251 = ((2415 * 10 ^ 70 + 1895545828723112503820878698117912546377937268575505453907309345194924) * 10 ^ 70 + 4767730817532985415409994685740814730579202337365118610426944569789882) * 10 ^ 70 + 7961955199517610591890644198388563979431517183913383519656508831384895
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_252 :
Polynomial.coeff recurrence2Scalar0Left 252 = -(((2235 * 10 ^ 70 + 5013111489292384816588772390118635904146368320348518640739433550270866) * 10 ^ 70 + 9789953501939289623233606063028003798045834390376321087520826502935027) * 10 ^ 70 + 4215698766616678584746432801533911729348071182439464548706738073768752)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_253 :
Polynomial.coeff recurrence2Scalar0Left 253 = ((1957 * 10 ^ 70 + 4707689098844416364159422261593376016458785768213412563751884775941276) * 10 ^ 70 + 9593482993378843817851300500125147240696817476453681342473424158687348) * 10 ^ 70 + 2365659783285374709217176723270097556253112405952518951462547311781950
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_254 :
Polynomial.coeff recurrence2Scalar0Left 254 = -(((1632 * 10 ^ 70 + 7327214547659729423457591824067524031260883359827303188222391664166230) * 10 ^ 70 + 9071846114794916654206449750991604015309029225473224224573547797032973) * 10 ^ 70 + 5742408301915137123935452852921022820664777417164660016984069230513170)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_255 :
Polynomial.coeff recurrence2Scalar0Left 255 = ((1302 * 10 ^ 70 + 6221107580814811306154132480549583024319676368613740566011711547730905) * 10 ^ 70 + 9134798278427189975066262170662036288865586229185404423640386119072197) * 10 ^ 70 + 5398450603464977819318486779041805780737978720291695990095706074817977
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_256 :
Polynomial.coeff recurrence2Scalar0Left 256 = -(((996 * 10 ^ 70 + 3669867699707944727616819915328535224449079556363559559940672402064171) * 10 ^ 70 + 9775831075967996729001137409645283649899574425552645669871886870287338) * 10 ^ 70 + 5576852383982616418436887204300658515569251867764901523615336845520662)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_257 :
Polynomial.coeff recurrence2Scalar0Left 257 = ((731 * 10 ^ 70 + 4353295244741897716150426065741651721667291407203906027439523746583469) * 10 ^ 70 + 6683287814248049488267432422726772712652214635715781791887454507812311) * 10 ^ 70 + 4755673383426421723492393127616913376416375665626012216824018311945685
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_258 :
Polynomial.coeff recurrence2Scalar0Left 258 = -(((515 * 10 ^ 70 + 3255426890082522746422430095021359278030620326600615006230908305911908) * 10 ^ 70 + 3477699281586768221835713244327761407438112820517062645452952287185604) * 10 ^ 70 + 2539714106628701868872742850593379108221687487145535069057068751205586)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_259 :
Polynomial.coeff recurrence2Scalar0Left 259 = ((348 * 10 ^ 70 + 752519827901355206694124503564085902505860683457858318062167640838954) * 10 ^ 70 + 6316083784567726967684845154940206156179891446761431161523024511552143) * 10 ^ 70 + 7547994513205943108339460538679287377022044258995684408277126432586531
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_260 :
Polynomial.coeff recurrence2Scalar0Left 260 = -(((224 * 10 ^ 70 + 8837573986826452103017266734893939258866212154223405038157001740040327) * 10 ^ 70 + 3754465410112505074025786804730685602570452186386530868685649774745438) * 10 ^ 70 + 1412700325148950522695936458284276731309240234703625061526630510299440)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_261 :
Polynomial.coeff recurrence2Scalar0Left 261 = ((138 * 10 ^ 70 + 4303759736970614633736238155255201547998466402798863632075947167486206) * 10 ^ 70 + 5201619083232256814655400518951070602791688340374418918600291205326134) * 10 ^ 70 + 1794502772864902461460660761483189027640251618729161041167841533724129
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_262 :
Polynomial.coeff recurrence2Scalar0Left 262 = -(((80 * 10 ^ 70 + 6653269756217027618234927843998519867558437332525914944011131290241021) * 10 ^ 70 + 2558948665781063435013683354137873789540348044951565507844509133171966) * 10 ^ 70 + 5067284436272958194375787607857755387950432906105174796080859642620341)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_263 :
Polynomial.coeff recurrence2Scalar0Left 263 = ((44 * 10 ^ 70 + 129453667092273991703075417049215824967731122093920842055007109604533) * 10 ^ 70 + 4728753047074687853425813593474284490715635043386337867395985885251515) * 10 ^ 70 + 4549158442908772759340035207019349731003674448047350590542260232825412
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_264 :
Polynomial.coeff recurrence2Scalar0Left 264 = -(((22 * 10 ^ 70 + 405844279578019712444758346682514393924004767701043939545049041994494) * 10 ^ 70 + 9411759246683680136445926963654021064306099513153614138355350518763277) * 10 ^ 70 + 2363499605815203002251112473231333077528820564217531593417796562235942)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_265 :
Polynomial.coeff recurrence2Scalar0Left 265 = ((9 * 10 ^ 70 + 7086748920823271512181310730484557059063090398771160681973136708390356) * 10 ^ 70 + 1890484215169742066894709227438399469717535203415709251461468111259018) * 10 ^ 70 + 3050826318416569664124441198078468134727110009873381486147536092643169
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_266 :
Polynomial.coeff recurrence2Scalar0Left 266 = -(((3 * 10 ^ 70 + 3365331324918413668747007049318807920415926515173409097224893059116025) * 10 ^ 70 + 2309992821621255603739485456207655024364126701035442711178798972222783) * 10 ^ 70 + 9911257388863293070211351816492971012453272264968160404522498876337858)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_267 :
Polynomial.coeff recurrence2Scalar0Left 267 = (4078525747702871299757396308236880890193106180016228060837012699275828 * 10 ^ 70 + 8308720311700111545195410625280085335861911969364750533513719157320915) * 10 ^ 70 + 6122199696920957386276340692273423459451292708398059316597212477630011
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_268 :
Polynomial.coeff recurrence2Scalar0Left 268 = (6870643032497612727564255685181634434775187414176560039324229959997435 * 10 ^ 70 + 3276978819509970026537487608293759599055583270193993939827790387019587) * 10 ^ 70 + 6302482302020979726043941585470874833306608842358645549332157083688125
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_269 :
Polynomial.coeff recurrence2Scalar0Left 269 = -((9071434387300656745117418366606945076005673748077717502580814251968499 * 10 ^ 70 + 9211219022823938017677760884882113494027022666109948030776584762218712) * 10 ^ 70 + 5686459396410622291863816320122816354589656612114953980331948009418181)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_270 :
Polynomial.coeff recurrence2Scalar0Left 270 = (7784360680628956792169924123946087260681175156401155633211097415448784 * 10 ^ 70 + 3142211232881263050693841487907502188069741711691435179274646634163620) * 10 ^ 70 + 552527458833888218460920781826062451690466713832205351493378591397923
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_271 :
Polynomial.coeff recurrence2Scalar0Left 271 = -((5604976650371474375627053655083887878778960326329279277340425939702424 * 10 ^ 70 + 4921346911441263993360895472193436205795875611133828169942311837419492) * 10 ^ 70 + 704670832987992109160405046059837999325447747145480698979851147221871)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_272 :
Polynomial.coeff recurrence2Scalar0Left 272 = (3622553259906066889008402757606564104729791383624257067979578108411103 * 10 ^ 70 + 7286869207113395311852228168551018814874238000165068505813500966781846) * 10 ^ 70 + 3742366856801869467014907400913073869967214850926625454019653876059573
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_273 :
Polynomial.coeff recurrence2Scalar0Left 273 = -((2159688178277758047327046418090966170767547699563185258786652187219467 * 10 ^ 70 + 7242609280681263875819149867181811401017064082858742719866394225403631) * 10 ^ 70 + 1496464607668881441328633355318569394648332165622544036053708665939875)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_274 :
Polynomial.coeff recurrence2Scalar0Left 274 = (1203347489683287888870416616252323052209590409731755133913184785813785 * 10 ^ 70 + 5793903537092278362750742129397280697163206371527452152592610112852436) * 10 ^ 70 + 7393020998630876631200684652282589142872795324074460587440040563862106