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_0 : Polynomial.coeff recurrence4B2A4 0 = -250723319715491387426816

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_1 : Polynomial.coeff recurrence4B2A4 1 = 1864476666001642366720473472

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_2 : Polynomial.coeff recurrence4B2A4 2 = -3569686250833381937635207519792

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_3 : Polynomial.coeff recurrence4B2A4 3 = -537769351529052494138995328763480

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_4 : Polynomial.coeff recurrence4B2A4 4 = 7110500776170259367016631016540540992

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_5 : Polynomial.coeff recurrence4B2A4 5 = -6255076918588020364139369479897699620168

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_6 : Polynomial.coeff recurrence4B2A4 6 = 2426614741576056851443027134418781854258748

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_7 : Polynomial.coeff recurrence4B2A4 7 = -1429206354234730129809942456143335411719639650

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_8 : Polynomial.coeff recurrence4B2A4 8 = 1108097447283585225396256906314174821245125269500

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_9 : Polynomial.coeff recurrence4B2A4 9 = -367284853420002635620590002294630101260396320550060

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_10 : Polynomial.coeff recurrence4B2A4 10 = -76101461934266160011199120718902905397684798944098844

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_11 : Polynomial.coeff recurrence4B2A4 11 = 115047717663466810038290548993233867418835761025599185901

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_12 : Polynomial.coeff recurrence4B2A4 12 = -47935450340062161529473061999253649111401592517910788545441

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_13 : Polynomial.coeff recurrence4B2A4 13 = 10858453469900909626777224769539580197096975507937383437871215

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_14 : Polynomial.coeff recurrence4B2A4 14 = -1309508251955955536567967993760896612998366449886922540725633641

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_15 : Polynomial.coeff recurrence4B2A4 15 = 44593500571543711823180292973405911629003831366358303727936181411

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_16 : Polynomial.coeff recurrence4B2A4 16 = -7534778521895817897236503938612743142629432083149724370879903853430

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_17 : Polynomial.coeff recurrence4B2A4 17 = 1 * 10 ^ 70 + 2931840542876155429120004319988556378002835211271618891098430103559398

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_18 : Polynomial.coeff recurrence4B2A4 18 = -(620 * 10 ^ 70 + 9868794591161146589212683876744790941595464994046548633450616915458329)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_19 : Polynomial.coeff recurrence4B2A4 19 = 190967 * 10 ^ 70 + 3602457576660064891718325780827661561360025554877397162291124109938802

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_20 : Polynomial.coeff recurrence4B2A4 20 = -(45245227 * 10 ^ 70 + 9528046842746793724200036755756903260200582827460270210908364962513830)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_21 : Polynomial.coeff recurrence4B2A4 21 = 8798099602 * 10 ^ 70 + 5108406791725778420033506901305377648246280487961495031340756493648127

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_22 : Polynomial.coeff recurrence4B2A4 22 = -(1434363610433 * 10 ^ 70 + 2818543423062394532265784381274917710717369779989952261798564181877401)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_23 : Polynomial.coeff recurrence4B2A4 23 = 196201738880345 * 10 ^ 70 + 1336192959744305434260814260398491071502211239014964159580860025263713

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_24 : Polynomial.coeff recurrence4B2A4 24 = -(22101978243623940 * 10 ^ 70 + 3711239482417576976846035089494679750905368473545327617912561059765089)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_25 : Polynomial.coeff recurrence4B2A4 25 = 1930247162433618915 * 10 ^ 70 + 8314899743149801209544888052664252079616528154124588988226503017556975

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_26 : Polynomial.coeff recurrence4B2A4 26 = -(102273239584682030343 * 10 ^ 70 + 7195562905365162254567820512604782165375282270746959264777161078576959)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_27 : Polynomial.coeff recurrence4B2A4 27 = -(3688589242541473888897 * 10 ^ 70 + 1521115112866276766230510926927930215332762426212443004414590823901956)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_28 : Polynomial.coeff recurrence4B2A4 28 = 1891438540485751878524048 * 10 ^ 70 + 3841040467826977263095485383797140635580344346117786956155156351090480

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_29 : Polynomial.coeff recurrence4B2A4 29 = -(313349742802975424412566826 * 10 ^ 70 + 5052266482493022556497174788611252999561341378310728359995198466518984)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_30 : Polynomial.coeff recurrence4B2A4 30 = 38032869794394728502892794556 * 10 ^ 70 + 6975228124433035109273209765377988395436469141799693136265136954738208

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_31 : Polynomial.coeff recurrence4B2A4 31 = -(3830920177060954553472859923315 * 10 ^ 70 + 7794589174345229489571445472556894822967480882174797929354313283342614)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_32 : Polynomial.coeff recurrence4B2A4 32 = 335176221239636550260582138982033 * 10 ^ 70 + 1727915931643038232874671757414051397213510253447597153237390376838761

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_33 : Polynomial.coeff recurrence4B2A4 33 = -(26058008456666328377531551198934977 * 10 ^ 70 + 835164172168132872890890642908370054662836022167422865620505311353128)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_34 : Polynomial.coeff recurrence4B2A4 34 = 1824587931475987246517482406543829509 * 10 ^ 70 + 7994913091345693882717777305698288162344742034477155457786326802923592

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_35 : Polynomial.coeff recurrence4B2A4 35 = -(116102061801450769327505534598369915275 * 10 ^ 70 + 160393736685144102695732050011053778497514264163413231166773176916325)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_36 : Polynomial.coeff recurrence4B2A4 36 = 6757274863569242899901223575007104106778 * 10 ^ 70 + 5230622578803450361782347149354198104192550192014982105598574798739403

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_37 : Polynomial.coeff recurrence4B2A4 37 = -(361489671500779623949241871901688374042645 * 10 ^ 70 + 6145410294920790161926729669056394055882866240322836509084515797268299)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_38 : Polynomial.coeff recurrence4B2A4 38 = 17844533077206598135177825280157258053272278 * 10 ^ 70 + 3483975743737091277694042621958760853824071776665058027947686326364707

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_39 : Polynomial.coeff recurrence4B2A4 39 = -(815410192045601857329690609626624543107840079 * 10 ^ 70 + 8019712882274404459773908056683748560621633364668792710951274233602165)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_40 : Polynomial.coeff recurrence4B2A4 40 = 34581649834613834706154213513051833802143971029 * 10 ^ 70 + 5563113758839669763298520363708457754078113652635150039840424841787369

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_41 : Polynomial.coeff recurrence4B2A4 41 = -(1364132481751366218506370342623966742910326419036 * 10 ^ 70 + 8291666306375401926552837180754796646834310531483918748110440996728127)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_42 : Polynomial.coeff recurrence4B2A4 42 = 50139786830717165234481993537192573756989000701755 * 10 ^ 70 + 5860894219540593922520619996839864935027896252448285402810469921394168

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_43 : Polynomial.coeff recurrence4B2A4 43 = -(1719647366949173555922279131663302846703795437395982 * 10 ^ 70 + 4983987955419099497562759137933392573998595502982875718367077614705412)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_44 : Polynomial.coeff recurrence4B2A4 44 = 55091336076499940535950799302496406282350606211376243 * 10 ^ 70 + 9644294987060014234873775479272338364575642808309506702176605917104766

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_45 : Polynomial.coeff recurrence4B2A4 45 = -(1649660615427960993619303902199393685729069414332227573 * 10 ^ 70 + 8747759706679811943133505370081371223950080021271497264211201496268104)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_46 : Polynomial.coeff recurrence4B2A4 46 = 46179005053010967834304794787679298949438002245064988646 * 10 ^ 70 + 9016416409415359169806771390770323119107659940992196711236876348218261

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_47 : Polynomial.coeff recurrence4B2A4 47 = -(1207911579845617098914637267244582409496049161481667872149 * 10 ^ 70 + 4374342295368943178675546006275406435068899767358999560911562941842509)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_48 : Polynomial.coeff recurrence4B2A4 48 = 29484537361086172062840421545232316705368222161987518312081 * 10 ^ 70 + 1355423591525122042763615180442712845628480206561065825956179119973403

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_49 : Polynomial.coeff recurrence4B2A4 49 = -(669870014335153566657956168284240777409960993473532198423506 * 10 ^ 70 + 6063333155369493472770390065953224250478432166542600499302858905679164)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_50 : Polynomial.coeff recurrence4B2A4 50 = 14098919823713827331988710677223377203117299548906422282473868 * 10 ^ 70 + 1973779492114580918629666551409746811667774898516509446905508746702131

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_51 : Polynomial.coeff recurrence4B2A4 51 = -(272604275292922453663082550594846516807927406434222617201151446 * 10 ^ 70 + 3822590635544137972083899571650446421306161679186412641456593497819466)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_52 : Polynomial.coeff recurrence4B2A4 52 = 4766168366112645997205443657894495973700912195956391946132896020 * 10 ^ 70 + 4347729252182763621677326644942180060006131899591051781131084212393418

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_53 : Polynomial.coeff recurrence4B2A4 53 = -(72886712770076133340003014788850916717279135419352349856251864661 * 10 ^ 70 + 2118987223553884605049295444319971629531302428947011105568320096870936)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_54 : Polynomial.coeff recurrence4B2A4 54 = 893089505348588657766325659890121999822154543174709813074933336751 * 10 ^ 70 + 8016689219780435242003441578979125492930097816357185196442673382892139

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_55 : Polynomial.coeff recurrence4B2A4 55 = -(5828690320607545914677535266063768582473896497067574483122986275603 * 10 ^ 70 + 7746714333571799355588583746839015181140182604099254919165873565518895)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_56 : Polynomial.coeff recurrence4B2A4 56 = -(106425874410547567304650137411090801444563854751198862184650292245516 * 10 ^ 70 + 5110028472345523895626313505246741239210441893484787219002717148378069)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_57 : Polynomial.coeff recurrence4B2A4 57 = 5708569714897884256299516041182764067178085663130427592888206656298262 * 10 ^ 70 + 3513512808601089405251757600983516551823478636807400288929491796431564

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_58 : Polynomial.coeff recurrence4B2A4 58 = -((16 * 10 ^ 70 + 1994504717074827271462534044768612069529663717476117641010654170573510) * 10 ^ 70 + 6276699437428076407249898224800140273971565628714718474931406145081317)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_59 : Polynomial.coeff recurrence4B2A4 59 = (369 * 10 ^ 70 + 5633506073163803676718282519122429518213570295214890863417699624546177) * 10 ^ 70 + 5074755132377149557041531043250438331773798658922901963900415499233597

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_60 : Polynomial.coeff recurrence4B2A4 60 = -((7419 * 10 ^ 70 + 7519711765764923126345049743407058146979415249648197750135159930836115) * 10 ^ 70 + 6932711319130301025848793265419770674029535649596390347073874921039908)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_61 : Polynomial.coeff recurrence4B2A4 61 = (135828 * 10 ^ 70 + 7671902381270864032731431903200379440119805001512413390216372235900877) * 10 ^ 70 + 4168623702866525572379980249394289502711242694795862975163822650999967

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_62 : Polynomial.coeff recurrence4B2A4 62 = -((2308050 * 10 ^ 70 + 662480434515538789246702155289011672666772591236862411492479517110010) * 10 ^ 70 + 4504677357643485408857640411590143111872940394362670942626164767307070)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_63 : Polynomial.coeff recurrence4B2A4 63 = (36785580 * 10 ^ 70 + 4349568630241084851922562399393573092690351461140052215447752900106597) * 10 ^ 70 + 4662668467213260964346459481174920843779578550460371510767195524022877

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_64 : Polynomial.coeff recurrence4B2A4 64 = -((553625837 * 10 ^ 70 + 8360501959337681302300643535554662918077134541495389771715425595986773) * 10 ^ 70 + 4992233518233178308542219230543567461106493620523313230067471577287040)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_65 : Polynomial.coeff recurrence4B2A4 65 = (7904974074 * 10 ^ 70 + 964546665283683188732163082323760947761069811261248134916837779493451) * 10 ^ 70 + 1022759438784291319100638705703176855901438041068103478385190998093450

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_66 : Polynomial.coeff recurrence4B2A4 66 = -((107456843140 * 10 ^ 70 + 556136117300599481187102325600155384359646889737839053763991178052105) * 10 ^ 70 + 312327671194276085501621521062868803987341306520912435718452870910981)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_67 : Polynomial.coeff recurrence4B2A4 67 = (1394372005831 * 10 ^ 70 + 4082666125214609263660323752911435137227605807213578776393480303040290) * 10 ^ 70 + 1612307059069892357332798211045881066752638638530201015218108020731695

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_68 : Polynomial.coeff recurrence4B2A4 68 = -((17308709769958 * 10 ^ 70 + 7692866883299494855826369592823454464770061350104636929468782778502280) * 10 ^ 70 + 388223011189122907651381165934667602346124092745199503506075915040067)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_69 : Polynomial.coeff recurrence4B2A4 69 = (205902016343702 * 10 ^ 70 + 7650230867409491377250231769963215465157414751158486660213220538292198) * 10 ^ 70 + 9856422267573584254178708381785651204228931057466777851484794542360526

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_70 : Polynomial.coeff recurrence4B2A4 70 = -((2350806667332144 * 10 ^ 70 + 5386899012672728179797678654354346031411431433887077745997638937039111) * 10 ^ 70 + 3404082349303508975178160190709550408302591410059350716326796704817494)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_71 : Polynomial.coeff recurrence4B2A4 71 = (25792646363158258 * 10 ^ 70 + 9563692466845701423667441986563663359133529633679905903663779080522575) * 10 ^ 70 + 9957266402841415700685943833124440304897401809174642977972954383930871

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_72 : Polynomial.coeff recurrence4B2A4 72 = -((272265083576200837 * 10 ^ 70 + 7912560667062170154675260078742605353202976916415067637399131038673515) * 10 ^ 70 + 7163017954831796916655058883085764230401238378193010709722698154424443)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_73 : Polynomial.coeff recurrence4B2A4 73 = (2767872038985009830 * 10 ^ 70 + 4656710763651960833072072116349000464629908424209655691127449917119848) * 10 ^ 70 + 1307736443296969719590827603681601349951569560503512976719464508459061

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_74 : Polynomial.coeff recurrence4B2A4 74 = -((27124149245619473066 * 10 ^ 70 + 5508554981453099885525952592300973626456479099952754603895257989918594) * 10 ^ 70 + 5566021405973902436832103895328699173931516561871458811152345982051885)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_75 : Polynomial.coeff recurrence4B2A4 75 = (256439680535666165277 * 10 ^ 70 + 9971029767839823482325081965345068449793066338935490014821968305228690) * 10 ^ 70 + 6283700213914539795680432615687752779690872683724674939162573669754657

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_76 : Polynomial.coeff recurrence4B2A4 76 = -((2340814635344036785646 * 10 ^ 70 + 172410479872762032857829831702901103940128886381690682205705986042241) * 10 ^ 70 + 7996346468976650616805902817040725392412593534714212090088688238847599)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_77 : Polynomial.coeff recurrence4B2A4 77 = (20644793774088341209445 * 10 ^ 70 + 8796744516896506333576965166203468672741814183479815918048861147498410) * 10 ^ 70 + 4833526728338318585475985465867371374784987499523109582760421185827664

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_78 : Polynomial.coeff recurrence4B2A4 78 = -((176036897693003460181251 * 10 ^ 70 + 3549906173519214618253864615327799991112186315364021928958523462621464) * 10 ^ 70 + 4795853324539117715654393315411936243295360039782589946767074716035300)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_79 : Polynomial.coeff recurrence4B2A4 79 = (1452165406992312482326819 * 10 ^ 70 + 9619556078438448622451093139183947194458234997794856189007821007250385) * 10 ^ 70 + 5336911156213634133574417501910386806803765542697139387218379308835240