Recurrence 4 lookup certificate: B3A3 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.recurrence4B3A3_coeff_0 : Polynomial.coeff recurrence4B3A3 0 = -339893486487797897668608

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_1 : Polynomial.coeff recurrence4B3A3 1 = 1825597917337870660811191680

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_2 : Polynomial.coeff recurrence4B3A3 2 = -428971828641491358868229619936

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_3 : Polynomial.coeff recurrence4B3A3 3 = -8304046254995357982452078793427368

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_4 : Polynomial.coeff recurrence4B3A3 4 = 16110170556877509886238473929896988244

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_5 : Polynomial.coeff recurrence4B3A3 5 = -12232043466069130236830010935964608014860

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_6 : Polynomial.coeff recurrence4B3A3 6 = 4013091064938287720635270187195559299551964

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_7 : Polynomial.coeff recurrence4B3A3 7 = -1004509553318186273598034840445955988155365630

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_8 : Polynomial.coeff recurrence4B3A3 8 = 508567231109865387474176571215239035071837146860

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_9 : Polynomial.coeff recurrence4B3A3 9 = -148766500421212944821417185561648292786870718559324

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_10 : Polynomial.coeff recurrence4B3A3 10 = -46788981881717499994111611801987570896988486471569876

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_11 : Polynomial.coeff recurrence4B3A3 11 = 53806298055300082749085579245498452721001790792795811782

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_12 : Polynomial.coeff recurrence4B3A3 12 = -19864362097378961804085083226824600669648176867464486241871

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_13 : Polynomial.coeff recurrence4B3A3 13 = 3684292248073798700160870639943129724937394206549460824124188

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_14 : Polynomial.coeff recurrence4B3A3 14 = -206101096070203844720954009061904692097185843474164462720780188

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_15 : Polynomial.coeff recurrence4B3A3 15 = -38708747060025426283416732420023880875701969472093227998187413260

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_16 : Polynomial.coeff recurrence4B3A3 16 = -12817326555566654700020596657196955975183537839626458707146858649239

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_17 : Polynomial.coeff recurrence4B3A3 17 = 1 * 10 ^ 70 + 6436338359175499245291898743685808142276523380882100600223687187803631

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_18 : Polynomial.coeff recurrence4B3A3 18 = -(740 * 10 ^ 70 + 1404419203359801025944445845876693558854586739267326448394541450134259)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_19 : Polynomial.coeff recurrence4B3A3 19 = 229483 * 10 ^ 70 + 8638257149463820403533703024984404055695768497160466246370501601187369

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_20 : Polynomial.coeff recurrence4B3A3 20 = -(56051980 * 10 ^ 70 + 3064764848747991794701006827816847812081990325212289081647976242310387)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_21 : Polynomial.coeff recurrence4B3A3 21 = 11312014376 * 10 ^ 70 + 9713898609685977266897378539084934359507059244683511750555921031767797

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_22 : Polynomial.coeff recurrence4B3A3 22 = -(1922132765170 * 10 ^ 70 + 4629697237615818701088022261279647062666482053078008978695137398770652)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_23 : Polynomial.coeff recurrence4B3A3 23 = 276337739101953 * 10 ^ 70 + 9998370066976269159901281687263113327307011181952800952160926467034200

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_24 : Polynomial.coeff recurrence4B3A3 24 = -(33372170385659370 * 10 ^ 70 + 3295373201171733102534573815868293576968915207033724120925563638600323)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_25 : Polynomial.coeff recurrence4B3A3 25 = 3293034004509070802 * 10 ^ 70 + 4210231992721438150666387158651586016894413509173669390675447332761107

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_26 : Polynomial.coeff recurrence4B3A3 26 = -(243466141569319016743 * 10 ^ 70 + 8784552891812520067426851079685536411488351034293485484845992347098979)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_27 : Polynomial.coeff recurrence4B3A3 27 = 8646559293535951821884 * 10 ^ 70 + 464069596878917828745353409405834900503956539802854220007478596408312

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_28 : Polynomial.coeff recurrence4B3A3 28 = 1022884975030964398433120 * 10 ^ 70 + 8842054038792769810563289663388453407497501806452195973829481291566869

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_29 : Polynomial.coeff recurrence4B3A3 29 = -(271071020408217754800003217 * 10 ^ 70 + 9127374023430696347367639307457872690749843061117617301899843953308306)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_30 : Polynomial.coeff recurrence4B3A3 30 = 37862286719991861070720901821 * 10 ^ 70 + 1430414742995767647574189213577523764762194525620538614666605446418356

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_31 : Polynomial.coeff recurrence4B3A3 31 = -(4094260291567617857192654575261 * 10 ^ 70 + 6241264850664197747007141128979016513846574808979705419475324793285518)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_32 : Polynomial.coeff recurrence4B3A3 32 = 374469081023399615767262547060130 * 10 ^ 70 + 7384000643957351658440270476047722034297888633828180619354059037501981

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_33 : Polynomial.coeff recurrence4B3A3 33 = -(30036910243735193579831158779297681 * 10 ^ 70 + 4834845534781499384104131877781396973427785551723323424526825173555640)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_34 : Polynomial.coeff recurrence4B3A3 34 = 2153748010942077515608707688450643263 * 10 ^ 70 + 2119770870370888096687370791008992035768066953107719841149841788608546

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_35 : Polynomial.coeff recurrence4B3A3 35 = -(139681341824669807628495389001914896915 * 10 ^ 70 + 3487556254190649319835934045401330923138795335023245683854924517691068)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_36 : Polynomial.coeff recurrence4B3A3 36 = 8259621441667998529800525234955332986834 * 10 ^ 70 + 1224616453729624294382642622449835395380451901312715530086770995433797

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_37 : Polynomial.coeff recurrence4B3A3 37 = -(447920126842412236640965124535622494666414 * 10 ^ 70 + 5168094619843127903908688897151655503709488914556068541975405664792195)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_38 : Polynomial.coeff recurrence4B3A3 38 = 22377608959096842504845758454735466145875894 * 10 ^ 70 + 6595622940133106600930173159013975236347897587123263333365478495398931

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_39 : Polynomial.coeff recurrence4B3A3 39 = -(1033608108528410226861771924168300212997574232 * 10 ^ 70 + 7422089703716064309301789163098697314628377307306236585297692505932858)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_40 : Polynomial.coeff recurrence4B3A3 40 = 44268522273574152038026611622561887251667173486 * 10 ^ 70 + 9983210126119055071425204805769752814032090837733968547021517839470308

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_41 : Polynomial.coeff recurrence4B3A3 41 = -(1762278834682488283502593953570581200635745320318 * 10 ^ 70 + 6638082509726938122664258257604007894653287191304739518390113359502866)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_42 : Polynomial.coeff recurrence4B3A3 42 = 65335885975297456139132031829237341768765715325058 * 10 ^ 70 + 9775445574501668048367401931616534372053301862479746998713022819748002

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_43 : Polynomial.coeff recurrence4B3A3 43 = -(2259521673548384759309378657482213345525809258151853 * 10 ^ 70 + 674728566600575779139625275716113006639522641847597708550711673601340)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_44 : Polynomial.coeff recurrence4B3A3 44 = 72978817553803847586304405341535212565814854987075869 * 10 ^ 70 + 5416847698066398048046461856242593618439691767231126361511184376759560

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_45 : Polynomial.coeff recurrence4B3A3 45 = -(2203180271460153608491348161663958045725411464035920510 * 10 ^ 70 + 8663203384607014935180423439653836458657799553403220062039852688952462)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_46 : Polynomial.coeff recurrence4B3A3 46 = 62192472452716796956771875008008280911303545354219807833 * 10 ^ 70 + 4362365926804725310701005702930718440178099930765315063227518736178477

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_47 : Polynomial.coeff recurrence4B3A3 47 = -(1641264421027755436489000385491040992710700417821160288690 * 10 ^ 70 + 4526983467076213032753377956269006862867375153733553445068812864706748)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_48 : Polynomial.coeff recurrence4B3A3 48 = 40454184241002773841827111072718483504863614107766075279388 * 10 ^ 70 + 3701934276718407017285057995074659772603437975330671784758996443519725

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_49 : Polynomial.coeff recurrence4B3A3 49 = -(929413988378644390881343422008283456386207783164926943522655 * 10 ^ 70 + 8673566953407694740029914998974794600934823869154569104996708902203738)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_50 : Polynomial.coeff recurrence4B3A3 50 = 19828448308111374919460774355873570682861176115785263793627607 * 10 ^ 70 + 5876956278052517069883169597913259083167426081860191134826543295679120

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_51 : Polynomial.coeff recurrence4B3A3 51 = -(390215020885068912361692205755326920286726471627880469152075673 * 10 ^ 70 + 3722251717655952821335107721192045960760309151328063800783923567251469)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_52 : Polynomial.coeff recurrence4B3A3 52 = 6997508239921951688166016265739440892621805690661067891979732476 * 10 ^ 70 + 6435149431254835441461114025883450550709836943351769700546458295260295

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_53 : Polynomial.coeff recurrence4B3A3 53 = -(111584674327240022359780636054690727758336992834209644928888429792 * 10 ^ 70 + 5586879587479609220613015154418361940388066010402740085123461148133059)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_54 : Polynomial.coeff recurrence4B3A3 54 = 1493473036075845387278903759116278554825653838817025309419124491298 * 10 ^ 70 + 7576475243541352591688407459045282104197504011184917815896611442987047

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_55 : Polynomial.coeff recurrence4B3A3 55 = -(13760438480243305636077905017007203114259886454834370587061412744682 * 10 ^ 70 + 1341699655583396370728289023084410330455136557364881911049352719087762)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_56 : Polynomial.coeff recurrence4B3A3 56 = -(30009822521924179343290761159579959703207852602143724133785935201409 * 10 ^ 70 + 457229427311396065712841993461959825541439737081318110876100088451179)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_57 : Polynomial.coeff recurrence4B3A3 57 = 5632660231834099540296994226647102559460383609122039552804040658463614 * 10 ^ 70 + 3188788472254097514733393978611153872560459492404180030047580066109727

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_58 : Polynomial.coeff recurrence4B3A3 58 = -((18 * 10 ^ 70 + 2804250676601797025102397728010598459190630868080429123226030288330328) * 10 ^ 70 + 8240684846897248608212290320919220834729855643618166379947606849721669)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_59 : Polynomial.coeff recurrence4B3A3 59 = (439 * 10 ^ 70 + 8726739092625690278112197164110740315862241795000895366094903440426216) * 10 ^ 70 + 3940872592659571559274032878837243190822962719082878507052528231209692

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_60 : Polynomial.coeff recurrence4B3A3 60 = -((9091 * 10 ^ 70 + 5728615741974364059839821524438108472348953375754599141950916430734905) * 10 ^ 70 + 8046740695946100941925407447512525422892961865035814243543309403141143)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_61 : Polynomial.coeff recurrence4B3A3 61 = (169537 * 10 ^ 70 + 2258604907774669750728237001061793455155028549208103653319504367985307) * 10 ^ 70 + 5287153528121462408608926130966528357757270975844483255418875610440770

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_62 : Polynomial.coeff recurrence4B3A3 62 = -((2918229 * 10 ^ 70 + 8718768796702721558080919175190388367733717409543398898792326745315104) * 10 ^ 70 + 4939470144730006839973208188368548563466203088338528734727281110775248)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_63 : Polynomial.coeff recurrence4B3A3 63 = (46957863 * 10 ^ 70 + 6173636329066750729916026959639817422955287170585887336394155641370896) * 10 ^ 70 + 9025598810589173231441188665374841281949235497536803422671985746173843

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_64 : Polynomial.coeff recurrence4B3A3 64 = -((711977717 * 10 ^ 70 + 4864434600567074947421153488941938594840567689569331879185630746671601) * 10 ^ 70 + 4213146616553389970647564530370682423019190716989547554322071329382565)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_65 : Polynomial.coeff recurrence4B3A3 65 = (10226397996 * 10 ^ 70 + 7232560717645733273655295425067242350725337624902010514746174344566321) * 10 ^ 70 + 4418028736343340591675887045181599279858910749386493938965502575861109

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_66 : Polynomial.coeff recurrence4B3A3 66 = -((139688121142 * 10 ^ 70 + 6454141061733320843151146742224556598565751079342306327561413513976403) * 10 ^ 70 + 6984299758782707648163920612133974148512071554724080107446257478218927)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_67 : Polynomial.coeff recurrence4B3A3 67 = (1819926775426 * 10 ^ 70 + 2630756600830911786684206556108652995314893921189704515671291830548435) * 10 ^ 70 + 633333401103282697319145890415568975349285472865735526589601876235938

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_68 : Polynomial.coeff recurrence4B3A3 68 = -((22668104579955 * 10 ^ 70 + 8979176612535730717019203338609739033697805079849738400186701961501712) * 10 ^ 70 + 4866708458478269470739982843949584364082780847062544335195741269654851)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_69 : Polynomial.coeff recurrence4B3A3 69 = (270437735351151 * 10 ^ 70 + 2100649274607885890932532812851424041037471662915499171457016265538110) * 10 ^ 70 + 9351258897610409050666836039218933502176163168266893379215703725539578

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_70 : Polynomial.coeff recurrence4B3A3 70 = -((3095288693073230 * 10 ^ 70 + 4535791006227763142592521584032953188591803673225762731116734853639721) * 10 ^ 70 + 7153100620785850281324440839983770066981684756746818467052952320700065)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_71 : Polynomial.coeff recurrence4B3A3 71 = (34033714745175886 * 10 ^ 70 + 8009071934162496013488725338851588770034651602925618962737841741492889) * 10 ^ 70 + 8992728854396385281720276085434533130994079977878256759562715392733347

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_72 : Polynomial.coeff recurrence4B3A3 72 = -((359922865517423387 * 10 ^ 70 + 5743105282844334338279277728536341923503959474265505297206452909517036) * 10 ^ 70 + 5370378107582127313590781618514424706429000542949040406685015870257134)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_73 : Polynomial.coeff recurrence4B3A3 73 = (3664886261391725512 * 10 ^ 70 + 986474725999863402963408364190045659993378065126550312256234017109289) * 10 ^ 70 + 1883303637870129035933913379167854534994999835154854970710375861528506

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_74 : Polynomial.coeff recurrence4B3A3 74 = -((35964582682354608485 * 10 ^ 70 + 478347578263236163058212896971889432248148753970583880874469346701988) * 10 ^ 70 + 2009035560737894538543459152612878132169468714672600551640477184837667)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_75 : Polynomial.coeff recurrence4B3A3 75 = (340429839933200307427 * 10 ^ 70 + 9371516537509349574865392009480536539256179437514579179586880375458722) * 10 ^ 70 + 5757107310907432650276965349220779435935780518894643314790870881583795

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_76 : Polynomial.coeff recurrence4B3A3 76 = -((3110724762638332471189 * 10 ^ 70 + 7649052861654001504350246238193433292562690903043502896017526035138067) * 10 ^ 70 + 3631817816230040671153539401603248264049638867092046770243619225725537)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_77 : Polynomial.coeff recurrence4B3A3 77 = (27459582338537658192000 * 10 ^ 70 + 9429536525349103268151715367818550046465865886091230089971852912753417) * 10 ^ 70 + 3705797830755623696152295955870601998563259823394647996878064157787712

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_78 : Polynomial.coeff recurrence4B3A3 78 = -((234325336854024581191418 * 10 ^ 70 + 64211546229547052390051321613694437509303736820424504211777300929114) * 10 ^ 70 + 5340903922428696297111965387256692087825796434041521666991821686969425)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_79 : Polynomial.coeff recurrence4B3A3 79 = (1934251023385424921728337 * 10 ^ 70 + 9404712891952630104588433361849940082383716524250063030343702389801357) * 10 ^ 70 + 7075564992706713220163051944301397551759189622901465180417268446279386