Recurrence 5 lookup certificate: B1A3 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.recurrence5B1A3_coeff_184 : Polynomial.coeff recurrence5B1A3 184 = -(((3172591669950470 * 10 ^ 70 + 3117848169261494798353356916486739123748733135827238134365795456001274) * 10 ^ 70 + 4024229980423821147446948768939578893263184663804797363974949577025814) * 10 ^ 70 + 4544916761693237964402363004850624024107076442551175421767562095715774)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_185 : Polynomial.coeff recurrence5B1A3 185 = ((2621383613296346 * 10 ^ 70 + 8781073551209731810679929409237878531690981457957746368798145741638424) * 10 ^ 70 + 7130748609238725168858905521779363818954798838442021429076002589109228) * 10 ^ 70 + 323675767094156735014036061534654877507548613961146890639932043327589

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_186 : Polynomial.coeff recurrence5B1A3 186 = -(((1887171857404294 * 10 ^ 70 + 931911352196016422908787924834950597444092475119787234918267600202328) * 10 ^ 70 + 8493047673190939274910351570194789860642081461990711258455485488547967) * 10 ^ 70 + 6151762300291903139560878929101501394810066048628203285538828418157449)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_187 : Polynomial.coeff recurrence5B1A3 187 = ((1235412132012376 * 10 ^ 70 + 2555563888233247413025374429569548601497250915271488522123071137006562) * 10 ^ 70 + 4066929186949037322117212937288759207670784113706921523058481647719162) * 10 ^ 70 + 6996002436330733963264237931071747300879406937121372321532417334022480

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_188 : Polynomial.coeff recurrence5B1A3 188 = -(((748696731855336 * 10 ^ 70 + 486606207628409066254395736746351236023678698564299235490255241674132) * 10 ^ 70 + 909338820213000186556474152262090225773257993130058025209417181838912) * 10 ^ 70 + 4264056296064662189191608241060553093141651885874929471271553497973066)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_189 : Polynomial.coeff recurrence5B1A3 189 = ((422825305877086 * 10 ^ 70 + 3519185704377583867568448620935708545939899239571648014804907625187904) * 10 ^ 70 + 9169836865984658429206537641955046439237212791648950714210347147004740) * 10 ^ 70 + 470572064581151257910552748873882425279213954326782187641906021266229

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_190 : Polynomial.coeff recurrence5B1A3 190 = -(((222229740744681 * 10 ^ 70 + 2253480997395341638415843587555543183511919162069991231176880392894533) * 10 ^ 70 + 4823033426174026435445318445979140957933343698321347386286122978935165) * 10 ^ 70 + 6959041041792331820486517308192123663131890679963738918856011017613911)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_191 : Polynomial.coeff recurrence5B1A3 191 = ((107552472377463 * 10 ^ 70 + 6602247201734166220241145215369825578262419966262754569733473317838368) * 10 ^ 70 + 9136994020176901661294883521012983543484357388129835429231133057359544) * 10 ^ 70 + 7466169135345708378890484148024810779206553276349096908817478172612229

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_192 : Polynomial.coeff recurrence5B1A3 192 = -(((46606450430257 * 10 ^ 70 + 456844321509393360567145812862427459816622015845000229310752810824835) * 10 ^ 70 + 4173802211862737196382950516622449126191953917835299588592230130126274) * 10 ^ 70 + 8621625054562789528509426334325685787425430004209793044022347567881176)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_193 : Polynomial.coeff recurrence5B1A3 193 = ((16742386760387 * 10 ^ 70 + 6623260712028782546722332134196918591378209828961649043404801115809848) * 10 ^ 70 + 4662605462728452840486516023006610079913128395930849788970852674289665) * 10 ^ 70 + 4805912896633660437112948966073948045025359611846427144277940217379568

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_194 : Polynomial.coeff recurrence5B1A3 194 = -(((3568930129904 * 10 ^ 70 + 1065297006426968911923491700488599011707087216948333128718073285438145) * 10 ^ 70 + 5739038902233538676682236846271119735828133321385335691535034118548973) * 10 ^ 70 + 4631533997043068430736523952176621060328585249498308584513635282414862)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_195 : Polynomial.coeff recurrence5B1A3 195 = -(((1333547296810 * 10 ^ 70 + 2216305558486899146392464377441179985974294823536595952796049491704330) * 10 ^ 70 + 5204591863562158963313542386988232569804294301857263441855844766998820) * 10 ^ 70 + 6653122931166873624224158340259947558725365835201298024762289844821909)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_196 : Polynomial.coeff recurrence5B1A3 196 = ((2529770858323 * 10 ^ 70 + 3991846018269387864685888735024711478510602111334144104028652711276834) * 10 ^ 70 + 1537661530406075109807856986463839392047593285314454766033856505157249) * 10 ^ 70 + 8551595564773514943150020935025645944600954872603541482564866368500349

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_197 : Polynomial.coeff recurrence5B1A3 197 = -(((2304965858753 * 10 ^ 70 + 2677058927590319329646105272622864060280333153859424376486219340695701) * 10 ^ 70 + 5801231657780276148139482443439712902433547228618599283386464382980735) * 10 ^ 70 + 7576614802840951231231338880183659349267276068337252921183431444086091)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_198 : Polynomial.coeff recurrence5B1A3 198 = ((1697646554394 * 10 ^ 70 + 2032209954997916685285323156479072224858634970257874339572368399589805) * 10 ^ 70 + 6925305507251209957381879046683276073597066325766748168519794460481935) * 10 ^ 70 + 7565771053707463287212019480590706036012791571371480231649652576624915

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_199 : Polynomial.coeff recurrence5B1A3 199 = -(((1116377313102 * 10 ^ 70 + 8420355740900661889566800591895212748325652513580875918620440474882640) * 10 ^ 70 + 259714484143456839074677500539711414601778883523873964540868294741728) * 10 ^ 70 + 2541935240834607829598250917137458564423206110891246393937907065545389)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_200 : Polynomial.coeff recurrence5B1A3 200 = ((679767278873 * 10 ^ 70 + 8648215487895280297808510023085974048733903463415736239181041463608486) * 10 ^ 70 + 1537380300299218648046191192902181524591328892605269487941292788942818) * 10 ^ 70 + 6323652081702439490088518861912173992421571914594463499760044249620063

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_201 : Polynomial.coeff recurrence5B1A3 201 = -(((389725248462 * 10 ^ 70 + 8558417394915663132269896035300230952890739277026546543632851803258402) * 10 ^ 70 + 9478403886091046361030048377874796622736559918480966017024526107241348) * 10 ^ 70 + 3998604578510787326085015178137707339285632630633665691212507764794302)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_202 : Polynomial.coeff recurrence5B1A3 202 = ((212154418763 * 10 ^ 70 + 7804424256375848388738927977913339617585869769049884057395329953433419) * 10 ^ 70 + 4299578897460946657485598985741495911093559463618574770836555462044105) * 10 ^ 70 + 5563797137564573992329345829246825795929329569478371685906908270413776

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_203 : Polynomial.coeff recurrence5B1A3 203 = -(((110111236024 * 10 ^ 70 + 8988784018832301300441820823051185894631096471786290786991942922622019) * 10 ^ 70 + 7071578226540123125623985269664034011509241499030945694007422822956294) * 10 ^ 70 + 3578402077751291555727661065894815315764010741193879509274439243365660)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_204 : Polynomial.coeff recurrence5B1A3 204 = ((54572852897 * 10 ^ 70 + 8578908346250739957737607651832341858875629635312563417396973118796284) * 10 ^ 70 + 2060268933698258458333030335547640611743017905843939103148494650494903) * 10 ^ 70 + 191918819248137013658158425597695392742159031212001340651888798144104

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_205 : Polynomial.coeff recurrence5B1A3 205 = -(((25821654441 * 10 ^ 70 + 8155186010385139644844567201366017076595103311423546883694464988973882) * 10 ^ 70 + 8100781927035281062987285433322905031471291157564319623448037228364624) * 10 ^ 70 + 6661260502410617490441244349715174669515247355482675384662086118173788)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_206 : Polynomial.coeff recurrence5B1A3 206 = ((11643438502 * 10 ^ 70 + 9961377340920586411927444420664077116433370739592159700617960828458275) * 10 ^ 70 + 5666441157685412409711130500151390042895916519666964370334696793016174) * 10 ^ 70 + 7157068832754152017845244954436222336939494210634043394397089515158908

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_207 : Polynomial.coeff recurrence5B1A3 207 = -(((4986327634 * 10 ^ 70 + 1702527065842475973354232269621562616995053016910181878739572577071752) * 10 ^ 70 + 6433998375580226983483926668695394432385370304210025259300031286013684) * 10 ^ 70 + 8980838355552498279853346672808111387222163017797870033304037292216582)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_208 : Polynomial.coeff recurrence5B1A3 208 = ((2016751701 * 10 ^ 70 + 2178418428828565547347595843990256980503173717245865072322027514923625) * 10 ^ 70 + 1236588640991712635418375259586079303909091891161471923441225074245792) * 10 ^ 70 + 7265265163514030305685426556476468182038830934849421706190294844242350

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_209 : Polynomial.coeff recurrence5B1A3 209 = -(((763448485 * 10 ^ 70 + 3086207580169140902575806387481179727443434073319832386993911194951860) * 10 ^ 70 + 403029516977474598080311938671728230743586505225714037206436177851154) * 10 ^ 70 + 1290784094002481573710865460093776032063672840648463053756710745985018)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_210 : Polynomial.coeff recurrence5B1A3 210 = ((266381632 * 10 ^ 70 + 2883601699803619232280385893110904424343187164137131736083369722858537) * 10 ^ 70 + 8098114128377826264987808525925944697496316828082925251435867323558671) * 10 ^ 70 + 8113547118028783060586430630659794177392201918234735600867210808077250

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_211 : Polynomial.coeff recurrence5B1A3 211 = -(((83204665 * 10 ^ 70 + 1718606093450564055588283071481128692328769085309022351459103220391020) * 10 ^ 70 + 1517764067465709471356340651340817787307846982853555459305892280608938) * 10 ^ 70 + 3518414088256057631299828967530141063624482427030208000813972028674328)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_212 : Polynomial.coeff recurrence5B1A3 212 = ((21730866 * 10 ^ 70 + 9212884718067363178953977770008683935771164228571309176215820200983714) * 10 ^ 70 + 7792103897002764463488975581515098349866644129708212597762750586605502) * 10 ^ 70 + 1143151295615856166579896845372144042849678343300387133711178929717256

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_213 : Polynomial.coeff recurrence5B1A3 213 = -(((3705583 * 10 ^ 70 + 2783985133226448623810973801778259451462411594684398541066303228628749) * 10 ^ 70 + 8686953999975839801623027734567091262337832716612217906205399264385090) * 10 ^ 70 + 7449276995364027555979433556241350385058342637213582152088009045646793)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_214 : Polynomial.coeff recurrence5B1A3 214 = -(((421235 * 10 ^ 70 + 3903460176081791154604124754344037892331359721584313672093286909549665) * 10 ^ 70 + 632182762951011656806632710151250035285978996641248593009369120918687) * 10 ^ 70 + 5315399510973165997742630496122375972900190811041493096151151709623909)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_215 : Polynomial.coeff recurrence5B1A3 215 = ((804500 * 10 ^ 70 + 9054267417714945479659398415506508145253262055986134820165404566569026) * 10 ^ 70 + 8195540981397872084381048793846561325717787355087667272315131625340543) * 10 ^ 70 + 2978225367282056727121212470187079684058805016582800497782460923020796

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_216 : Polynomial.coeff recurrence5B1A3 216 = -(((500391 * 10 ^ 70 + 1417315261298425192553785875182464074384961866037431730035080119143047) * 10 ^ 70 + 3746406204411280510118573328758001986681314964372017669803036561392785) * 10 ^ 70 + 2452357915191370770370315949858418295134448069126264372072436918076121)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_217 : Polynomial.coeff recurrence5B1A3 217 = ((237142 * 10 ^ 70 + 7135719865686587007320314450714139296646413577273072971759564641604467) * 10 ^ 70 + 4115480429313470707998534123961826066678077159472197025002255236551206) * 10 ^ 70 + 4889454087389417314501725750835269187966613456138538016248254445075939

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_218 : Polynomial.coeff recurrence5B1A3 218 = -(((96974 * 10 ^ 70 + 1987984446919245652789344979551161880668959896863176242109012358079752) * 10 ^ 70 + 7122809058969689464147973479232192172109083057242984086151120232909337) * 10 ^ 70 + 4643990619779582481603864028768459212604674215392200434298172040613601)