Recurrence 4 lookup certificate: B3A4 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.recurrence4B3A4_coeff_0 : Polynomial.coeff recurrence4B3A4 0 = -17170333563205017326343168

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_1 : Polynomial.coeff recurrence4B3A4 1 = 63765286811474699076992674944

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_2 : Polynomial.coeff recurrence4B3A4 2 = -51558851730324849482796682197792

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_3 : Polynomial.coeff recurrence4B3A4 3 = -75682887295544516468778111016532136

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_4 : Polynomial.coeff recurrence4B3A4 4 = 169503547611494126153709633557401566284

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_5 : Polynomial.coeff recurrence4B3A4 5 = -110545608536465323112602061600564415166728

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_6 : Polynomial.coeff recurrence4B3A4 6 = 30391720998073691699717733756473548080821198

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_7 : Polynomial.coeff recurrence4B3A4 7 = -9262104637886248654636690882910874797137953054

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_8 : Polynomial.coeff recurrence4B3A4 8 = 5145575856698294529205511969328677367811025869980

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_9 : Polynomial.coeff recurrence4B3A4 9 = -1086046462413650888054133701416983597870976383994900

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_10 : Polynomial.coeff recurrence4B3A4 10 = -626600649901033956763947088477199642203949036411582270

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_11 : Polynomial.coeff recurrence4B3A4 11 = 514198754912965874274195752204557015896411457380322470971

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_12 : Polynomial.coeff recurrence4B3A4 12 = -170245807094603034138188199416580583734359065939032374569663

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_13 : Polynomial.coeff recurrence4B3A4 13 = 30935033518289031514104127673384094796758667528666789954565219

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_14 : Polynomial.coeff recurrence4B3A4 14 = -2622062958699295268566392295929843595782015088896367945335413019

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_15 : Polynomial.coeff recurrence4B3A4 15 = 2948582024453440676599997047928135638629698250642125473794668839

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_16 : Polynomial.coeff recurrence4B3A4 16 = -68530268170995041534988187931086504765669973835226124400684314243244

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_17 : Polynomial.coeff recurrence4B3A4 17 = 6 * 10 ^ 70 + 1002931404494411823583227494502255114532846138999548347733471659552715

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_18 : Polynomial.coeff recurrence4B3A4 18 = -(2408 * 10 ^ 70 + 1834275356176856670375706754654700974873630705651664880766817152090355)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_19 : Polynomial.coeff recurrence4B3A4 19 = 668003 * 10 ^ 70 + 3100365237488501639556065127333452195269520300088583822032477789463014

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_20 : Polynomial.coeff recurrence4B3A4 20 = -(147423907 * 10 ^ 70 + 2219909680397463209859047986731475926781373117813391762412974955647626)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_21 : Polynomial.coeff recurrence4B3A4 21 = 27062320657 * 10 ^ 70 + 1518789458551453282066098105151009392405662385050293109062143103849542

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_22 : Polynomial.coeff recurrence4B3A4 22 = -(4194195608754 * 10 ^ 70 + 1221167322610049029016789386730496850536211848162824960777672524318434)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_23 : Polynomial.coeff recurrence4B3A4 23 = 548500713518168 * 10 ^ 70 + 461194092393600195268921087289640960707561005926787805585484703806091

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_24 : Polynomial.coeff recurrence4B3A4 24 = -(59529386384730404 * 10 ^ 70 + 8728758346280526533414526710753425906921166890618442671909436852521305)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_25 : Polynomial.coeff recurrence4B3A4 25 = 5092116171534792667 * 10 ^ 70 + 1568043175578299590467719939764472607873989387564482408198907072297270

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_26 : Polynomial.coeff recurrence4B3A4 26 = -(283380160846016553060 * 10 ^ 70 + 5603905858643695775631297132244047214282361717208146166569701468523954)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_27 : Polynomial.coeff recurrence4B3A4 27 = -(3331046813802695265472 * 10 ^ 70 + 7629008268487652290252961928164585785044542866111086406000721923375628)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_28 : Polynomial.coeff recurrence4B3A4 28 = 3546246969183283327850324 * 10 ^ 70 + 3991675643711748510219912074308064193056029674625844172810868981078656

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_29 : Polynomial.coeff recurrence4B3A4 29 = -(595571730118155461468567904 * 10 ^ 70 + 1739621766949171952780314997481529698944353670032640190778803508658434)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_30 : Polynomial.coeff recurrence4B3A4 30 = 70757612577922893895446693135 * 10 ^ 70 + 7563266110419335394315068064873374648986734487172948687944901602555596

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_31 : Polynomial.coeff recurrence4B3A4 31 = -(6912653328665081957274875041917 * 10 ^ 70 + 3959126273426882982903848818683961051869177695950759645980819336406331)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_32 : Polynomial.coeff recurrence4B3A4 32 = 584624022135074751031264439738414 * 10 ^ 70 + 7219324874820497787158067345885579157904988081176490020932307358075662

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_33 : Polynomial.coeff recurrence4B3A4 33 = -(43874037860933431831248717406825486 * 10 ^ 70 + 5486017903424476004937673759585406965650844202142876299160484029534237)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_34 : Polynomial.coeff recurrence4B3A4 34 = 2963910064216881476950357323491138200 * 10 ^ 70 + 6430641651574506596721178817245415665030802146408736609995806752675673

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_35 : Polynomial.coeff recurrence4B3A4 35 = -(181937754015303410527269542639558718178 * 10 ^ 70 + 1836028794213912347083773384707439782783709731934123865659480615074017)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_36 : Polynomial.coeff recurrence4B3A4 36 = 10215915213600439366270322595190986243881 * 10 ^ 70 + 1991469047372949327619478921475545975063917068304174488144580720768729

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_37 : Polynomial.coeff recurrence4B3A4 37 = -(527365847793271567731341771763966848940532 * 10 ^ 70 + 7614608500999034617012475841845086211702114063820725244327904739003969)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_38 : Polynomial.coeff recurrence4B3A4 38 = 25127111427606667387433163851521921716320358 * 10 ^ 70 + 1903154542521475625540246735253770726115653092010327526007355907677114

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_39 : Polynomial.coeff recurrence4B3A4 39 = -(1108547341908187973571276171236303651934134748 * 10 ^ 70 + 4141197333678674989303728195461118405345633430584838054971700947002019)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_40 : Polynomial.coeff recurrence4B3A4 40 = 45402826512917426964002354106900213186420188613 * 10 ^ 70 + 8598407465738301604389048732712524000347777277561396753679056094547287

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_41 : Polynomial.coeff recurrence4B3A4 41 = -(1730066051280948636054755388538318068191254015382 * 10 ^ 70 + 7669725739740949522023085017042111380765774113850576079003713088899872)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_42 : Polynomial.coeff recurrence4B3A4 42 = 61440186868523226076847677074433156749983792476551 * 10 ^ 70 + 5236230984800485691547342265054235471144111913457935732645203011638376

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_43 : Polynomial.coeff recurrence4B3A4 43 = -(2036322918751745348648828387025486323298850604107719 * 10 ^ 70 + 6691068851520591657372871392985630233510231512384377164541717684802739)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_44 : Polynomial.coeff recurrence4B3A4 44 = 63047988248638330402200374744283793246456029282308472 * 10 ^ 70 + 5871217202603437280566052153487678772603245394091316072123106889109522

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_45 : Polynomial.coeff recurrence4B3A4 45 = -(1824592192401261495827628789319637660417700282855900683 * 10 ^ 70 + 2880924151867233459882780993043580115426617327158882717188052908359317)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_46 : Polynomial.coeff recurrence4B3A4 46 = 49356520548113354178724953368019327534039062282588353164 * 10 ^ 70 + 3213570781338789948958714722176608240496008895387214866476756821383914

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_47 : Polynomial.coeff recurrence4B3A4 47 = -(1247173142215588937376198593673987860619045555483565554523 * 10 ^ 70 + 9550145810461779281230599062930574357952678828737037868970809180791729)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_48 : Polynomial.coeff recurrence4B3A4 48 = 29391068774499547487033152468693243383540568327934365177097 * 10 ^ 70 + 6428589388634073721929235600119956775274594652633314911551548489276782

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_49 : Polynomial.coeff recurrence4B3A4 49 = -(643988556587790952350133673332682823755147252680104054510622 * 10 ^ 70 + 5422529391215386448274914396354701124396089306426871715610034319224975)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_50 : Polynomial.coeff recurrence4B3A4 50 = 13047588943244749795115690222515983803989450520251425446497161 * 10 ^ 70 + 9425307701547514776238969044198095065865640483978778284046407655652874

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_51 : Polynomial.coeff recurrence4B3A4 51 = -(242026927414999306503619473438532509080966421650465781823986494 * 10 ^ 70 + 9634296327264320394299766025954353995334609163736951949048596070950728)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_52 : Polynomial.coeff recurrence4B3A4 52 = 4032513029095859205120214678873334849892986199526067413683207099 * 10 ^ 70 + 5218718916076043792159039889266861560023211639451273587223152398312916

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_53 : Polynomial.coeff recurrence4B3A4 53 = -(57855105986179784351285160574356682828235167024002674046201340017 * 10 ^ 70 + 9158825859408875410638575063199904116599652858562749518005163783537050)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_54 : Polynomial.coeff recurrence4B3A4 54 = 632083386135718499165264351008713347889428192977090362259980347761 * 10 ^ 70 + 3690126671281390578030114213747596842684274100878746508193191573935024

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_55 : Polynomial.coeff recurrence4B3A4 55 = -(2223775553871885018221969875564856471179025879078691750478719377731 * 10 ^ 70 + 166478563218233295385965577337149293331869861853423495702061468946228)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_56 : Polynomial.coeff recurrence4B3A4 56 = -(135703096157525107000577293520594833110916780354964055485760070812149 * 10 ^ 70 + 4019597140279954151563141638783854684293299058061822723520310539258057)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_57 : Polynomial.coeff recurrence4B3A4 57 = 5384944106712872961319107947397531570696695201594187511661262535135320 * 10 ^ 70 + 3575509766377436047619903948610966975569422929162509988261744287804941

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_58 : Polynomial.coeff recurrence4B3A4 58 = -((13 * 10 ^ 70 + 9352130086286857918425526675384713831970545053000563959241964430165651) * 10 ^ 70 + 4901075895292370469312193972734570973846727231624029806301635567679093)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_59 : Polynomial.coeff recurrence4B3A4 59 = (300 * 10 ^ 70 + 4777473268899604458112719800899014658692862783649596836959059828237189) * 10 ^ 70 + 8851578618131351276975796594171539539887077379228654732997714634169059

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_60 : Polynomial.coeff recurrence4B3A4 60 = -((5774 * 10 ^ 70 + 9694281347015255806191707762258361789481777231063335491468033099579213) * 10 ^ 70 + 5141700998448042635920766444284782262860640809901405985969910544848421)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_61 : Polynomial.coeff recurrence4B3A4 61 = (101816 * 10 ^ 70 + 9548949629205894015822444106852185598026771393789158126075468671872966) * 10 ^ 70 + 6990501404511659116699881223102824336046401315941834632744482044942788

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_62 : Polynomial.coeff recurrence4B3A4 62 = -((1671949 * 10 ^ 70 + 8875182957688473418189303124960629640777792506040416366504297162517098) * 10 ^ 70 + 4925661539143895323377363919704895362850710859819134295223769386485593)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_63 : Polynomial.coeff recurrence4B3A4 63 = (25807067 * 10 ^ 70 + 7166260244071107639217437512894443641670200914029275749883322034154223) * 10 ^ 70 + 4167314919620557979265261956875746796132058080411052969693555905325262

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_64 : Polynomial.coeff recurrence4B3A4 64 = -((376702280 * 10 ^ 70 + 9360887242358579709629690947397663444223618363156250838592224267247797) * 10 ^ 70 + 4853004562488281472043269516264234411440790400190167329339477466269671)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_65 : Polynomial.coeff recurrence4B3A4 65 = (5222363639 * 10 ^ 70 + 6720383426657146571029757489200042406011373870269596922457233457074556) * 10 ^ 70 + 2577297612753412173306704944022632715720916267844526307261285278722179

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_66 : Polynomial.coeff recurrence4B3A4 66 = -((68982654889 * 10 ^ 70 + 1526411436634432137327857818356574750794410403304770770340591867167712) * 10 ^ 70 + 6199361397967747612054300262991831957574632798704008044881177508381249)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_67 : Polynomial.coeff recurrence4B3A4 67 = (870372817881 * 10 ^ 70 + 4317227382245145106371143413016017754177580892177429438483036175099546) * 10 ^ 70 + 3973784285460947532876777706450254884267851140506439475402331040605175

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_68 : Polynomial.coeff recurrence4B3A4 68 = -((10510983803957 * 10 ^ 70 + 7717761554655355688437270062012057964564880777534057230913814459185176) * 10 ^ 70 + 8166281760306581528289264080517613941103016718203506865640434093814423)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_69 : Polynomial.coeff recurrence4B3A4 69 = (121698732186185 * 10 ^ 70 + 5768749131266580557340877107243820162046740992781204097536667020986148) * 10 ^ 70 + 4526265840360259456976832740996878587344054667454641735840615492123990

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_70 : Polynomial.coeff recurrence4B3A4 70 = -((1352872417155737 * 10 ^ 70 + 3541710841790632223220102055987649926821032292736216965124036423239098) * 10 ^ 70 + 6236511725828860344880656241026003154907516563052067245956047545583579)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_71 : Polynomial.coeff recurrence4B3A4 71 = (14457635121594877 * 10 ^ 70 + 6572835309633227328862718243022572241944242201348593587915025569612147) * 10 ^ 70 + 9019342143908748280414798962045614673552314127913639986707182021765101

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_72 : Polynomial.coeff recurrence4B3A4 72 = -((148691246999517090 * 10 ^ 70 + 6325446837146302679200900157713513509981958891836911183209108480849538) * 10 ^ 70 + 3486650454007652885327669629627998806012697233676633567995803315834903)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_73 : Polynomial.coeff recurrence4B3A4 73 = (1473157400544504215 * 10 ^ 70 + 5825894580398806062731264851661119180331475671120259179993657148442286) * 10 ^ 70 + 7682139468261677168559733923692936424518012769854089751791257393053207

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_74 : Polynomial.coeff recurrence4B3A4 74 = -((14072647871657198398 * 10 ^ 70 + 6013372398718816766000226524851234315961160261900981329530536647988718) * 10 ^ 70 + 6707241075974446876920381689511250604112059777855260635414770139183299)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_75 : Polynomial.coeff recurrence4B3A4 75 = (129723713127066712106 * 10 ^ 70 + 9062045138046107763169938828749465738172220509001559834162152192682568) * 10 ^ 70 + 2378373484630940613603597446860070802150467429081419710052930895006801

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_76 : Polynomial.coeff recurrence4B3A4 76 = -((1154797632143634932093 * 10 ^ 70 + 5155626549489875616090185028338133778562146118711874504844988367101959) * 10 ^ 70 + 6714113598847748300093212856103453329899041173571017525800281705329516)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_77 : Polynomial.coeff recurrence4B3A4 77 = (9934312066601556428473 * 10 ^ 70 + 6166902520341484000278420033070392472023156538768991182166075152996829) * 10 ^ 70 + 2894374888165318454797636733753676281961107358147885539019813092450692

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_78 : Polynomial.coeff recurrence4B3A4 78 = -((82641316354142442822558 * 10 ^ 70 + 1287636543387656009506541315954581432377075184054555223792009478497653) * 10 ^ 70 + 9707138973917185391118235077046214832654892614296131590578455626803690)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_79 : Polynomial.coeff recurrence4B3A4 79 = (665194428897354010847527 * 10 ^ 70 + 4375354593708784300533347337640658569770469600286197882352543570245864) * 10 ^ 70 + 220481095146071645637310637427004413811341121619887047159142038126733