Recurrence 5 lookup certificate: B2A3 coefficient convolution

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

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_183 : Polynomial.coeff recurrence5B2A3 183 = ((352382914316756 * 10 ^ 70 + 3106620601373648582056319184045735706894697796334385558924104842885649) * 10 ^ 70 + 5816551977432280702509403094929565729093663377862418109204820111968631) * 10 ^ 70 + 4176413435967663861397936819748140951606256426926068618828406084644472

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_184 : Polynomial.coeff recurrence5B2A3 184 = -(((208084786633657 * 10 ^ 70 + 4259707813135106901587758027756676093703084081615531687088374922480671) * 10 ^ 70 + 4933968142979061432206904716657867142669796555364968241689550493351144) * 10 ^ 70 + 1100194931656596142080724680886447276173058246727832415068237550375410)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_185 : Polynomial.coeff recurrence5B2A3 185 = ((115245238534358 * 10 ^ 70 + 2916853538500727252279382743964083076178241870300013639110010579860846) * 10 ^ 70 + 1530942092169338702952386424081532692299415792940370018323032966455908) * 10 ^ 70 + 4685001977229890997816603122055160331743237229620220467976006266308174

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_186 : Polynomial.coeff recurrence5B2A3 186 = -(((59509068720985 * 10 ^ 70 + 6487549448428391460378161674886199236151323415658705760665528626093926) * 10 ^ 70 + 3464669180982536835873937381267315928259206997565842478941074071956109) * 10 ^ 70 + 4336559784672732381689172319466850712574539089720222647578098768999050)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_187 : Polynomial.coeff recurrence5B2A3 187 = ((28226426042342 * 10 ^ 70 + 5869179443661848573755372548601939779819151544216997940098678407802356) * 10 ^ 70 + 2383078414116010728829126866725007532620740749093572902030816007232982) * 10 ^ 70 + 8623215895216636834168704349290202153130852133216122537943390734827860

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_188 : Polynomial.coeff recurrence5B2A3 188 = -(((11875026520815 * 10 ^ 70 + 1360188031497922287397615722232991211272513013007608211991526178273777) * 10 ^ 70 + 8861179274758561386342123086035285703713189211814702911190215397970297) * 10 ^ 70 + 1596350281992745606129421693705757731809129850418290199379578030696172)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_189 : Polynomial.coeff recurrence5B2A3 189 = ((4012764492363 * 10 ^ 70 + 377430900950862728834502284605279396705546973687948504916936943523187) * 10 ^ 70 + 3141838044715843148733058852698701120574778764349126742476171922158863) * 10 ^ 70 + 4221460128804175163184934220075247494567333515652393616455248082608749

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_190 : Polynomial.coeff recurrence5B2A3 190 = -(((637740799541 * 10 ^ 70 + 6829337798901231008055332391320472231408112321712985598376510873353945) * 10 ^ 70 + 2449139227409918442716354397375834803800662191599150350985647950439319) * 10 ^ 70 + 7177534473350100227065471518569895785110400214695636158511299106677571)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_191 : Polynomial.coeff recurrence5B2A3 191 = -(((553562745379 * 10 ^ 70 + 224834889361838679011531114772306170240597166740707499991560907037237) * 10 ^ 70 + 3943975931900459621879894308877305395836852752017157365722489938853346) * 10 ^ 70 + 1599962829393173744170093031788043248484481306703204984487466732250014)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_192 : Polynomial.coeff recurrence5B2A3 192 = ((791147051783 * 10 ^ 70 + 2614130065297292968203636780930294886809727383963883715193752936368252) * 10 ^ 70 + 6851084196852072087469976550556441025761602545597603666380434314024117) * 10 ^ 70 + 8005314797131524400097646768616310456453090082880479198941429330579330

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_193 : Polynomial.coeff recurrence5B2A3 193 = -(((679907189728 * 10 ^ 70 + 540970921001196055619278038513352406153192163910092774251828403601530) * 10 ^ 70 + 3846631964686254119887000087656320421181495985477465649476954782300473) * 10 ^ 70 + 1050500036095072821743301453523146400804949697017956052265001221130277)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_194 : Polynomial.coeff recurrence5B2A3 194 = ((487965919058 * 10 ^ 70 + 1109305376975709931795501639046729146181611178269447490797363442852194) * 10 ^ 70 + 5995185731389675032312386232722538713906437564304327531124747856413884) * 10 ^ 70 + 6962259221012392555341984260368734241549114933016556062166833578066670

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_195 : Polynomial.coeff recurrence5B2A3 195 = -(((316334678791 * 10 ^ 70 + 5631056189221049116183091294457188654763183828148852256737357442178458) * 10 ^ 70 + 4419644912644108694759949802842893140786837237934523811679066669045330) * 10 ^ 70 + 4692597031485957068773364072184164669424202373202983103560196685390958)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_196 : Polynomial.coeff recurrence5B2A3 196 = ((191004179411 * 10 ^ 70 + 384231703470269965223739389725277060290520616174273798129853473018883) * 10 ^ 70 + 5712037787362068054622811035132391650702801602968925833193088068069622) * 10 ^ 70 + 1309804990076878389439409163530419603851373329955841934539734115923686

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_197 : Polynomial.coeff recurrence5B2A3 197 = -(((108981784147 * 10 ^ 70 + 8928654090943987705025682533593087717076242567929845141407487420083327) * 10 ^ 70 + 7898180848202491891789784612173053343055624470677168962264224057982300) * 10 ^ 70 + 664161491024038366065400976194701299008391472240593698533047366367442)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_198 : Polynomial.coeff recurrence5B2A3 198 = ((59186381141 * 10 ^ 70 + 3059510932837058656265463850347801081333181208969978847233402859080165) * 10 ^ 70 + 8730522442371465483789390094891990215687603166332371927771251677519349) * 10 ^ 70 + 3454791079584344410806748685230037875786002055631059846384217309339870

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_199 : Polynomial.coeff recurrence5B2A3 199 = -(((30700349678 * 10 ^ 70 + 6240082259299287476597035219522053147788877976337676117583795441106232) * 10 ^ 70 + 810956993985941530340328562951877175705001480320485742963611198692779) * 10 ^ 70 + 2523139526717817436739948922494207631268829566334102151781496259845944)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_200 : Polynomial.coeff recurrence5B2A3 200 = ((15228480955 * 10 ^ 70 + 3762539379204706327467904055605776383078986479790941976223585914045211) * 10 ^ 70 + 4103482237028659183293245831190906276827002931817231001156449845147930) * 10 ^ 70 + 9640766819751873013519797343661933175373303399246678819332609726115262

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_201 : Polynomial.coeff recurrence5B2A3 201 = -(((7223001046 * 10 ^ 70 + 7767404090394287630905603426214570721133901714678625938294476786311159) * 10 ^ 70 + 3331111897050182560829960254365480578460494348826772091586731377981378) * 10 ^ 70 + 7985428895537705892887307152018985255883066461760362974085781883948190)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_202 : Polynomial.coeff recurrence5B2A3 202 = ((3273192663 * 10 ^ 70 + 6693181415517279169060815810370644662139048406985032928403001550491130) * 10 ^ 70 + 8369769335788572192181469499656657724846940084677475043455599799607890) * 10 ^ 70 + 4886251051686034241672677497451159046786861453190755244909915543583070

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_203 : Polynomial.coeff recurrence5B2A3 203 = -(((1415976056 * 10 ^ 70 + 3596193485812195796989242817991533369681595605644689051041535875520042) * 10 ^ 70 + 8075598903560876667466849186271569718633689695488763692472028751086044) * 10 ^ 70 + 9752409758998293821844978403143553011013880435298677266738597249968317)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_204 : Polynomial.coeff recurrence5B2A3 204 = ((584949954 * 10 ^ 70 + 8998598442698872612662394309303487555058133519335397325275973199252544) * 10 ^ 70 + 8155113466008229339480436138811174209018105526239486611000324012206463) * 10 ^ 70 + 5617625777146945952254776252998617003901443011826631072816097595133108

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_205 : Polynomial.coeff recurrence5B2A3 205 = -(((231671320 * 10 ^ 70 + 7430589634659818635101964262398158825311442363882586991124962053510498) * 10 ^ 70 + 6744647959781755533930982112846220996006438461726688404814085869796010) * 10 ^ 70 + 7185221055008654707760862940948146814984575589573055228257660201714326)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_206 : Polynomial.coeff recurrence5B2A3 206 = ((89064932 * 10 ^ 70 + 6196776714131466090016869479495838085831466122299628508659612991390329) * 10 ^ 70 + 7547357581053795778981422791067990707519610453232150218039590137943825) * 10 ^ 70 + 9964534410959329274987815684055004397332680212882339460794893495493575

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_207 : Polynomial.coeff recurrence5B2A3 207 = -(((34209280 * 10 ^ 70 + 1221770088766626440887686728469665080450931069360758176538169870109358) * 10 ^ 70 + 7504779399429640522150884908019458594496472321587737344181884040037089) * 10 ^ 70 + 4492662972987118044588946562614080986621948260965031399709413986696916)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_208 : Polynomial.coeff recurrence5B2A3 208 = ((13812153 * 10 ^ 70 + 3744063093435506570632420583117931533614298169902042156109049681662335) * 10 ^ 70 + 155255044648451325094645690026228748779993630027201536784496106764875) * 10 ^ 70 + 9709373438082877059762337442998982445923040727177217319654653608362568

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_209 : Polynomial.coeff recurrence5B2A3 209 = -(((6204201 * 10 ^ 70 + 1031196967946206277302966929713269342520781038107705254914321251451857) * 10 ^ 70 + 1933271522863414292290852658479150097163687939603425487626231688550739) * 10 ^ 70 + 3972604820159112800121525000335913905781766471379066650983577734244600)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_210 : Polynomial.coeff recurrence5B2A3 210 = ((3155854 * 10 ^ 70 + 143775695949349263134505994185985735809903745572906961210453875212874) * 10 ^ 70 + 7069945440020243303570349353050017185114705841512871280219000750178832) * 10 ^ 70 + 7261955632183353065030477954753658604388499673083568453541587653114657

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_211 : Polynomial.coeff recurrence5B2A3 211 = -(((1747244 * 10 ^ 70 + 6604792074604942990573296254067081806474718131921922184472786305371167) * 10 ^ 70 + 6231418425670038411497811415986801337322646303659300374838908426610233) * 10 ^ 70 + 3523790488155184757938860601819947966376283661633860296277210770838730)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_212 : Polynomial.coeff recurrence5B2A3 212 = ((993351 * 10 ^ 70 + 3946839383434243221338638972341676530757970481578678319460788909343659) * 10 ^ 70 + 88729787418643478852082688381514973404429421125179622637907854862626) * 10 ^ 70 + 4269712500069810794952489523805305607415848631528705805525712045709437

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_213 : Polynomial.coeff recurrence5B2A3 213 = -(((556442 * 10 ^ 70 + 3163051700850701796681576669069334507688303584340600953737772380942451) * 10 ^ 70 + 892915176593928555277795403985470687702784775536261627587406581067392) * 10 ^ 70 + 6952273621517187217560628396777978879084116803483246748267971723027064)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_214 : Polynomial.coeff recurrence5B2A3 214 = ((300906 * 10 ^ 70 + 3174901380127088969569000581074614280756289789191058032863202283602536) * 10 ^ 70 + 5731061802906432264557300351485393257656086050038931080610814839837382) * 10 ^ 70 + 2219464342585982712387756918155028677897990967506483272586796673966607

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_215 : Polynomial.coeff recurrence5B2A3 215 = -(((155894 * 10 ^ 70 + 8907009656679085608086838223970877966952468679472345746076778083914631) * 10 ^ 70 + 3809388396013125537776987996605691235506266438985661691955841223180769) * 10 ^ 70 + 6453287495727374737058160968484301557361824617143917726766042912405678)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_216 : Polynomial.coeff recurrence5B2A3 216 = ((77262 * 10 ^ 70 + 9601544337318447748566123922125662583393772523120514705331437939944674) * 10 ^ 70 + 4773343444367142708463126145017642510812177779452585137688421312041120) * 10 ^ 70 + 164443704340924315427292495750596621337162133555472127011263032717329

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_217 : Polynomial.coeff recurrence5B2A3 217 = -(((36667 * 10 ^ 70 + 6121344507718293062894073448914756448777551401784330587430342360471543) * 10 ^ 70 + 1080684356790561157528417933985036705313390996954296575029191235981090) * 10 ^ 70 + 8491637660691037799403738615710162817622475601925667027498415609811366)