Recurrence 2 lookup certificate: Scalar4Left 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.recurrence2Scalar4Left_coeff_186 :
Polynomial.coeff recurrence2Scalar4Left 186 = -((1627949653795240896780413946324346024267677451767303134362 * 10 ^ 70 + 6867899552367409861361753578075949626558465261379816776406216754369130) * 10 ^ 70 + 6067820910532590076265812217548960141867041971584617866442303458041725)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_187 :
Polynomial.coeff recurrence2Scalar4Left 187 = (6292961356627434509191394352328122248879102484847680490162 * 10 ^ 70 + 8391520191215601107930284871779376381258774169938628312729110147540905) * 10 ^ 70 + 472027636526566725001395257951983322977340652577741062169367600163335
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_188 :
Polynomial.coeff recurrence2Scalar4Left 188 = -((12737413072199246568362288327373829875473921017278671811089 * 10 ^ 70 + 5927521499314886615997639867026075091712544228205333657157141673322248) * 10 ^ 70 + 7059594012720475647315619073182514215179154180520039232535240833146700)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_189 :
Polynomial.coeff recurrence2Scalar4Left 189 = (6150400160683154879244788430936716715913437785859932217530 * 10 ^ 70 + 691399162937367579449708498498616827277885417212676500541089739327358) * 10 ^ 70 + 5903813484348313539861493672716680350088335014868905902295815709419721
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_190 :
Polynomial.coeff recurrence2Scalar4Left 190 = (60400456361386790598115046214903924857698536403202056631579 * 10 ^ 70 + 553651759886491720191055186280433870065707069136990571323717055220509) * 10 ^ 70 + 8659670572115036062298701909797814410610794154757505616961879247618732
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_191 :
Polynomial.coeff recurrence2Scalar4Left 191 = -((268887622811659333922900090327245913205802587360255712682504 * 10 ^ 70 + 9565661521707272596751430855293272022242615539569839505578619533268975) * 10 ^ 70 + 3071330581394990306860561340756128592231401139195077418648212799302753)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_192 :
Polynomial.coeff recurrence2Scalar4Left 192 = (638151811013234694063500608344322681909701326619022484961303 * 10 ^ 70 + 8255057276995276115268923028042843677811811373728551661703951714417166) * 10 ^ 70 + 9216368847428038543609112559857063095484662537659267826238903071791273
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_193 :
Polynomial.coeff recurrence2Scalar4Left 193 = -((751684925467382539006493709922707406625265442856593831231938 * 10 ^ 70 + 1449248626434919630507856722267071993431223924653385214761378940496170) * 10 ^ 70 + 4765797389855031567164394778285745497845510638136511432142533191897272)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_194 :
Polynomial.coeff recurrence2Scalar4Left 194 = -((1038115777529604779242251427543453599382025758222428473940534 * 10 ^ 70 + 4973874502574353608276635764923602600733739405578949694165701309513444) * 10 ^ 70 + 4987622099922667144254895874173107293451119032494427157820775842749155)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_195 :
Polynomial.coeff recurrence2Scalar4Left 195 = (8443887623079004840029131435630820013103222378023201779487619 * 10 ^ 70 + 5762294424129767746414014760603926120434541466806260138674330171059617) * 10 ^ 70 + 3565194960570321121179111075986847669478072377156977642155136056997215
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_196 :
Polynomial.coeff recurrence2Scalar4Left 196 = -((25988380427028819830633862667310875719043427288033394575370826 * 10 ^ 70 + 9685245093543784633398840273511263798168370068613950072529510290380622) * 10 ^ 70 + 9722743705326687489717882596249909768470179345845987753727302669158709)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_197 :
Polynomial.coeff recurrence2Scalar4Left 197 = (50120410365496759174737178587938783371739294315307910484474137 * 10 ^ 70 + 7921971865724403739099089585513532599488726151912382994847924235338340) * 10 ^ 70 + 3518615033951596009170940584444621339142067760634271267240539751649265
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_198 :
Polynomial.coeff recurrence2Scalar4Left 198 = -((43684506964067896684957258574145584736576696789049882956427146 * 10 ^ 70 + 3992602409085591699053583129865659082426198172967609589290382216290893) * 10 ^ 70 + 9192671346150517452069829707574556065617841845488617850467774291290929)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_199 :
Polynomial.coeff recurrence2Scalar4Left 199 = -((111409589393948041439415601560068170112749289571538326674130176 * 10 ^ 70 + 1751727744088141837091814301144521595205249383066583046614163604458389) * 10 ^ 70 + 3101945848854921965896139577497599062941269200264997927492137663828496)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_200 :
Polynomial.coeff recurrence2Scalar4Left 200 = (659612386200120735749869537972392868348565572281491942391916621 * 10 ^ 70 + 2402303964772000771662841512866002872443634405977956053405045322123992) * 10 ^ 70 + 476071201437236939459533443723136053015700490773397151762827883190975
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_201 :
Polynomial.coeff recurrence2Scalar4Left 201 = -((1910145307895521764819552292682799261015739705955689194520515688 * 10 ^ 70 + 4845900321952777290776216401094129427331751264846832857008270486375936) * 10 ^ 70 + 1232548623837476025828675394838449299943727702603655056472929422798221)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_202 :
Polynomial.coeff recurrence2Scalar4Left 202 = (3809524652486926977562369306850281123483893852241945576653934166 * 10 ^ 70 + 6985568294667077488090698990272456018744247599075068549786791252206246) * 10 ^ 70 + 6461831076623353251570806171189090343626820791166159536842604181797442
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_203 :
Polynomial.coeff recurrence2Scalar4Left 203 = -((4704016638078736998155297826290059619575724111695539213319682616 * 10 ^ 70 + 5030850184972157636919595164425636706747403945549809751027371978551269) * 10 ^ 70 + 3406222281159951552914397433046762030283808630752765862564592605125874)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_204 :
Polynomial.coeff recurrence2Scalar4Left 204 = -((1167329874637797918873686780140892517276992991755257735570223139 * 10 ^ 70 + 6940291293971809408186940523100455457691297468276256693169298966491223) * 10 ^ 70 + 8976589261309341052616733504021054409553876047794425277180478463483285)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_205 :
Polynomial.coeff recurrence2Scalar4Left 205 = (27263074207577445220628455763624123254573888202809170669035743145 * 10 ^ 70 + 6215010080025674550986732973572858084238263294935238412552052676974740) * 10 ^ 70 + 5399616848254408081187272691571128496715692241693256922782685036416469
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_206 :
Polynomial.coeff recurrence2Scalar4Left 206 = -((97074888138047149311087106525008127876983835372209504184491063783 * 10 ^ 70 + 9713696898894706944523258122515619224535297868795782998708404233749002) * 10 ^ 70 + 5043808304190074119166629115462745596368194311106812148809806888740135)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_207 :
Polynomial.coeff recurrence2Scalar4Left 207 = (238180666293798216379793215204988567408287338816341768757848151835 * 10 ^ 70 + 63433704337396204883098139141416506196423969718056551421413047304249) * 10 ^ 70 + 3235734193251770370010405416996139924516685677514216971525713216204640
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_208 :
Polynomial.coeff recurrence2Scalar4Left 208 = -((453196897081291254153890968261201679044494920137217481805156960206 * 10 ^ 70 + 3212353386255983109538877773078492975735422685744637450381509988485298) * 10 ^ 70 + 4387800845354111602406633283394308264899781537870594905827409238427410)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_209 :
Polynomial.coeff recurrence2Scalar4Left 209 = (643095837466498307689750552176476460581123110459096357719200113093 * 10 ^ 70 + 2193304332561714776388391922210207553718680226473628278484913268056789) * 10 ^ 70 + 302933323861031867346009019531267455298711501920915848069891408237069
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_210 :
Polynomial.coeff recurrence2Scalar4Left 210 = -((451340811990318091730283453625367904017693280950100923862023603392 * 10 ^ 70 + 1826994727577542840847687159828079945750674262362614311815716755237747) * 10 ^ 70 + 6747027732336250991768465244005639284230611578001038394978383627410580)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_211 :
Polynomial.coeff recurrence2Scalar4Left 211 = -((997602887395623159397345571280407311459864676169060815281575402124 * 10 ^ 70 + 7900809597936422712893194307598667525417242497709647672718110275271423) * 10 ^ 70 + 4511369368018090698754471340873901773077514038233277766770170944335934)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_212 :
Polynomial.coeff recurrence2Scalar4Left 212 = (5460983507174505190151637732476064444772760346033114156869829219984 * 10 ^ 70 + 3591234974384925592510221336171742877564123967716574466934839206659873) * 10 ^ 70 + 6555370815672050933669157487836839544991545088935880175155635109857539
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_213 :
Polynomial.coeff recurrence2Scalar4Left 213 = -((15967202558881762006757163384480717609785698115482298821985246771854 * 10 ^ 70 + 3815636617971187155461953292269115105157183432344364389201352972092085) * 10 ^ 70 + 5858779982167323070147931936744020139692736308939803762383760739213394)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_214 :
Polynomial.coeff recurrence2Scalar4Left 214 = (37043709159462220990011842767114419211251786307369564913722737650769 * 10 ^ 70 + 7758927784285450501775927941127909254851203163083382063951868192886761) * 10 ^ 70 + 4166760793071846252312373793296739367370985942922608993075018436445285
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_215 :
Polynomial.coeff recurrence2Scalar4Left 215 = -((74454770881176143976920082833656379190871956677181597753049721220264 * 10 ^ 70 + 8180096362198972782195216800102509854101112681107440102687887926371321) * 10 ^ 70 + 1490256461290775641869658259448866161660942369102476653287109561506316)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_216 :
Polynomial.coeff recurrence2Scalar4Left 216 = (134003060405536959135041502986243314434557516211893740461040589395667 * 10 ^ 70 + 7866945185112468189635281138803216935926518616521702836311734134633934) * 10 ^ 70 + 8063756043304869939076072967285043933565614321949619597886958809715249
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_217 :
Polynomial.coeff recurrence2Scalar4Left 217 = -((218936614815821699987241046515332615570958883828919973888737212564108 * 10 ^ 70 + 6727847785060523425128642831179537547154466856868854259301632743576645) * 10 ^ 70 + 7549253433671536305832697628148821156588274940677886785438099429233441)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_218 :
Polynomial.coeff recurrence2Scalar4Left 218 = (325692413521851710894100240192710303890355938398332160505435814071260 * 10 ^ 70 + 8546685252372202791339290378361664335734916394597231618242475999713279) * 10 ^ 70 + 5413116657022418162005455968990480612827375444165059103317042511766706
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_219 :
Polynomial.coeff recurrence2Scalar4Left 219 = -((438170456375454917485448699281360494608807468392503279132383101937280 * 10 ^ 70 + 6510481184815264902995955835612954218553403231444518610429974663767059) * 10 ^ 70 + 9097003297655567478817490867590257177520044757232723464387232829755821)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_220 :
Polynomial.coeff recurrence2Scalar4Left 220 = (521456696753516695916316001438152283784366721488765527445369265076622 * 10 ^ 70 + 3104483169934605770707035036281393491999837590966495642461288188125727) * 10 ^ 70 + 9924072035367436600122987548330879364060117739665513647467123547863560
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_221 :
Polynomial.coeff recurrence2Scalar4Left 221 = -((516756994163840112989163722876100210896925505458855604462059042323261 * 10 ^ 70 + 911595919175642724501451042181172485947202102145137315318558570738727) * 10 ^ 70 + 9019855232116965595980798996939723889698773939575952480104034956417081)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_222 :
Polynomial.coeff recurrence2Scalar4Left 222 = (339981883412546331721515556785593324168305048781341135414924776908170 * 10 ^ 70 + 9256187609209932256357098314468929606713301910714231266768143705124883) * 10 ^ 70 + 3783541080672104281324822729475593873237055996740425608572961035241525
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_223 :
Polynomial.coeff recurrence2Scalar4Left 223 = (113440904869323901937885627177393995452428635229239082208175126464062 * 10 ^ 70 + 328761999895422438878712696311228423582183708872829843738812020910196) * 10 ^ 70 + 7854255987385433753571964052100231824465416086870777281324116376921751
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_224 :
Polynomial.coeff recurrence2Scalar4Left 224 = -((955689033537035643495952829496818140248169529440544132427459569967921 * 10 ^ 70 + 2232297509110277705097561910962287091321138829434741157535952987102522) * 10 ^ 70 + 9945783684767560525685170664124794357865996553985283605877314046667966)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_225 :
Polynomial.coeff recurrence2Scalar4Left 225 = (2285511510727141944925958653422759309929110460161509861454221922149434 * 10 ^ 70 + 2973013941837576807105492794024864945113268164024618501618106394640263) * 10 ^ 70 + 7990945886818060778149237804014520687992881712719622337925169329406851
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_226 :
Polynomial.coeff recurrence2Scalar4Left 226 = -((4161470413785962910862444100619517673731881193380224085430887985060997 * 10 ^ 70 + 7900039896641714685761745587999396863816848853006924797804817905361794) * 10 ^ 70 + 2785515688300530017268623948392686902589127050962885912704891230782340)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_227 :
Polynomial.coeff recurrence2Scalar4Left 227 = (6574567033371985923845909658358650569444596878429785874021824003933861 * 10 ^ 70 + 4032053844094867653991891770797135897734168085493404532354587979874062) * 10 ^ 70 + 3562004449594393104481778942489252378480790094086372184986696937154702
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_228 :
Polynomial.coeff recurrence2Scalar4Left 228 = -((9427281533582818841310743815196606075441756441672285137795044080997707 * 10 ^ 70 + 6340906766835153635050689047310905850483226132948691382860618069632054) * 10 ^ 70 + 4765342652578071566495332352068620831113820958262542852856273951240780)