Recurrence 5 lookup certificate: B2A2 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.recurrence5B2A2_coeff_184 : Polynomial.coeff recurrence5B2A2 184 = -(((12300755274771914 * 10 ^ 70 + 773549778073779754782156440503565832839496730514381348443784341132046) * 10 ^ 70 + 5202030591022399759534305826521551862384867722740679954276815087900606) * 10 ^ 70 + 5532253652458754273339951555036255059972869829010510017505298246932055)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_185 : Polynomial.coeff recurrence5B2A2 185 = ((7986123934412801 * 10 ^ 70 + 5249809862509781274820046353052095991970048982332784069415133010532798) * 10 ^ 70 + 2694864182723050885246666739863689537466730212519680683835568115200714) * 10 ^ 70 + 8116051061763147361838889201248450642582697522068413617438387485387956

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_186 : Polynomial.coeff recurrence5B2A2 186 = -(((4876981231128202 * 10 ^ 70 + 7952229015421207882351175623568758903257908162667346914670316602827589) * 10 ^ 70 + 6413256610186174375837756533637923218984987949806831955773195847844193) * 10 ^ 70 + 9066441165026698262478225729809739034994035324907728541086245391697088)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_187 : Polynomial.coeff recurrence5B2A2 187 = ((2808416905908046 * 10 ^ 70 + 8046504023116676255196032412800884678091942562677980129484715740990676) * 10 ^ 70 + 7416230599115222567201322978879920914665215457437085063373562337025768) * 10 ^ 70 + 811081449573121192706320895476252048567168727801157233928413668937047

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_188 : Polynomial.coeff recurrence5B2A2 188 = -(((1523782745061185 * 10 ^ 70 + 9433752033819035189544732442045598987449626892072162656134198950263142) * 10 ^ 70 + 1171343845806203372916661914849100038830618295896153527119081972415592) * 10 ^ 70 + 5968915934789675641199844395496615101097762621006015636170615901357522)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_189 : Polynomial.coeff recurrence5B2A2 189 = ((775373658596855 * 10 ^ 70 + 9911840754142006586886974561506533734936350496948348734126450448534224) * 10 ^ 70 + 4879065328683247276595111058831938366689665278414041016531213929449175) * 10 ^ 70 + 3024824872050628420569710902336750971768625429696690718100555454605231

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_190 : Polynomial.coeff recurrence5B2A2 190 = -(((366045271063706 * 10 ^ 70 + 5301614061242744641284347227785795795761830507644429864571573338555997) * 10 ^ 70 + 1840970003739199195163098367878677565943049849155421751501237048622024) * 10 ^ 70 + 1623091265252511717082588382661612775268510260197174332731456574732715)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_191 : Polynomial.coeff recurrence5B2A2 191 = ((156620874784390 * 10 ^ 70 + 9016221990547509264601205227270591153530240910975066833534297209985692) * 10 ^ 70 + 9710033654988713955934391982885375041136464949505724803401496844429839) * 10 ^ 70 + 9159442614766484171980632079913036591655392104515898400354267888491316

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_192 : Polynomial.coeff recurrence5B2A2 192 = -(((57372470679003 * 10 ^ 70 + 2416168296729820651261964451492616813862137978036865452076478162617708) * 10 ^ 70 + 6545817133343137779682736355570759697194100980928270331156407461049928) * 10 ^ 70 + 5960830632825832706977038240657468728869755955259101914024984417061622)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_193 : Polynomial.coeff recurrence5B2A2 193 = ((14762980637724 * 10 ^ 70 + 3343713799975189522870451094830888685915520098866014317899625181742772) * 10 ^ 70 + 3520011419676396833255028866702593349702310952128460126895806051360532) * 10 ^ 70 + 1477783399893821138148406162745441194795509132802560732893089187053387

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_194 : Polynomial.coeff recurrence5B2A2 194 = ((926838118679 * 10 ^ 70 + 1621674819103230374755103664286570166602661395866507812698649584654396) * 10 ^ 70 + 9584923818633413829397011021871893820681356701189292774437247383289234) * 10 ^ 70 + 2342079103814933796231213413454027666060723892955486915028822046658859

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_195 : Polynomial.coeff recurrence5B2A2 195 = -(((5035049523063 * 10 ^ 70 + 1474860024413424603842087335248576294967666574590648883891570087915775) * 10 ^ 70 + 7318264782397813862634219158046881375015279347019878261005697325216254) * 10 ^ 70 + 2168828615133992396623799194597021793467863711219934040543346736411148)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_196 : Polynomial.coeff recurrence5B2A2 196 = ((4864820857674 * 10 ^ 70 + 6327304163678910930840768752712778830569294996242874437043771817210953) * 10 ^ 70 + 339621201133139452459554971700744231942362263220073707047708715924132) * 10 ^ 70 + 5802156161962280106284987662071833217422306685595531125214208915501995

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_197 : Polynomial.coeff recurrence5B2A2 197 = -(((3560575761375 * 10 ^ 70 + 7545061087900235785769878228088506705780721327117179384816418173367554) * 10 ^ 70 + 4205044426375571952654741274067606809630762956620856171555515715847019) * 10 ^ 70 + 4791365462502584151467692514997027856711436046255517712090669019800738)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_198 : Polynomial.coeff recurrence5B2A2 198 = ((2285443885359 * 10 ^ 70 + 1762474966093986580299110903944119314328033123873830611305258297268661) * 10 ^ 70 + 4233497518293514374722219822122315830883016332722816895649629014807353) * 10 ^ 70 + 382675709912755159841400163228343243188582750891626305187140171034073

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_199 : Polynomial.coeff recurrence5B2A2 199 = -(((1350066374832 * 10 ^ 70 + 7672537792436582192859047736791132790271442941319577955045291634721438) * 10 ^ 70 + 157784987479396921611796024843090884561934548619849347534723239275373) * 10 ^ 70 + 8670323835419176116819483478678153409717478082524861330173415916333374)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_200 : Polynomial.coeff recurrence5B2A2 200 = ((749922265896 * 10 ^ 70 + 9783972970695111304254912848725586565197430397697088562423816467998835) * 10 ^ 70 + 520111662090799646391436188744130063445416488685685217166503441227861) * 10 ^ 70 + 6409720475696111438985726455109617124958214022755972043675781487353178

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_201 : Polynomial.coeff recurrence5B2A2 201 = -(((396021321552 * 10 ^ 70 + 1624090457182165553956083876418317270398298034044260263432844285826823) * 10 ^ 70 + 2794185737729759182602568941460854706630484735302649805436241223177686) * 10 ^ 70 + 6659572754505534257571857390359795994730261625917042633039003725318669)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_202 : Polynomial.coeff recurrence5B2A2 202 = ((199990934371 * 10 ^ 70 + 8579816350872286951759798621605796316406549031729708043528874202864449) * 10 ^ 70 + 4745833928512846770010525194796090749784892284005732015871147316829103) * 10 ^ 70 + 23867833522789702960292143609296208705288693823292634757039171965696

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_203 : Polynomial.coeff recurrence5B2A2 203 = -(((96882200578 * 10 ^ 70 + 1588918730944041244007279853872088409822822109015258322463977767522818) * 10 ^ 70 + 7883769683144272853536884451595000466664655094818719675143105915046049) * 10 ^ 70 + 8021148991779649773642155302913710018949845551588333108232548742923743)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_204 : Polynomial.coeff recurrence5B2A2 204 = ((45095998087 * 10 ^ 70 + 654748396423518033346466196690611842800797616266267939186082308904772) * 10 ^ 70 + 5499466148741165790830781361562348614372183599587019800247887846757014) * 10 ^ 70 + 7612416783437328958204734009797349341006926232938132145353026717908192

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_205 : Polynomial.coeff recurrence5B2A2 205 = -(((20193090205 * 10 ^ 70 + 9208895522717874912979048111147950454846780190784841966338988894897220) * 10 ^ 70 + 5869393619631180568804511301295304792567301628614154239290395106369332) * 10 ^ 70 + 7049003293205371672248278203885701581168037793485604457247946827500219)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_206 : Polynomial.coeff recurrence5B2A2 206 = ((8713958196 * 10 ^ 70 + 581956740052625359952754917729140405485645055254408877398505563101758) * 10 ^ 70 + 2173552878437949450461707740018559338921840817261889034886811208629170) * 10 ^ 70 + 8126957807415872661385241445718514604885262727524511206037522136101982

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_207 : Polynomial.coeff recurrence5B2A2 207 = -(((3638451110 * 10 ^ 70 + 3819455266539707516798397339704652339835330941538523877611180433967520) * 10 ^ 70 + 6992410071625239835097269615894249924302758316029008937250565493234207) * 10 ^ 70 + 8686810411685391803559347850045438520959714540909637903155528682198568)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_208 : Polynomial.coeff recurrence5B2A2 208 = ((1482901119 * 10 ^ 70 + 5137307402736299368543665082945612562626578471194868887241116199479477) * 10 ^ 70 + 2052603951684510479126473946245244916554986996681441003194127260621842) * 10 ^ 70 + 7816264802055906542050791941865869239166911129980050116987879370630395

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_209 : Polynomial.coeff recurrence5B2A2 209 = -(((600059408 * 10 ^ 70 + 5848271850398435053496476615168691271615181726817267632813999624266358) * 10 ^ 70 + 297701987511513011579325393703619461875905110675277256845053283412505) * 10 ^ 70 + 5246642838529942840676069711941935529813903246094526564449316495341999)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_210 : Polynomial.coeff recurrence5B2A2 210 = ((247885641 * 10 ^ 70 + 9047867546805332994879224618090751018174572422910416851581088829199894) * 10 ^ 70 + 2961797582109563226375258582845993096419924721730301369008603848163704) * 10 ^ 70 + 4672558445610376012476183600778930013102150244791162591336273626174565

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_211 : Polynomial.coeff recurrence5B2A2 211 = -(((108198585 * 10 ^ 70 + 4003513648956427930146443826751983978189205376952784381040250050419839) * 10 ^ 70 + 8475569976969962023767348878010026922573292061324912730316205389774537) * 10 ^ 70 + 3388779969689048403539736180439595049427997443686813936792304393693873)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_212 : Polynomial.coeff recurrence5B2A2 212 = ((51140293 * 10 ^ 70 + 4149118097948932432832327017549686514277583219826746698516741339361305) * 10 ^ 70 + 3368086344791214124663446929677417781867886641075176839108901477476686) * 10 ^ 70 + 6989496318166930397895778822350987147682781117119296155799576475318553

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_213 : Polynomial.coeff recurrence5B2A2 213 = -(((26093137 * 10 ^ 70 + 8028767684640936788405204868071664462923179748677733855849546993454635) * 10 ^ 70 + 5927814075767490002579851450062927423310875535901162097919120669935275) * 10 ^ 70 + 8882754949640865374790576925316127938909058233172508967894973067251441)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_214 : Polynomial.coeff recurrence5B2A2 214 = ((13972647 * 10 ^ 70 + 3331651994033822976802760675330865757762094294773313530415375763413547) * 10 ^ 70 + 1576685413445754622211718820879015842857802038321700159529143876460966) * 10 ^ 70 + 7225603812760674547331437989580047148200499731917196846175080924964609

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_215 : Polynomial.coeff recurrence5B2A2 215 = -(((7591928 * 10 ^ 70 + 9112224572006329232883775314492392905557961267431999048466133774639442) * 10 ^ 70 + 2988904043615760646735377572415698823299100763830011049508520295902461) * 10 ^ 70 + 1420432701814508840683762637050945521920433467329862011379611187404063)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_216 : Polynomial.coeff recurrence5B2A2 216 = ((4080720 * 10 ^ 70 + 4635169006861128124330566316879262231981660277696960630579444277720180) * 10 ^ 70 + 9957254030079069876849123707152713540184228442859854050941780808763342) * 10 ^ 70 + 8535979515447568265146109180827767383075720355937129235507743509529618

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_217 : Polynomial.coeff recurrence5B2A2 217 = -(((2138209 * 10 ^ 70 + 9650294636940918179219992111564715796039557231636253725608273810935978) * 10 ^ 70 + 9244322056940981662461603325221450532174962909634222414764452769423703) * 10 ^ 70 + 1199027910198775580765507764122974548575544959341441737257852466537079)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_218 : Polynomial.coeff recurrence5B2A2 218 = ((1084478 * 10 ^ 70 + 8390634276571582110446119613246659977137250091826670798989827898350256) * 10 ^ 70 + 601515074645328491605291287255157739805954603256811799323215994006974) * 10 ^ 70 + 2851893576141108519636235154487074467623267124670294770444037193121103