Recurrence 2 lookup certificate: Scalar1Left 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.recurrence2Scalar1Left_coeff_189 : Polynomial.coeff recurrence2Scalar1Left 189 = -((1418632472046961307487660882481714260269294723768235110779602 * 10 ^ 70 + 8298813904390552930421395889054777283323039498057853296611434448750876) * 10 ^ 70 + 638561011306453788973715159818071118845254755820280663708244298182435)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_190 : Polynomial.coeff recurrence2Scalar1Left 190 = (4195790753690015988687364388536215038247846232495432447779620 * 10 ^ 70 + 6601547731937809872440510218186548082999359505386900973714631184452889) * 10 ^ 70 + 5083695993010967841074742833568222760369065389635753662116299470204355

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_191 : Polynomial.coeff recurrence2Scalar1Left 191 = -((6312249890870967870887258118088302066419141505757968981645060 * 10 ^ 70 + 869169900128097926162056576187741638131839910992045783796897500655835) * 10 ^ 70 + 1592222228938206699159650242159660828561837676147852050889012071588761)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_192 : Polynomial.coeff recurrence2Scalar1Left 192 = -((4478495803124155339311480606822346312334794082107008376472234 * 10 ^ 70 + 6073338930364359880915372399099713798886045311181202745826613606345371) * 10 ^ 70 + 1455436193443761933140091223824931320740673596622917101314038317690306)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_193 : Polynomial.coeff recurrence2Scalar1Left 193 = (60271633325200724010497421813002223604010515785956904046173145 * 10 ^ 70 + 4991824449363191832499560416360762662964163328234344217128682295680172) * 10 ^ 70 + 7215510816713828884218648132512245938142134334972477240406280684300890

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_194 : Polynomial.coeff recurrence2Scalar1Left 194 = -((204487012982112028369984310382552011469739010139818207268664250 * 10 ^ 70 + 594835063492274441345715625079610144459582718583387081138568276553058) * 10 ^ 70 + 4299306211144855398082999718341786989015496391968402028756821139962727)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_195 : Polynomial.coeff recurrence2Scalar1Left 195 = (400535573241269882865658612574475092008285840703828147624804246 * 10 ^ 70 + 2664251970952163200115187966618891752351389640027187331405489799177166) * 10 ^ 70 + 591001115121611362450174604385464429999764099106775280045478130529554

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_196 : Polynomial.coeff recurrence2Scalar1Left 196 = -((242890467206966803639873851037670469355043494220341692058590367 * 10 ^ 70 + 4860270862390699867121036282376444707212400890209980799687521293537125) * 10 ^ 70 + 4983049910634564941361199667327396765816981157083941017088729407648506)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_197 : Polynomial.coeff recurrence2Scalar1Left 197 = -((1584245267412596992569707830790470905197301628662377038472699015 * 10 ^ 70 + 2061801045625450484495722043432531113780114810854034224289878002767227) * 10 ^ 70 + 2063380568148981245578474562778264178118841298459279023583588954128652)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_198 : Polynomial.coeff recurrence2Scalar1Left 198 = (7668896101032207279888264576498180544959924568085971516153776349 * 10 ^ 70 + 5631176722034342903493844868960445750785980329821433155497140834677660) * 10 ^ 70 + 3291083398835210032728132663264203971242767676887644276684406244362478

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_199 : Polynomial.coeff recurrence2Scalar1Left 199 = -((20195402903915083250113835691525053757556023761730877352193592847 * 10 ^ 70 + 5341086843022906550603802238079312771332681383393695445408528281980378) * 10 ^ 70 + 9092097237944999680644401703019052909224304280813353702815888558621400)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_200 : Polynomial.coeff recurrence2Scalar1Left 200 = (32772781479400615601793681366693365403302996260602555478826497214 * 10 ^ 70 + 3682398299589600083788365233206586165850841423589568083981885854474541) * 10 ^ 70 + 7152073090876253032830661562115879594345775694426965631076216845198976

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_201 : Polynomial.coeff recurrence2Scalar1Left 201 = -((9180035765992096886839451098997099316101019316871957795937487839 * 10 ^ 70 + 1058511517876485254687221776346364156493801827491541391245195400427966) * 10 ^ 70 + 5912509716715304875414025785611217562112139918030754684226405406210008)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_202 : Polynomial.coeff recurrence2Scalar1Left 202 = -((152492569169894375404759722781716731857286960543885075748203766139 * 10 ^ 70 + 9635423140308679911482572926487242304872153318570285991269213088121046) * 10 ^ 70 + 8168073728409073382869799568166756437734238114767011291415123186475107)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_203 : Polynomial.coeff recurrence2Scalar1Left 203 = (643915599584658827449926993394375109112008756483835125346614336818 * 10 ^ 70 + 766139691773069041218347129138887407680594664277580127907230864913642) * 10 ^ 70 + 6882811692879446749080739084106930470489576078203531712080376659777156

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_204 : Polynomial.coeff recurrence2Scalar1Left 204 = -((1657608042650168596269322088420787166830088553922827348124379507329 * 10 ^ 70 + 7522825819378164456977354224475686998493854694812519964855408800507465) * 10 ^ 70 + 9037860016286470500773329592241942796926969751888258035876180298128253)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_205 : Polynomial.coeff recurrence2Scalar1Left 205 = (2946416892133043923891611387351114486703655517313808721939010204375 * 10 ^ 70 + 1698395254338344633267407343194291354114324972219447140972170711342656) * 10 ^ 70 + 6175821073787977852994248821825599420957137379014284456783850484583897

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_206 : Polynomial.coeff recurrence2Scalar1Left 206 = -((2636769464127089858089485388528990011003327294222941814177744304196 * 10 ^ 70 + 9872077889934416707465677805760572367336435537213301843216715883911394) * 10 ^ 70 + 3476659787747434067376667846451107810056273185567424523287962599558506)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_207 : Polynomial.coeff recurrence2Scalar1Left 207 = -((5067678409909005316375713207307273182471925255754075656109026990278 * 10 ^ 70 + 1410350935283069476440280446369314921440411982708007861425353070725433) * 10 ^ 70 + 4203044993681094399314543289138011815247225951232160107674155161129728)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_208 : Polynomial.coeff recurrence2Scalar1Left 208 = (32928826232472594555536874165746959490736235220482102489351027080345 * 10 ^ 70 + 500502410823182743003925262394187529637537960368172436925730473620794) * 10 ^ 70 + 3047676334124881935273800273189016321754682205641395012826317515431908

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_209 : Polynomial.coeff recurrence2Scalar1Left 209 = -((101769769322447193805052553232616363729304322286686511515990794419974 * 10 ^ 70 + 9674922241196182822579221997436629605555360980651065249656790374967167) * 10 ^ 70 + 5378655831151704729181774209235989649812824481232373392720678736653856)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_210 : Polynomial.coeff recurrence2Scalar1Left 210 = (231818398020090713965998203760960614269000198119352200536182739044266 * 10 ^ 70 + 4335305347933622690120894852875326316643873724821496551071374927183708) * 10 ^ 70 + 3273047377771217629250071813447454939141531827432501749547468420235776

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_211 : Polynomial.coeff recurrence2Scalar1Left 211 = -((407803996490467773244788515014861530159746934891592531161217118916456 * 10 ^ 70 + 3796530470508827866441189980929939168611675173517309977093133664225006) * 10 ^ 70 + 364223379519526016426758939684284181635768382166517554013022023837659)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_212 : Polynomial.coeff recurrence2Scalar1Left 212 = (490049723781047492218914319392997320698618802722711532436783412845231 * 10 ^ 70 + 8414524777243729805968619502026812321419460816538802401111378020615680) * 10 ^ 70 + 843184376740225643573352824643472408453129537814506922745505784705338

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_213 : Polynomial.coeff recurrence2Scalar1Left 213 = -((34942180964155502586668616554716540007171417050495919888294061916858 * 10 ^ 70 + 2393763482160529523895728041453961192954969505207599170977097015330206) * 10 ^ 70 + 8321653259396257703821236373781042016977937044166007072703064881127726)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_214 : Polynomial.coeff recurrence2Scalar1Left 214 = -((2007199778061594218758252305549678148505846677237723619552042047332621 * 10 ^ 70 + 4490434256101289621228135716367428499052956624212205730864005807248177) * 10 ^ 70 + 9077663632519759984619981229957423671109615564710094768236966497630981)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_215 : Polynomial.coeff recurrence2Scalar1Left 215 = (7713012661192368575864509658122425817853462002925470405088689938612861 * 10 ^ 70 + 292163095738648245103664729813527503754535234019188142339365533968746) * 10 ^ 70 + 7386732780029244395313349576370525405185774090948262883013481725988984

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_216 : Polynomial.coeff recurrence2Scalar1Left 216 = -(((2 * 10 ^ 70 + 634422359596865083342623215968321821708139177809924757375243471171058) * 10 ^ 70 + 5819119773713971584181518315968626336629944076547742797702719751970177) * 10 ^ 70 + 9476076303103932532315075840392702565153285653259425152800176923204735)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_217 : Polynomial.coeff recurrence2Scalar1Left 217 = ((4 * 10 ^ 70 + 6031072769913614955620647233022665997368577842755780389890777362891218) * 10 ^ 70 + 2749279347146398608625531367522680646199365187917748729263338651132522) * 10 ^ 70 + 9456943827373087333953920605119559149359973997788701854975068698127677

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_218 : Polynomial.coeff recurrence2Scalar1Left 218 = -(((9 * 10 ^ 70 + 438357080996561024147745113762521095897119120746228460262384959477441) * 10 ^ 70 + 8692820044988735646295625812501667263537630364211726388384590298899737) * 10 ^ 70 + 1169858267394510468860756315738940372996717142510734996388827311467095)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_219 : Polynomial.coeff recurrence2Scalar1Left 219 = ((15 * 10 ^ 70 + 9919140532597677445708467320761129119444764695142150225637140681327113) * 10 ^ 70 + 2604390117276683672773557078471439396204912674479075212452833755579470) * 10 ^ 70 + 5571874965507556679259843336833586218539171750312510342740363130904115

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_220 : Polynomial.coeff recurrence2Scalar1Left 220 = -(((25 * 10 ^ 70 + 6254431353736171326358122748444053793190475895094205628388708605759386) * 10 ^ 70 + 8681636328428740271421813150219137904142799144874949914724911413857095) * 10 ^ 70 + 7347848841090862970059916758275465727080069447750644897639351633509450)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_221 : Polynomial.coeff recurrence2Scalar1Left 221 = ((37 * 10 ^ 70 + 497226217932027742499476702886624624997561900244444739052547887251499) * 10 ^ 70 + 6783016421262662355824999298377546395278938363439650599600827019335394) * 10 ^ 70 + 1839773222765009415481465779033298948816156822724503372163356833365207

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_222 : Polynomial.coeff recurrence2Scalar1Left 222 = -(((47 * 10 ^ 70 + 3892062145135940479177476331149615842105226690562336540744705627941918) * 10 ^ 70 + 781274291120193253779318027936702976080580402289010705832031999897107) * 10 ^ 70 + 1009737161557965755360218760611787202719734187970713094456098843496086)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_223 : Polynomial.coeff recurrence2Scalar1Left 223 = ((50 * 10 ^ 70 + 7213803151175817387599775857499503082133200260067707080322289463166186) * 10 ^ 70 + 2304585563548943950303089067908938248908884443563186917574976331129902) * 10 ^ 70 + 3959232743177568419201218504499732503495714822083090699627044053109791

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_224 : Polynomial.coeff recurrence2Scalar1Left 224 = -(((37 * 10 ^ 70 + 987578689526767046748395219522154625342842547907438019392975488650984) * 10 ^ 70 + 5196350165426807365528284029144148225105069775258110983135404752091909) * 10 ^ 70 + 16159293326951426367193272021222482292282595411390723482576517201274)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_225 : Polynomial.coeff recurrence2Scalar1Left 225 = -(((7 * 10 ^ 70 + 9541975432019897261611754979053423766443697028814013519878208323417705) * 10 ^ 70 + 2902107159094221144844435623555269789630045703449163462054712012188300) * 10 ^ 70 + 1857009651830510502650833808850198869476496941626053025349106910195883)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_226 : Polynomial.coeff recurrence2Scalar1Left 226 = ((103 * 10 ^ 70 + 6490922768201796991717260381268273461190509926778877686125283642417) * 10 ^ 70 + 9097386663711946129962375627137571904961280668557354938360334078864) * 10 ^ 70 + 5191517128394252036337980523074441593653095256732929606399972902556670

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_227 : Polynomial.coeff recurrence2Scalar1Left 227 = -(((268 * 10 ^ 70 + 8833446266451442225150604014441332730303099076124611751795913485740403) * 10 ^ 70 + 1941211661446064847034202940446224413250699727343775232045654451324161) * 10 ^ 70 + 6269446463430461993858297385458434111619993665654508956063957934584355)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_228 : Polynomial.coeff recurrence2Scalar1Left 228 = ((525 * 10 ^ 70 + 3456096397521538766220467153505221860004621284572629185371776072964225) * 10 ^ 70 + 7817061092778613930341674283559476564632596832552669754855196845697449) * 10 ^ 70 + 8417105471431044110029948467215425631293089871480356690200627217757454

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_229 : Polynomial.coeff recurrence2Scalar1Left 229 = -(((886 * 10 ^ 70 + 2773016778906308248566804039041850615732895932073081969337702724780526) * 10 ^ 70 + 1622144627261881045211066213020891431272626316606491313780329327897456) * 10 ^ 70 + 184802692726810397513276796412791179782789035717439923417416167482631)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_230 : Polynomial.coeff recurrence2Scalar1Left 230 = ((1354 * 10 ^ 70 + 2908201667597651693918355201722715657175541392798920768884528498176686) * 10 ^ 70 + 5430390254856958869184968238744717064152317760549193760762094814950616) * 10 ^ 70 + 189838581792615597386739858204819299029460062974311622683477707298163

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_231 : Polynomial.coeff recurrence2Scalar1Left 231 = -(((1915 * 10 ^ 70 + 8114698411270642247998473036237990039137030003723102680201210375945360) * 10 ^ 70 + 9354727462636701435190582310718334431075337824814301463855172778509463) * 10 ^ 70 + 5308345921314674871344472446989679804348374369645770229048540456861899)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_232 : Polynomial.coeff recurrence2Scalar1Left 232 = ((2538 * 10 ^ 70 + 1354143998385301813168434240066161773636614404613100578696817133737011) * 10 ^ 70 + 7502822215234057618882720694149314097320682032610198013375005545235533) * 10 ^ 70 + 7329500889394409591162514117597573152688509765376142169284416297628242