Recurrence 4 lookup certificate: Scalar0Left coefficient convolution

This is a checked coefficient-lookup shard for the fourth pseudo-division recurrence in the order-seven certificate.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_163 : Polynomial.coeff recurrence4Scalar0Left 163 = -((((12656 * 10 ^ 70 + 777806645448703861349552744758787599798449343863859163825089022705141) * 10 ^ 70 + 6800408043601036814749578376781860628424102988931483383441501052318039) * 10 ^ 70 + 4673968790819223432144008075316399718003201258591368054806635922384973) * 10 ^ 70 + 9192527060055279323636656664423267262153065910530674584110377292154018)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_164 : Polynomial.coeff recurrence4Scalar0Left 164 = (((45055 * 10 ^ 70 + 5023886982134648444622798295702295787443459386135358166122739615371057) * 10 ^ 70 + 3404002836315062057249575288089452528515954160813142359098008237884186) * 10 ^ 70 + 730545957859554254714259612683933193662026557287213211337782431687809) * 10 ^ 70 + 6709208771150360425202648264439162514899423068234051317016518455921952

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_165 : Polynomial.coeff recurrence4Scalar0Left 165 = -((((157905 * 10 ^ 70 + 4978525256935031620415861891903657111043589765387914170051756083212428) * 10 ^ 70 + 4276879427139099367103721944044177090317291579760895049148957458256510) * 10 ^ 70 + 6647524794784505196483838781159740721546880951887164376076132475115076) * 10 ^ 70 + 4648799222303829796137530683315983218998153160851294317899942189627999)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_166 : Polynomial.coeff recurrence4Scalar0Left 166 = (((544852 * 10 ^ 70 + 5782991011257407187455527779072846643492056296178528524539488959280714) * 10 ^ 70 + 6180786861197125752200367606983094516633195489300065076426644121932949) * 10 ^ 70 + 9459917982966928229294089256508929263031864679114417955446105372798798) * 10 ^ 70 + 8965020031523185574488079961445725008758000939785112044499362999107215

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_167 : Polynomial.coeff recurrence4Scalar0Left 167 = -((((1851074 * 10 ^ 70 + 2069920784770314113862513072513572817959928906532488814963135084587679) * 10 ^ 70 + 5569553334769236210000871299005189766792315877519647826338752185457574) * 10 ^ 70 + 4508114363030141374710664252328114341084119377187425594072449414442452) * 10 ^ 70 + 1259068336794265643970318441408887546974472852752678882309156153717030)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_168 : Polynomial.coeff recurrence4Scalar0Left 168 = (((6192436 * 10 ^ 70 + 178880103313770417086381523525989607981398130789866206334054096028841) * 10 ^ 70 + 9202484331608533800109197921396670710464937256946838549607096977360444) * 10 ^ 70 + 9734233028664144842642576748718697564207925213911754647279737482632805) * 10 ^ 70 + 2781627860065270100810765033154050936847006831807541633512468363094184

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_169 : Polynomial.coeff recurrence4Scalar0Left 169 = -((((20399571 * 10 ^ 70 + 7279818231960837132542741814576231197526117521506443182830804590574769) * 10 ^ 70 + 4770585052736303092394283595507856079753738995542055966838571676635540) * 10 ^ 70 + 7418981437117806900805621673305514220022312654472225174986190893696769) * 10 ^ 70 + 7638999820202057162265670972827629243959145300747297551382986180514170)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_170 : Polynomial.coeff recurrence4Scalar0Left 170 = (((66180566 * 10 ^ 70 + 5860315762723590948730976475652732823900807202484046588848708668683904) * 10 ^ 70 + 4696310733971679673408672512044288720371926472744805776166732233412408) * 10 ^ 70 + 3480685257098345550649271974035712111636795748059899960036715203436953) * 10 ^ 70 + 1772684747742535136961357496744389490753528230209526726546481516214113

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_171 : Polynomial.coeff recurrence4Scalar0Left 171 = -((((211454566 * 10 ^ 70 + 1079103980463304971962081157398149527361183528229754308049030623545575) * 10 ^ 70 + 6368908390997761231038568103519425778682668028529981611875674557159994) * 10 ^ 70 + 6904580044656762888624982144496234778375241594791452449645439592141124) * 10 ^ 70 + 6445625017508530524512973376755234307429416543537188270418694373120430)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_172 : Polynomial.coeff recurrence4Scalar0Left 172 = (((665437443 * 10 ^ 70 + 233694934183728039345308200276541796939196658640850815417290900632892) * 10 ^ 70 + 3965193350600184936513452441881057717263508189559055150834833169759295) * 10 ^ 70 + 5384396797941975002244929918360736740545981830955024391498664909137008) * 10 ^ 70 + 7910045852720843795576284428604939679777381477207696698687140188431971

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_173 : Polynomial.coeff recurrence4Scalar0Left 173 = -((((2062655024 * 10 ^ 70 + 8531462457559524802315211694796544202047659788682342325853505662880579) * 10 ^ 70 + 6811935832971263667684987510508357119614286971088203975952477279414731) * 10 ^ 70 + 6691206413909836915701536794278182523941708628440532606236079664922543) * 10 ^ 70 + 2057402757144292337644615083626274097800439130634789614303392160112600)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_174 : Polynomial.coeff recurrence4Scalar0Left 174 = (((6297961348 * 10 ^ 70 + 2981242774409599385507480641222334844842831083269440294660181184873685) * 10 ^ 70 + 3686017165729718634649870633425803906689600244159269761070703190918504) * 10 ^ 70 + 3756498330028419685140520765676833315034004064969963936840494384241279) * 10 ^ 70 + 865030140515012822972947313850270903717884301459743844733286412472040

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_175 : Polynomial.coeff recurrence4Scalar0Left 175 = -((((18943117965 * 10 ^ 70 + 6328817176869866504803137270900077514968828134224359666452292284201143) * 10 ^ 70 + 5874598221623581649294065638616115889148952198722657702094871877437514) * 10 ^ 70 + 3060505419954813083214216505120607531689163508655638009201308533789489) * 10 ^ 70 + 1350952541914709228577845803058360330849796926056670142418343285509051)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_176 : Polynomial.coeff recurrence4Scalar0Left 176 = (((56131198005 * 10 ^ 70 + 4603014987189838053623290575347190282171986377320725777796427158085311) * 10 ^ 70 + 739305401033732437322863647055581483335980072179707643302111951634203) * 10 ^ 70 + 1767576304362305162878661758067479002426670398944473556863630951006891) * 10 ^ 70 + 7158554321779521747666630067560228485519480391566660364944287685104894

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_177 : Polynomial.coeff recurrence4Scalar0Left 177 = -((((163863067878 * 10 ^ 70 + 4882175770180708262598271374056230470169952398702448885819882928525917) * 10 ^ 70 + 342887422045194384796889119777972483355942296396446909386533018096391) * 10 ^ 70 + 2473834082448541781512979181554893907704821915938598199844950406580139) * 10 ^ 70 + 8622053289179454423969503612502716916727597412885480658133022470563103)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_178 : Polynomial.coeff recurrence4Scalar0Left 178 = (((471306672772 * 10 ^ 70 + 9892942295281089802624855281995718000751813958150281470103538897340740) * 10 ^ 70 + 2568820239586346400230654463057997773051076419640011948802982012351740) * 10 ^ 70 + 6846591926650979824927147921085952428204665998767651229448679812342398) * 10 ^ 70 + 7207660651847893391961388209452342868088910924672495428162407992177196

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_179 : Polynomial.coeff recurrence4Scalar0Left 179 = -((((1335650792743 * 10 ^ 70 + 1836033655199476243829088399919647673503113793553264236832058299425249) * 10 ^ 70 + 8152008677127662449013478957918841856105445703410866895045283611850675) * 10 ^ 70 + 9739909736862991541418566722713123218722072837045339117715226653935852) * 10 ^ 70 + 8179774508419807290323392965865710124174596607722375437949483056266494)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_180 : Polynomial.coeff recurrence4Scalar0Left 180 = (((3729662032582 * 10 ^ 70 + 4867518539859930419101306715673405858105071316745211600169332275042427) * 10 ^ 70 + 4535414395792162132621732533379649325696666449740273452782923114751180) * 10 ^ 70 + 5436496918806813004473081246800153532499763283450955240702631460051056) * 10 ^ 70 + 6970615854764561901188470633557266367415747795047882797031477531399744

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_181 : Polynomial.coeff recurrence4Scalar0Left 181 = -((((10262494455177 * 10 ^ 70 + 7305296701270846246601523265047265287957331450904107689528502254467774) * 10 ^ 70 + 8074133278440317638163367885082028282602021758427742767876527400691864) * 10 ^ 70 + 7919724416812063901247095982350639668106760147570174002508653508384707) * 10 ^ 70 + 4879056338790925999557911104312675969587540174026876357871022066452819)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_182 : Polynomial.coeff recurrence4Scalar0Left 182 = (((27826737668887 * 10 ^ 70 + 9557956187621655786428391048822358372398725186056894260591286192372741) * 10 ^ 70 + 804215135487541320843489534375617298584144737374769483465974245517814) * 10 ^ 70 + 2227126686073790290115201461659318460617508999083990831989294763888123) * 10 ^ 70 + 4632744154405616145225236515671264085191369417114167394956758896573967

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_183 : Polynomial.coeff recurrence4Scalar0Left 183 = -((((74355975644912 * 10 ^ 70 + 8478327469430422522941859003090302226475955299528642510975308591183523) * 10 ^ 70 + 2430576912962238343009441640185392867377615117108975851478795016955621) * 10 ^ 70 + 4482347386848532580410840821495791347588920961194123956867793473957262) * 10 ^ 70 + 9327339193444628295450753899577744020000513174047731953612741370334478)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_184 : Polynomial.coeff recurrence4Scalar0Left 184 = (((195808408126996 * 10 ^ 70 + 8658266067254605652378450131078306476537367295250789669857596451665158) * 10 ^ 70 + 4251104981339227665872984631047693687525174831763431822656019348773393) * 10 ^ 70 + 3830786949024437601006168602394994300669514263409950533967097646942656) * 10 ^ 70 + 899008347854349617900767673778805121130352691345139608951891276652907

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_185 : Polynomial.coeff recurrence4Scalar0Left 185 = -((((508189476112890 * 10 ^ 70 + 3052448872818012376507223084028064130052337898533663849336972259978258) * 10 ^ 70 + 9919643733916472554110710662190245861973115964956904477059817824019767) * 10 ^ 70 + 6815557802337764707351928749885269506973864866691331228404556293166606) * 10 ^ 70 + 8243987062421607255352065999601507063648055886654406231722771226133606)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_186 : Polynomial.coeff recurrence4Scalar0Left 186 = (((1299915755132334 * 10 ^ 70 + 5492245477743175253739341496276495266089785972154407699783377069555727) * 10 ^ 70 + 5475507524468959099341285471608896626210086312137513614230917377878257) * 10 ^ 70 + 3139556732715745032871634668646347004630697845273919794811125421382409) * 10 ^ 70 + 2850299429028716459939128831328862651356884391969354638100444500918668

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_187 : Polynomial.coeff recurrence4Scalar0Left 187 = -((((3277295871809373 * 10 ^ 70 + 9515116964041466851632241106098963837068546697235906666907802353256298) * 10 ^ 70 + 1370856024171806730469212518224220658520423011562963275955817977582978) * 10 ^ 70 + 5707480868001546087768825394640796215931489806794787745052031258307105) * 10 ^ 70 + 9055545773659039332704788268255926120768388187381707121401840964541434)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_188 : Polynomial.coeff recurrence4Scalar0Left 188 = (((8144080361628203 * 10 ^ 70 + 4596963896828314553195265914726085012870706248409414513805628632518012) * 10 ^ 70 + 5823498951000382488715952167152335831539008661789618522933945048178245) * 10 ^ 70 + 5264302814080027396111683448088863065751448059599393153014966325094646) * 10 ^ 70 + 4932990333461206884306744530273822326246279211455130762962027207948545

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_189 : Polynomial.coeff recurrence4Scalar0Left 189 = -((((19948434704419600 * 10 ^ 70 + 2023802610467813690538269055402674283544198682810320011437275961786720) * 10 ^ 70 + 5330465796598726121915614945830659387775816400872000007339096937896724) * 10 ^ 70 + 6325122159964929678860300999776974247384208080230760850753058401362150) * 10 ^ 70 + 5280105683416462547634523652353674905805587504601896591833980270341676)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_190 : Polynomial.coeff recurrence4Scalar0Left 190 = (((48164799521073356 * 10 ^ 70 + 2636988131917120153895704564052050579748146414080773455070192314855056) * 10 ^ 70 + 2144136852593929573061257706168630517271876495775151309656522732800906) * 10 ^ 70 + 4561095893098285069027911100761413592247027027450768116076444208895973) * 10 ^ 70 + 9711080526193516595495682913856803311207687411277303436409083598223204

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_191 : Polynomial.coeff recurrence4Scalar0Left 191 = -((((114635204400698466 * 10 ^ 70 + 4904135320383869521524360933746848323329088986923339928696246408437849) * 10 ^ 70 + 5893127208544983724664579164291161283022624455897783957044300958598333) * 10 ^ 70 + 9261925054538661000372215633719628989876677003969715800034646585833299) * 10 ^ 70 + 4045930621979266438803602504315325639514478886086125529546857620273022)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_192 : Polynomial.coeff recurrence4Scalar0Left 192 = (((268959021318884325 * 10 ^ 70 + 3115875796931118003297423114593685159066435973400230219242709519443376) * 10 ^ 70 + 8638549390728658368053392402027000891381379301617966425853966542591074) * 10 ^ 70 + 7011040693678147738578025556420852684654900985095247577415111842175461) * 10 ^ 70 + 2901447079143204745618106348477341307077453546669622660354425674542757

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_193 : Polynomial.coeff recurrence4Scalar0Left 193 = -((((622079637552590887 * 10 ^ 70 + 4413687491115518730238730752884431102648317678374297714320657614591981) * 10 ^ 70 + 5834892390007601181148142193014600615186431785403884077410694599864470) * 10 ^ 70 + 9150536151890478504320896395519059009846482081301615316143014012662) * 10 ^ 70 + 3556219653838139246403761626747615645291250665393170071561204194703565)