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_139 : Polynomial.coeff recurrence4B3A4 139 = (2698278955469032066560068359080402345204249782679857384715 * 10 ^ 70 + 7407843310518272159768694622544093697291412811331870170643347125073880) * 10 ^ 70 + 8352318926058057760575383794731985771740904159665067973756429103075271

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_140 : Polynomial.coeff recurrence4B3A4 140 = -((4959258180494536380118547026653064451657354103445537849728 * 10 ^ 70 + 777651448445433985254097036208191729377238894675256431721382447780803) * 10 ^ 70 + 8597123472055743819350647722181485746969487654439897385408471575596156)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_141 : Polynomial.coeff recurrence4B3A4 141 = (8929279428437885235883947042281531017948076558184847690865 * 10 ^ 70 + 3491832989403583079072094108212846461427819570552236786601764382781520) * 10 ^ 70 + 3506000862061470440122473144884494415718631928903258582378806600873588

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_142 : Polynomial.coeff recurrence4B3A4 142 = -((15750327849080757134399372382460340937766542409811712003977 * 10 ^ 70 + 3868219363374500414391870031556341148612579676903720071958384011429140) * 10 ^ 70 + 7193439093032175956854925775869839004345383572314961851535189604601031)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_143 : Polynomial.coeff recurrence4B3A4 143 = (27216824477247768428689410963615098107004517769708722959942 * 10 ^ 70 + 8000018227574764075142406384262421644643286395398382017123551753557348) * 10 ^ 70 + 6726729527820058815417167006586914692487842794877644140390267555927475

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_144 : Polynomial.coeff recurrence4B3A4 144 = -((46074276631110733022001841674826861344179775676098621120727 * 10 ^ 70 + 2741108137999527831520399494608777886048865490308340630271305356807210) * 10 ^ 70 + 2334186908118284558186596365931293381974892756672436346631011928278257)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_145 : Polynomial.coeff recurrence4B3A4 145 = (76409711833301157257165441584952152759542605872540778734886 * 10 ^ 70 + 641240162277608291650299597923667797057270373072027833883882574139153) * 10 ^ 70 + 9361123383402443494334345278169611824143745800253797516301356045136530

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_146 : Polynomial.coeff recurrence4B3A4 146 = -((124136729688439167100386014451864937780875740626804540068861 * 10 ^ 70 + 8829803206654840482833459803162481447091303514688187015645304486489616) * 10 ^ 70 + 9371814814620534030458854377292589449106733147459830794361146801498220)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_147 : Polynomial.coeff recurrence4B3A4 147 = (197561918593097902883399650211606517503809407368430099239467 * 10 ^ 70 + 3361612228964940198300955692991281782019883253453631441205397361109614) * 10 ^ 70 + 4543367586305001114478478312773172708164290210564348247568794785420206

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_148 : Polynomial.coeff recurrence4B3A4 148 = -((307994768814111580325959285925804410574893054418016813012867 * 10 ^ 70 + 8076830036353284822274819030278502519489277993793493634192100389382847) * 10 ^ 70 + 7680113084262313059264053331341522315299555374351688534795317420168120)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_149 : Polynomial.coeff recurrence4B3A4 149 = (470330060882752567676811672514400045418069779055334438835821 * 10 ^ 70 + 8438100373872585049509460593531070843107168939600603325925187254328925) * 10 ^ 70 + 712991148321636068798945006624420002531039091733005338490035552571482

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_150 : Polynomial.coeff recurrence4B3A4 150 = -((703492235409342256657528265731788603365992948946755188453610 * 10 ^ 70 + 9524816303876879532446932695574317714432325819307818068263646115025217) * 10 ^ 70 + 5447984110840511405001877591180947838985348852787663562298864860175864)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_151 : Polynomial.coeff recurrence4B3A4 151 = (1030590734034319962223536969471518204193099666436948264846654 * 10 ^ 70 + 1493547198859372723558793214222562147522246119752021684662668649792904) * 10 ^ 70 + 9101315254577119986581736971656574668852817110435447957427036214476857

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_152 : Polynomial.coeff recurrence4B3A4 152 = -((1478602510083843896773055183443005710969348371247735759149867 * 10 ^ 70 + 3114094238989029313364649863607042246454607220726464284287085652784361) * 10 ^ 70 + 1951946795638398553592103677144254248336013787287190909658808411325831)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_153 : Polynomial.coeff recurrence4B3A4 153 = (2077384742707583640066446616315974334012732085749752527418073 * 10 ^ 70 + 7298831370498003069359773136880724579102753652080265391652547535740444) * 10 ^ 70 + 2475169586896503019653084070010284906211965008094239824479981554370493

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_154 : Polynomial.coeff recurrence4B3A4 154 = -((2857840777596868752148933482032498780018124162722113846107679 * 10 ^ 70 + 6307317397054848073542837969665984370779834928185172511635009427618526) * 10 ^ 70 + 1745372183982786102221782766851229086711849639665742656791525651353672)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_155 : Polynomial.coeff recurrence4B3A4 155 = (3849127799237549498051064462399579676407802474216532753086808 * 10 ^ 70 + 2577509098706399649827963163434937713816430505234862279047866758339925) * 10 ^ 70 + 9701007123308605721052848368043167800620311602857218492293744720166974

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_156 : Polynomial.coeff recurrence4B3A4 156 = -((5074912928436252123788219607106846910329133324262684169926160 * 10 ^ 70 + 8905501001099940579210386643106613828110236295697085462545778504339589) * 10 ^ 70 + 3809348358973778726494822319302838172967727945663250528177172690427959)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_157 : Polynomial.coeff recurrence4B3A4 157 = (6548853039702880136488750152604631071483589088365115795159591 * 10 ^ 70 + 6454752709071938742709257443576543074998739811146486457446397487062222) * 10 ^ 70 + 9778501602300429846954484356558263938138954829186395245780853322923066

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_158 : Polynomial.coeff recurrence4B3A4 158 = -((8269677113438540007934052602976797502422919393563829182245989 * 10 ^ 70 + 7719258584569908692915066990851712165925526356763381934407516939798792) * 10 ^ 70 + 5501692389697944797071787755654521304930093555045225870059695707743916)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_159 : Polynomial.coeff recurrence4B3A4 159 = (10216458145899696982774632058299298509912354991192121288237897 * 10 ^ 70 + 5052768994348837852375297346897726681381652099164707177965381193076964) * 10 ^ 70 + 3594981460169681664127858996719008126146633852792633009654857007661377

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_160 : Polynomial.coeff recurrence4B3A4 160 = -((12344831550917946892194615972248162872147323282841714350270244 * 10 ^ 70 + 8980715585125937228764514398376750174977609388385212247688071600616340) * 10 ^ 70 + 3874988332707951894741988019648386010535157407428092796826789812211601)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_161 : Polynomial.coeff recurrence4B3A4 161 = (14584999183672579448841159655724427031230964983594281275844115 * 10 ^ 70 + 1981061309955345199514596343913643392978461422323488808030958865311285) * 10 ^ 70 + 1460197918880089084388394430786289419410958493573487745587140962437281

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_162 : Polynomial.coeff recurrence4B3A4 162 = -((16842307123780648306610760130741428707435689200691934555355420 * 10 ^ 70 + 5791934062303947175338522089416385002441233537595399552405425762661010) * 10 ^ 70 + 9313051952652711825381764972220193813138760585809697903019156525165366)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_163 : Polynomial.coeff recurrence4B3A4 163 = (19000972405436585999629831920289655571926152686985976071404138 * 10 ^ 70 + 23459363380074443544955979443616739060490037250860862406600713307891) * 10 ^ 70 + 9739616444947985980736580897440749974037411841566874013365781669170917

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_164 : Polynomial.coeff recurrence4B3A4 164 = -((20931159090234489634482512021372387814601687830028977627790376 * 10 ^ 70 + 595596252551134190907292921214110461360852067712407511887774683837668) * 10 ^ 70 + 6673608299309377925943703157365864768861762104600321774860568520170363)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_165 : Polynomial.coeff recurrence4B3A4 165 = (22499104301971557945260780347955586289500113338053459774890747 * 10 ^ 70 + 7039887138249154691531600427309310862591274144337612136423284518583795) * 10 ^ 70 + 2394093070575716784337292103949982110469244910664582256841937456755881

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_166 : Polynomial.coeff recurrence4B3A4 166 = -((23579443788258401959369290824566661655360133767591796624221243 * 10 ^ 70 + 5142237752505462756675374046267723029157460344219951846054922317411023) * 10 ^ 70 + 1133686576997973525036335032298979453465239036179396157386642065280219)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_167 : Polynomial.coeff recurrence4B3A4 167 = (24068385163394137024956618559724896324674779374573030644190004 * 10 ^ 70 + 3774777473287053284811647788674577485760392189314647652365293417845506) * 10 ^ 70 + 9611456052823900898349696939949725992447427178519744444003465466824555

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_168 : Polynomial.coeff recurrence4B3A4 168 = -((23896034504460385400952529177120406625670960057913486668354111 * 10 ^ 70 + 8497839952193424224920478853561601223384098004310519764512492925887335) * 10 ^ 70 + 1254989921390846308054987210833976639839023388842256227168176445261450)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_169 : Polynomial.coeff recurrence4B3A4 169 = (23036091388248349785988231164416559877439160471177460948004837 * 10 ^ 70 + 6569052499103959723105106594995835556552086516767167208918848258108508) * 10 ^ 70 + 6160093144403251230401117303259922036564584358793419852822400359845212

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_170 : Polynomial.coeff recurrence4B3A4 170 = -((21511340735374019009334576600711174564140105550809606632467019 * 10 ^ 70 + 5553609305018784680523313926045337158944579491194341700825383453109628) * 10 ^ 70 + 5195379040107518514674074165153391020125472559985893748136265098947715)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_171 : Polynomial.coeff recurrence4B3A4 171 = (19393880030910731516542144540791406176397362440135304247692261 * 10 ^ 70 + 3177287399581833314210275016439529203974480696067607587479421280901808) * 10 ^ 70 + 1479914631825769812872948850723244094354092549986032178806314850743508

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_172 : Polynomial.coeff recurrence4B3A4 172 = -((16799756516426785607689953908158390247720298512386738507799695 * 10 ^ 70 + 7674442110890351113932254544211358427692055904261595142584216209173521) * 10 ^ 70 + 6236251490723516700513310975418386723031617969500741212048212103362678)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_173 : Polynomial.coeff recurrence4B3A4 173 = (13878525840095855670956590677030781536247897291756441823800699 * 10 ^ 70 + 8266542153831944694710046972660871408270416950052066850249545593231495) * 10 ^ 70 + 662561260726034726801775888357966934479886184496381213032088231570722

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_174 : Polynomial.coeff recurrence4B3A4 174 = -((10799027229890590178070150253455023268122914239943027358312887 * 10 ^ 70 + 4280783773240980347861192873138997131581742422104048873815090222404449) * 10 ^ 70 + 8142310328305428349761406423881090224184325761061164085255922279464249)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_175 : Polynomial.coeff recurrence4B3A4 175 = (7733250619445091527417155152057236851488364915478360824521989 * 10 ^ 70 + 6292526327142722478361708946470105509670913686652390022995524478454249) * 10 ^ 70 + 9119307911009126089239705278784991548872838893501047228562632461295408

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_176 : Polynomial.coeff recurrence4B3A4 176 = -((4840436715313507984118602285484020048323704479033852689060836 * 10 ^ 70 + 8079002499308744240886802975935398630183246757331738539947078284326377) * 10 ^ 70 + 2510817268048430025876511324337209049449184223925404903246141067645459)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_177 : Polynomial.coeff recurrence4B3A4 177 = (2253454117332099240377821315012980953269052018004406370969841 * 10 ^ 70 + 8467978586264847921898115660651505916768342799437809964915537671976892) * 10 ^ 70 + 9674274815417825042884868792621217382222363910881310384106661328069654

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_178 : Polynomial.coeff recurrence4B3A4 178 = -((69065062670329878692415453045003894120368514717753377175550 * 10 ^ 70 + 9843853293229623308763645216812651017395623551115074037351527589844811) * 10 ^ 70 + 8268245508698886272441180723567076819018143955225312165747954467124833)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_179 : Polynomial.coeff recurrence4B3A4 179 = -((1656983134539141950940706486868244037773163916566868726077366 * 10 ^ 70 + 7269696889329454832342709326322919564019867856682520287681558743743231) * 10 ^ 70 + 1467841138476958779297439617754443105097676759791770119017656815301255)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_180 : Polynomial.coeff recurrence4B3A4 180 = (2909882833696289064567522620008016879455974127586694662354384 * 10 ^ 70 + 5064730375835693800974698120175560815915576196299954005167198995739922) * 10 ^ 70 + 4196165511624937758269624152914401263593413632042353999609541702694185

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_181 : Polynomial.coeff recurrence4B3A4 181 = -((3711283391408144823043890907902962610490703589940309056586189 * 10 ^ 70 + 3230253967033708587923315134880497186577318088900915361740392909915364) * 10 ^ 70 + 1225042068886190738456078687052392238524150272704187428821205161184860)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_182 : Polynomial.coeff recurrence4B3A4 182 = (4111540086892461739981251831800459401430217025889851081678183 * 10 ^ 70 + 4693695307305871639019345869773985233857549616670222111057329179607682) * 10 ^ 70 + 2405225320958095384826824127045522265507529716185120771314593273586944