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_277 : Polynomial.coeff recurrence4B2A4 277 = (17895263502851563503590368469691 * 10 ^ 70 + 4107236141892483684634950739574094755187449619081849020195242166816233) * 10 ^ 70 + 7080786296059333347496988999770307022996396922201786824327262515269645

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_278 : Polynomial.coeff recurrence4B2A4 278 = -((6119163007893538555947812174575 * 10 ^ 70 + 6620307414408691161024575253402574982230146629192735590526650040654982) * 10 ^ 70 + 7686427043987843255027039347731910094566386705846184216555435271015727)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_279 : Polynomial.coeff recurrence4B2A4 279 = (1977819197030521113939928910923 * 10 ^ 70 + 6180488525223890270049624099456813632110815090416572748230859117385100) * 10 ^ 70 + 2266413003429704977959586767081063418067319584804412335207833624199227

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_280 : Polynomial.coeff recurrence4B2A4 280 = -((597710087861672253939152566001 * 10 ^ 70 + 2197122061063567169393380762255555991524126897561501784186620427794597) * 10 ^ 70 + 7388882536720210024252847061045017699507859699861109940071608136900462)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_281 : Polynomial.coeff recurrence4B2A4 281 = (166001841842094956996534480613 * 10 ^ 70 + 2274474153146152486712595199327278568338878371796678246616709571802825) * 10 ^ 70 + 7318873289334185706435222299174580516936668295888385042830656552494488

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_282 : Polynomial.coeff recurrence4B2A4 282 = -((41069538245658022709410643154 * 10 ^ 70 + 850673477731790083080659625585991494456278464015077727166130714450594) * 10 ^ 70 + 1619181049473708710425391754789575413319316511632814450494092999359151)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_283 : Polynomial.coeff recurrence4B2A4 283 = (8432613365932767513106312800 * 10 ^ 70 + 1994697612452804045380129709063298165350921845589238440111525559986453) * 10 ^ 70 + 2221136471184089074081141327561604821141857246826649298888377596136346

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_284 : Polynomial.coeff recurrence4B2A4 284 = -((1111660795608050353613930905 * 10 ^ 70 + 1652658570591181184369357911743065196465053188745181603801429214732521) * 10 ^ 70 + 225027593871477604359591760654856755431989711599025057416479510430947)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_285 : Polynomial.coeff recurrence4B2A4 285 = -((109535104403255444193538560 * 10 ^ 70 + 3066418591635153592237989900705121525065531896936780112196666042573668) * 10 ^ 70 + 9625830102648819289777793526636479303907987376192520840945931290564356)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_286 : Polynomial.coeff recurrence4B2A4 286 = (151727232633205517020836761 * 10 ^ 70 + 1778613894082890417857312488627972309657167201835576322183873725423243) * 10 ^ 70 + 5012458822367279463251046422994328701571374216992268240460088275178428

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_287 : Polynomial.coeff recurrence4B2A4 287 = -((72001580661553729723264021 * 10 ^ 70 + 6046437145264973829584507755345327574375604937275535583102552622979915) * 10 ^ 70 + 2495683532124488515275750444816070185500417193361718148082447536811815)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_288 : Polynomial.coeff recurrence4B2A4 288 = (25916966337025013303459252 * 10 ^ 70 + 5134644533164500716674599340782072128812017905516054869394700642629532) * 10 ^ 70 + 7233563117596361227968538927767232639982698630674349439583890733957501

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_289 : Polynomial.coeff recurrence4B2A4 289 = -((7955689825198669725878092 * 10 ^ 70 + 7269871759943304643246355806809217100028759376786430878903249707698819) * 10 ^ 70 + 4456812668708928194283869792860459539250556042714694657376736256930070)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_290 : Polynomial.coeff recurrence4B2A4 290 = (2164267495353398145022534 * 10 ^ 70 + 9465932894208392475684608464100868894727941525786500480179406775422454) * 10 ^ 70 + 9544534689231847126822311774374235699433244015897842015753037655388850

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_291 : Polynomial.coeff recurrence4B2A4 291 = -((529469390948379761734777 * 10 ^ 70 + 9537655464016269778501691867948052711075521474066922466075475379331677) * 10 ^ 70 + 4155974215357293687394696671667440514632665257811412074344611303484932)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_292 : Polynomial.coeff recurrence4B2A4 292 = (116900770439539526389351 * 10 ^ 70 + 7122897551348849473254573741384129384444968357559809345472193200341596) * 10 ^ 70 + 3396286374561535237045813113704300237305130483266665969992243665125095

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_293 : Polynomial.coeff recurrence4B2A4 293 = -((23194210933135697163529 * 10 ^ 70 + 2655341763068558022071703453438005412753589993614605377359309374082509) * 10 ^ 70 + 7654999801745979943319782633065868933003230036747973578440664256194536)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_294 : Polynomial.coeff recurrence4B2A4 294 = (4081058085983550965374 * 10 ^ 70 + 4723361565200098674581433896051191147527991081807166457987146612680066) * 10 ^ 70 + 6622293800964453278148097862192073979559418334406823800702209898785797

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_295 : Polynomial.coeff recurrence4B2A4 295 = -((618537153695629182024 * 10 ^ 70 + 7697823931425654802995336133984763432460133847064770322902620044885898) * 10 ^ 70 + 6503874228054358046607396853387572419141115443696113676800067864534713)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_296 : Polynomial.coeff recurrence4B2A4 296 = (75273038020124357691 * 10 ^ 70 + 9739129796234781985882682553007662504178467405215395901283186317281732) * 10 ^ 70 + 4746104581082236390313069337907143327116898787914725559162127650071971

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_297 : Polynomial.coeff recurrence4B2A4 297 = -((5695300635668121693 * 10 ^ 70 + 2164437430996808958979075318043214175905865377030944173850282160331442) * 10 ^ 70 + 7091476843598818538515596470966008100613091466814792659075074950681361)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_298 : Polynomial.coeff recurrence4B2A4 298 = -((297763483305709540 * 10 ^ 70 + 8218646234961931531120640341910757240651110650826371901378612880036055) * 10 ^ 70 + 6213601133011903180866509188207256999996741503476152063368557726040607)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_299 : Polynomial.coeff recurrence4B2A4 299 = (220338644437793786 * 10 ^ 70 + 234810854319186366291866155050595307764458244259547774997550577789505) * 10 ^ 70 + 2294953256170715347431820952359353951226160264048864293391539462408611

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_300 : Polynomial.coeff recurrence4B2A4 300 = -((51650307588158803 * 10 ^ 70 + 3918663274460913693104150357967389767550027087859575284078450382635346) * 10 ^ 70 + 7490481737847919306221874337373185644304494313510952702425411965216692)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_301 : Polynomial.coeff recurrence4B2A4 301 = (8438674339922750 * 10 ^ 70 + 2630290364904141406247901376920491968191700264131280996851107726709873) * 10 ^ 70 + 2008688527093027595535438592065510400203119055334784292705883911976857

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_302 : Polynomial.coeff recurrence4B2A4 302 = -((1030619730505232 * 10 ^ 70 + 4510757442809382763041549264570377932847411509755392982254167269824403) * 10 ^ 70 + 1159414227965208878944948314437588959073379938364852235277466054003487)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_303 : Polynomial.coeff recurrence4B2A4 303 = (85293026545254 * 10 ^ 70 + 9154241651685360534725110954919943219928944191914063700508102039215047) * 10 ^ 70 + 6030162249600181681180170030255399168581890523177014747018164544501421

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_304 : Polynomial.coeff recurrence4B2A4 304 = -((1677164784925 * 10 ^ 70 + 5673385474657361967506116175893985231289327103368584933510183847424147) * 10 ^ 70 + 854009648691998418146252842145118905251937973052132399528418779452018)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_305 : Polynomial.coeff recurrence4B2A4 305 = -((921683278699 * 10 ^ 70 + 627717878797486511412995425768277885170698726154758447054452406059263) * 10 ^ 70 + 3700621659779002340418457917783089368318585833281203534523836055013100)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_306 : Polynomial.coeff recurrence4B2A4 306 = (200259054003 * 10 ^ 70 + 5728549342702557780116451776566463570891940108140522935124125861395652) * 10 ^ 70 + 8532097847364135726018637697700337697299687246148850632748879495407986

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_307 : Polynomial.coeff recurrence4B2A4 307 = -((25184851815 * 10 ^ 70 + 2131314677188985064630284568334177328375882026443802895239214342895555) * 10 ^ 70 + 5335832297050207791934706209633174971622683556324339261172390645407802)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_308 : Polynomial.coeff recurrence4B2A4 308 = (2127241998 * 10 ^ 70 + 8344873470183831537927098341333092399297667481784624307640334907319761) * 10 ^ 70 + 6639274826067595139250143026751811312692733633205013832876143160596256

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_309 : Polynomial.coeff recurrence4B2A4 309 = -((99870731 * 10 ^ 70 + 6065541556276123292453106569354673157287751487559167142677980084908823) * 10 ^ 70 + 6238311253747384022434219359674578635380273703781364746475393004125374)