Recurrence 4 lookup certificate: B2A4 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.recurrence4B2A4_coeff_184 : Polynomial.coeff recurrence4B2A4 184 = (30133265558152961431373882846928946854677460012370314215660228 * 10 ^ 70 + 9440056312031720713963442653721646454372652607665480727882397687289381) * 10 ^ 70 + 4001663038327011752664754390609513090999664021251629654376721141131804

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_185 : Polynomial.coeff recurrence4B2A4 185 = -((44247912640213762662832731349748545675839100640123288076571499 * 10 ^ 70 + 5552058834473936468442016339953407135345260242980576027571564029356045) * 10 ^ 70 + 4228570261313693251417813288368424841282388895772592271290668254721674)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_186 : Polynomial.coeff recurrence4B2A4 186 = (51039492011837523225763920884061806890843394154463902503156364 * 10 ^ 70 + 2874309748139645201331327307600064608713865780998056662856594624260561) * 10 ^ 70 + 5367836118007721834196278605729604310705328790534954071520716989853015

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_187 : Polynomial.coeff recurrence4B2A4 187 = -((52229254588023775380952823407197853510891057029461733172208613 * 10 ^ 70 + 4392002813887210094780630075075706428833850926828315564192000337015218) * 10 ^ 70 + 4364928946412645461535592115968722092376888587675342886398963715189998)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_188 : Polynomial.coeff recurrence4B2A4 188 = (49482535166656662181985493790283769578529581477539947488704309 * 10 ^ 70 + 7454355911943167766266491877532920876556111988442881547191539053751165) * 10 ^ 70 + 4082839578547991830889990287836003837871686698160650480674607649792121

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_189 : Polynomial.coeff recurrence4B2A4 189 = -((44279697623295983143442203366998175240058096500636140253430227 * 10 ^ 70 + 4889656809440252959274109176327112223845548377009554302665639017231000) * 10 ^ 70 + 4076372501070927908277187876495301280334071857144117933609382359863985)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_190 : Polynomial.coeff recurrence4B2A4 190 = (37838097148541595954384460852302644758131680493789380842211616 * 10 ^ 70 + 1387578599796180278939417271455166308027270564704805233433972791458598) * 10 ^ 70 + 7737110549373412125907720253179295359185626933732663879187914758905121

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_191 : Polynomial.coeff recurrence4B2A4 191 = -((31081489342007601300207378625049300637639037698487437339584405 * 10 ^ 70 + 8335431495171187180169517164510975397920278898831478875195290324721911) * 10 ^ 70 + 9723728696255969449707020988190005599506967000164077351630165806066582)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_192 : Polynomial.coeff recurrence4B2A4 192 = (24647896136064416033392903639478364114171325225126563444037519 * 10 ^ 70 + 7409429670119107601177547716775705943897654947807184113878278546019044) * 10 ^ 70 + 7204358033747075687480890418209433045078401995115928247137118867635841

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_193 : Polynomial.coeff recurrence4B2A4 193 = -((18924237988843966971234575671583979488245526142142049653054269 * 10 ^ 70 + 6052119351209351579789855801104928297718250822881947474535757779939143) * 10 ^ 70 + 7969016972902244765009009573365029426959271801871540851993184255924696)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_194 : Polynomial.coeff recurrence4B2A4 194 = (14095798094713771294407681160663223678425258510743215910638846 * 10 ^ 70 + 5914144929105335121659453240005210527329796621014386050619666300643324) * 10 ^ 70 + 7786468723233298982889597671288715497782004281298848211626178326848394

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_195 : Polynomial.coeff recurrence4B2A4 195 = -((10200165288699838741606185638750641257955246216113122357036098 * 10 ^ 70 + 1106857221601315415974368791797608396415389428127280912698384146841127) * 10 ^ 70 + 4848568517190593543335448468157941680352628642227683509739850448015029)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_196 : Polynomial.coeff recurrence4B2A4 196 = (7177927092645861755694275241542382551969843330799977564740427 * 10 ^ 70 + 5144048130320431563133563319080102126169701318794273903218842172994793) * 10 ^ 70 + 8864185691831212650445557734922936503821643235412279461464741645466807

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_197 : Polynomial.coeff recurrence4B2A4 197 = -((4915315490660395643080805411187436613326709931276797742787367 * 10 ^ 70 + 4686576909425455322840689309437565754994415977516418666062658387449458) * 10 ^ 70 + 6573040781874567566868564585358313799269487991693129325718637472763199)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_198 : Polynomial.coeff recurrence4B2A4 198 = (3276679373167342738210241113666875064810112737587359533585081 * 10 ^ 70 + 4924580478496447698410713394459690943517892663815963129596301947806725) * 10 ^ 70 + 8224988131183916565261783452154331087834925073160442834192509884989754

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_199 : Polynomial.coeff recurrence4B2A4 199 = -((2126728799267364192580746398098023381000101898621280477000638 * 10 ^ 70 + 756792150102203739780480305437146818239911216845553659535994709547351) * 10 ^ 70 + 1373184177084807359498157894756701771296281092084682832178410138682323)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_200 : Polynomial.coeff recurrence4B2A4 200 = (1343844124510073055770292166612846166790465565290624128762530 * 10 ^ 70 + 2865003504104487182093611871053632750978099937328315920521475514460955) * 10 ^ 70 + 3996068370713597403658525183078642777322909488855514604983203845465832

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_201 : Polynomial.coeff recurrence4B2A4 201 = -((826411824046306573220893432529425553111881162912555646350300 * 10 ^ 70 + 6142460338988360358361849770028548218162552171787487542820738525826051) * 10 ^ 70 + 7377640570600162003575413859621260951234517084075223274741183889160532)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_202 : Polynomial.coeff recurrence4B2A4 202 = (494283475397210825357194122676733699282081488315550705600047 * 10 ^ 70 + 5628986875814623507161979775295691910228556610704063189600429464242996) * 10 ^ 70 + 8711959561967899470671662883614689683855300529738045214330793567893577

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_203 : Polynomial.coeff recurrence4B2A4 203 = -((287237281960925168379380213442858490946834492295733258856204 * 10 ^ 70 + 1281560217966890452682346090659210964676433515853798870321962493999695) * 10 ^ 70 + 3663979522230024910064529385595303658875133001841255913800125059163043)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_204 : Polynomial.coeff recurrence4B2A4 204 = (161924965360436954142256714765718969447421484276982521780630 * 10 ^ 70 + 8307453513939647264497677598225366501630452525785691725407480531908079) * 10 ^ 70 + 7304255480408438333370674601712966956604957793807858869593396988703396

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_205 : Polynomial.coeff recurrence4B2A4 205 = -((88345247746627597550604985344229211587646576050543379061465 * 10 ^ 70 + 944729125827129943774563885004592807609828585014111264007909475195661) * 10 ^ 70 + 4380627398817974913596803716639839868461824827457812963906169186012431)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_206 : Polynomial.coeff recurrence4B2A4 206 = (46485636310668830006429303369874310411641654697878462109127 * 10 ^ 70 + 1262445158527248787775901852292045644323490736510901663732688919542511) * 10 ^ 70 + 6984887759693393857103230967839103468823412817979163116633731799526823

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_207 : Polynomial.coeff recurrence4B2A4 207 = -((23460299549333503256379512142750205521307873183588639682927 * 10 ^ 70 + 1989739327165493213633937841340692203172436914931018546620378979017693) * 10 ^ 70 + 5898437506375488826717419135645429661321874791300320408966943603545980)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_208 : Polynomial.coeff recurrence4B2A4 208 = (11253912919950975392239360968550853457350781441142823489905 * 10 ^ 70 + 9218626635194476002644715758076946912622299498141411902055923144548711) * 10 ^ 70 + 1925205011129021083596875952458058069975333500813799716445660386671141

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_209 : Polynomial.coeff recurrence4B2A4 209 = -((5049296226867692087088437926477874115744443456974590995466 * 10 ^ 70 + 1031093544237341692139019312447598776842133313984846697036554665876380) * 10 ^ 70 + 3918112193644306548157905704722230527377965756552291577573137257113888)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_210 : Polynomial.coeff recurrence4B2A4 210 = (2050720590460253431541816781088164222708141287455789075717 * 10 ^ 70 + 1214140503131395761900243211187186968396101279071477504800080155429137) * 10 ^ 70 + 323357318198974958327023646188083755998077946610748171417050387371455

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_211 : Polynomial.coeff recurrence4B2A4 211 = -((693488211905971793172973404724479669441857142585624137527 * 10 ^ 70 + 6924281582313877147847291112097342240374493056603736454772128187494408) * 10 ^ 70 + 9979865382563708561578515170279029491382807866465704646623336357083642)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_212 : Polynomial.coeff recurrence4B2A4 212 = (135237975448393384089732807673070931796155070897373482995 * 10 ^ 70 + 2771121015267995201731479816152941181727687175157838833515381220057913) * 10 ^ 70 + 3831374681214947810475547108862180699116294798463370040901755860732301

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_213 : Polynomial.coeff recurrence4B2A4 213 = (58363059668905961195141815345410933520774792965796737690 * 10 ^ 70 + 319221287156673241900268112076183765494747342983056384099121483832055) * 10 ^ 70 + 1087064414410350376081276182893033723387073296503845873970104579059426

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_214 : Polynomial.coeff recurrence4B2A4 214 = -((100230966719520844956904052787434043681570274472320763171 * 10 ^ 70 + 4567705575063618631546313997376905138232537005036940419591735473655649) * 10 ^ 70 + 3799409708092660139034168495977529646964237252803012098315747002550510)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_215 : Polynomial.coeff recurrence4B2A4 215 = (88302140807613370598344718788905848964774491282685754875 * 10 ^ 70 + 3836386264840991010756339412243384317862846557908216667494517650531304) * 10 ^ 70 + 9284624594515893853865154185886294325368310489170903168841103870941525