Recurrence 5 lookup certificate: Scalar0Main coefficient convolution

This is a checked coefficient-lookup shard for the fifth pseudo-division recurrence in the order-seven certificate.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_118 : Polynomial.coeff recurrence5Scalar0Main 118 = -((((1295393575595166799327761857928296621079471368923 * 10 ^ 70 + 3255273501485173647841159527696178908769872111200793172014849565707310) * 10 ^ 70 + 6948918373712377027465309808882314226048589666269972466030445039106555) * 10 ^ 70 + 3307807820712282775035579872258789425374948913388434643377153847454353) * 10 ^ 70 + 4719638107345024809038693416838942627267900517698101606984448041447669)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_119 : Polynomial.coeff recurrence5Scalar0Main 119 = (((7220907375928945822856214764937299297323939136796 * 10 ^ 70 + 7809823392894499250803303117084358738217685165346603114876432420810779) * 10 ^ 70 + 6546309771529328269787096570153166184649934378209899383284464401895018) * 10 ^ 70 + 2527153533572895982754147961096894621244134123804411165684531990391564) * 10 ^ 70 + 101627974133503368011324619504495757188645475438871589634724393494359

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_120 : Polynomial.coeff recurrence5Scalar0Main 120 = -((((39310828647536969835831949864220126238826183790951 * 10 ^ 70 + 5413706677923402433709504004407913433003292473501788439475926200549920) * 10 ^ 70 + 7755963512183470915402235722990588913497313065469243712288924648756343) * 10 ^ 70 + 6963445944506337478086293522738224866761939248205645398946383789678456) * 10 ^ 70 + 5537439364142674197120727395863525797492925031165617761088719430709041)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_121 : Polynomial.coeff recurrence5Scalar0Main 121 = (((209052532729867495274499354472482557346859058672849 * 10 ^ 70 + 2250679024020225393323156783129324486760221799050343838149973679501943) * 10 ^ 70 + 3019525087095294230434927722426677970221615086247708299172576403222177) * 10 ^ 70 + 438969862417584392118273364122798149588045838710931453125663879485986) * 10 ^ 70 + 9788746794131528473703893747176130436500933655046728616489692182089572

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_122 : Polynomial.coeff recurrence5Scalar0Main 122 = -((((1086204022514687780760156335479120333559092590021271 * 10 ^ 70 + 6050275900505087849431024153481200193015268492011897762569988698372789) * 10 ^ 70 + 5125448376161742049261982592368081968999784752473453953716619754371544) * 10 ^ 70 + 4347710662884676439285809541781048151818375056459549625309593269150893) * 10 ^ 70 + 5242485613086681732946278317486438854480235941813398585367470898965287)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_123 : Polynomial.coeff recurrence5Scalar0Main 123 = (((5515280916939257203815244128911099750222861526924812 * 10 ^ 70 + 2496392679069773341834509278873200375982383735458920572121404005806404) * 10 ^ 70 + 9097670052720012402123501928351906967085698343795692961708509466587163) * 10 ^ 70 + 2323963738900252273820487020465059275378571812051237350136469854195259) * 10 ^ 70 + 4944098227250093079216686420857571209308418696266634064988226454960592

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_124 : Polynomial.coeff recurrence5Scalar0Main 124 = -((((27372175622666761021703838624944644523436687629818307 * 10 ^ 70 + 222785823597937588783138805401977575161590320128477534168666014136496) * 10 ^ 70 + 8669889714050198115457003830726506696085759036286635871679509264919189) * 10 ^ 70 + 5360322293865939881766311784873042101239158815707101218111057252497105) * 10 ^ 70 + 1574720466021213115240267842207997198073864268763168487538964661589245)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_125 : Polynomial.coeff recurrence5Scalar0Main 125 = (((132806516149240328168350543512385304226565892845437681 * 10 ^ 70 + 3495781961600254775141728282760277113513871135559531972331908993762704) * 10 ^ 70 + 869886157040962747504889304489571416579405116032645908684459016786554) * 10 ^ 70 + 2802636768606162260067849944467519711337377242838614739463406609083521) * 10 ^ 70 + 8089581910543685021963398269825697398307997355645413270635157219295230

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_126 : Polynomial.coeff recurrence5Scalar0Main 126 = -((((630055186415657057431815603263629107143125011699610228 * 10 ^ 70 + 7070490315998503358806713851380655728491375571268677700212485198809254) * 10 ^ 70 + 1633306409664836209058545004825460839888857233480624855760844996469565) * 10 ^ 70 + 3441601844067422782831960091984729629018188843120244467853792442667984) * 10 ^ 70 + 512811585983212503557997113622797155791351308834074083100514411899585)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_127 : Polynomial.coeff recurrence5Scalar0Main 127 = (((2923247414496159180007816068524023263268840626113006999 * 10 ^ 70 + 4949404273676756900701828897058313015744171976757435622014505403176466) * 10 ^ 70 + 8203285533816013100531242212565986539226813237627210958229134441964371) * 10 ^ 70 + 597507149030045560131963981167515773926431153618563724510843665208880) * 10 ^ 70 + 3256040752778977808473408684820604636413572454340312694747973678408783

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_128 : Polynomial.coeff recurrence5Scalar0Main 128 = -((((13266516929997293438003953541953362235799044192495849828 * 10 ^ 70 + 6266316015371668286755479435849118825605975295580904946030175545251172) * 10 ^ 70 + 2926883737303009400857090822255239065749745311069381241380014122533043) * 10 ^ 70 + 4020488259749434445954987583592114414399775883936568453625496645284185) * 10 ^ 70 + 6372233168208387131794005479108627545121055399872566697606882401179687)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_129 : Polynomial.coeff recurrence5Scalar0Main 129 = (((58901614713113056431747384016145579552431375266781396205 * 10 ^ 70 + 8300640143063630892221190860849963638665358868421066282913116741707832) * 10 ^ 70 + 4354751844372218062633213426080129973453526683588534199109578922350596) * 10 ^ 70 + 9017143797843383848083349169928191700417691131648225542652415511976170) * 10 ^ 70 + 7121768859034208647595316043944603247152882566176706954767526031456179

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_130 : Polynomial.coeff recurrence5Scalar0Main 130 = -((((255887502611396750242402605173550097583127833740624827830 * 10 ^ 70 + 4123713653953808117405418625426888538668145015871650577257820242548748) * 10 ^ 70 + 7194606650609097970212166176439144350469589243858816246025788227528818) * 10 ^ 70 + 6861986010579088778838009575477032606466905742848329769735937519303357) * 10 ^ 70 + 3103765440383919576985063372052206076861085932550108174007680888316894)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_131 : Polynomial.coeff recurrence5Scalar0Main 131 = (((1087910835617722575952501930879692736168800824163923332824 * 10 ^ 70 + 9828332550074982518658984364113833050273424544731033691556323705991544) * 10 ^ 70 + 3875408868062066293091550908891040286871216811832731132744140059043762) * 10 ^ 70 + 2310279894532047849013598641874580489841853321764158314657762590317092) * 10 ^ 70 + 1176475709091786936159668956489582893245499587691662686000500993017118

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_132 : Polynomial.coeff recurrence5Scalar0Main 132 = -((((4527190904961871512722047454248875617174006826930928891140 * 10 ^ 70 + 6651652753255755605693900363808503262267034173434950327646162284549532) * 10 ^ 70 + 9535166175218691733673484884368224470925088764869855774976173109942560) * 10 ^ 70 + 4811174131104783914792244969794161377881812923910990687268404897981888) * 10 ^ 70 + 2904004292699823527727737671801107432995078163225317937295151420611605)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_133 : Polynomial.coeff recurrence5Scalar0Main 133 = (((18442625110990929372621561375457534140373155334302497443189 * 10 ^ 70 + 4619974917773372173292173816648558516420313642798536882432492508251044) * 10 ^ 70 + 7029449550350776457137405568139262035599472425042543748863478126010832) * 10 ^ 70 + 4957453067475724582577594689383108327751884330891633055031503708227616) * 10 ^ 70 + 4412316789645280986204139377097437720051792929748267749760894416693823

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_134 : Polynomial.coeff recurrence5Scalar0Main 134 = -((((73559793366677350971073763244473017773831771344560503793445 * 10 ^ 70 + 1778314647449559316869251890672650087260758150076028706702837220263006) * 10 ^ 70 + 3926217674780898098718324423739665395187184340692864701880168585913032) * 10 ^ 70 + 6638813134806887397599868533312884120307291260582622502274177142599491) * 10 ^ 70 + 5610011866254485871174259077478702626814875446023021129316583600969926)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_135 : Polynomial.coeff recurrence5Scalar0Main 135 = (((287306740183365314733243580843364424881922551666211194051836 * 10 ^ 70 + 1896971996101991440262075601249427088952847092378368565745374795528788) * 10 ^ 70 + 5513932566642554098989618163435355331387713110988322701262124495933791) * 10 ^ 70 + 988987445273901585949514809287465531282485570291365003906162850188820) * 10 ^ 70 + 1213500098923802776121373986103501124161448492717076040784419218314270

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_136 : Polynomial.coeff recurrence5Scalar0Main 136 = -((((1099007749838937205413072386618814224264649488972424414347652 * 10 ^ 70 + 7531264941299863209276256853726409263014632784752423291608094337035054) * 10 ^ 70 + 8497090823680602268025581645778725224052710627539507975713995933144889) * 10 ^ 70 + 4075729678660111647055146346039186228280128844015075479278227833924191) * 10 ^ 70 + 4308663592412749601295283908351666709803557337862910650928796854172893)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_137 : Polynomial.coeff recurrence5Scalar0Main 137 = (((4117805174417360860796731436421639037003383772466391245655731 * 10 ^ 70 + 5138132026414461206322973119359750969230079909442208445452018320464474) * 10 ^ 70 + 4817638315193232657229132719700046940308281216266491555180383194341491) * 10 ^ 70 + 450097275859703935278115812522438618624080718180013710732270537806749) * 10 ^ 70 + 8210344999119523108594535433538701027646529909136384520232727069246181

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_138 : Polynomial.coeff recurrence5Scalar0Main 138 = -((((15114711051583239822513275829508182662098187105745562534627205 * 10 ^ 70 + 8825394798299072004502572748631337482699511142095075230900585194599283) * 10 ^ 70 + 2235628261993034853506032194815086548785203967465843010457364013011815) * 10 ^ 70 + 257975498071525476744016447273100600461769140037488506542464764445489) * 10 ^ 70 + 8975420263620630822128831258498582587621950904533198751782831775923156)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_139 : Polynomial.coeff recurrence5Scalar0Main 139 = (((54357605027428490459938508628230384861711408366832409810772978 * 10 ^ 70 + 3693440229490306943297707079842537923014173600530359444731633401643936) * 10 ^ 70 + 2288690344134554931064567370408706487086865282196365705018088023667741) * 10 ^ 70 + 1029655510087947961350112888904765858848075717048144893069086705182173) * 10 ^ 70 + 7398853536820647888070511455630252200662561510083885088522846496290267

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_140 : Polynomial.coeff recurrence5Scalar0Main 140 = -((((191559240480450257867108901708750095566394568615185602121222522 * 10 ^ 70 + 5176918101378787325371238088880315751254029089579551441761336306252484) * 10 ^ 70 + 5850464031626858099758207351159539262809337548745449815628811209222594) * 10 ^ 70 + 289587192031510450587151167214373106738245376065329298251265714256513) * 10 ^ 70 + 3633358878792358431974260056617827439404611231089220922051042314671189)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_141 : Polynomial.coeff recurrence5Scalar0Main 141 = (((661580515326277010934383620892352584618353466327211923151926814 * 10 ^ 70 + 1109177824515182238236440890177026510381708262994904867290631481902378) * 10 ^ 70 + 2913229552809212678130687046805617129651744629954592810468533063274523) * 10 ^ 70 + 8538976530792715677824202188473496395548195905336465260728075549772052) * 10 ^ 70 + 6301577513228477678266416902662432466427953307694522374772690761333170

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_142 : Polynomial.coeff recurrence5Scalar0Main 142 = -((((2239505788928864394606791249792020775942374715068904401786402751 * 10 ^ 70 + 4119993282110683869586857981033846231141678413168297926320118747566439) * 10 ^ 70 + 9302264398936777791725458575920281227426597385258711139907251192816123) * 10 ^ 70 + 8796754488180610325171291976669473718051577645235031539626071705628) * 10 ^ 70 + 4991404472906639190449618832046250259805839412316419213234989249258)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_143 : Polynomial.coeff recurrence5Scalar0Main 143 = (((7431273902346027603093780666186205590510711909718710052798381453 * 10 ^ 70 + 3795253583546155146140366017072350036051512873800853897401979535673177) * 10 ^ 70 + 2201566156605374097155380932969326265395173309415253285666026637780114) * 10 ^ 70 + 5181142786044923637296110857532497479631020323644275034211023826785747) * 10 ^ 70 + 6864893460151066303153083244103198064086034196202496384053001622868921

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_144 : Polynomial.coeff recurrence5Scalar0Main 144 = -((((24174991389582003881947692590117085428638666834937271836739112831 * 10 ^ 70 + 5813408498444152137485473063960868487641782253033391388202987885927890) * 10 ^ 70 + 6289721209818045487248555651782927133532697078490531193124816296683182) * 10 ^ 70 + 2338099223519953769103372168227817099396432797292503336183512294622894) * 10 ^ 70 + 8041478467800026728682091090835700238479441138098567399546664800561592)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_145 : Polynomial.coeff recurrence5Scalar0Main 145 = (((77109956352988907505599386838748093379711965198023847192554395209 * 10 ^ 70 + 724118064822383585204100309491362783329164413841622762080555911875471) * 10 ^ 70 + 3924514253646672085348795291488205938601170928414084285992464849381369) * 10 ^ 70 + 2145449537098395448299179650886997096807418229658645635970453053678507) * 10 ^ 70 + 7214245531913241417491740364726152034907485245714195465312735344203284

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_146 : Polynomial.coeff recurrence5Scalar0Main 146 = -((((241181220012486037237976352193520900295746451759877931267121448178 * 10 ^ 70 + 5751646327788388995434011152601045713757164201561888384700034553705949) * 10 ^ 70 + 1589856682268071256160788529186586069354702147380371872061016606029553) * 10 ^ 70 + 4940932293916558878753748204355327183085862029086274235949275617380562) * 10 ^ 70 + 8549539489890749130767075074023573861605901347254210700780873591571112)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_147 : Polynomial.coeff recurrence5Scalar0Main 147 = (((739796078608136446161342572934737739420628035268405563332082076475 * 10 ^ 70 + 7299593233581535818482378790179993259993448765910693622822327998289841) * 10 ^ 70 + 9834008931726311562111840077229859357549051200558006087278313909295774) * 10 ^ 70 + 7985530656048697300165689559626296451952166417632409466675779074207637) * 10 ^ 70 + 2956072180432421085317149494224784082876860507336925303432769638294722

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_148 : Polynomial.coeff recurrence5Scalar0Main 148 = -((((2225673638734873877014299728077816800927750390152098846840782017601 * 10 ^ 70 + 2751465730302649503141619137188727058169017927565377003791475149095398) * 10 ^ 70 + 1301869574562576434100294435852168161864795179160795436951823215950087) * 10 ^ 70 + 3637454184310925552364542544360994069020291046257765594779654615524312) * 10 ^ 70 + 1866445133914362979412009659557116723968492580149372171173300078453544)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_149 : Polynomial.coeff recurrence5Scalar0Main 149 = (((6568044870040364313557817307368380988526512290142389775106971108133 * 10 ^ 70 + 4701018938298556012391881734128561431305940982733127659328083947854489) * 10 ^ 70 + 1384858244501458395884609751859358087591589779075717215929033711418692) * 10 ^ 70 + 3664257459016257830475194642591338284261323245730884032885661236154685) * 10 ^ 70 + 6530534695101305376531700905417838782637954571474028029080770916883616

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_150 : Polynomial.coeff recurrence5Scalar0Main 150 = -((((19014242787962633863314069588124054369057384747295086133545634041943 * 10 ^ 70 + 3893336129224424988561774632071343155053653348895769059802074558106248) * 10 ^ 70 + 2447285485895389574893769984541494879761112822423633657420043766100860) * 10 ^ 70 + 9908341414429369125351616785656750021250802797409198204696558802299235) * 10 ^ 70 + 6598542690195025533878186747777539858451879833620788787956796798357400)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_151 : Polynomial.coeff recurrence5Scalar0Main 151 = (((54004789540591919502434976984055347904161509369776334344177662463602 * 10 ^ 70 + 981363038869706311650546700693127467505855900705676616702854103809278) * 10 ^ 70 + 471365524818244512191823874842202858525149881165732328044844992429166) * 10 ^ 70 + 7066396260768447283308673433888483425742885867914789417043753981512830) * 10 ^ 70 + 7199382922606172073571549369832049184728348554230202077401466064031716

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_152 : Polynomial.coeff recurrence5Scalar0Main 152 = -((((150500102257421773213756956776578060601285685682564304671360980262870 * 10 ^ 70 + 1078849385990754622124712666130990609543593060219662165342891744793915) * 10 ^ 70 + 7738178595860539726687390716958410264184444813656448044394367408297005) * 10 ^ 70 + 6994424218605210228870583445292770672360157040145205642127756425269108) * 10 ^ 70 + 4216502699382967038264049400147677859933964685105766375360188941807336)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_153 : Polynomial.coeff recurrence5Scalar0Main 153 = (((411559377442530623646099543036096412714562953309351953930080096719419 * 10 ^ 70 + 8205432224140677563867326073228269437488088915220655680450121530942263) * 10 ^ 70 + 9978584867927993310832663226325182692447744338553710945030421317427969) * 10 ^ 70 + 4458729041423025857953655489757271185249885154511504087418900706932156) * 10 ^ 70 + 5041558203163187674917903187367332494966511885639181720261856169539702

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_154 : Polynomial.coeff recurrence5Scalar0Main 154 = -((((1104481133955000148338055899589564155981907848897079841582716364980186 * 10 ^ 70 + 1374771512455189816793899190563670369623439045690360622600041385701194) * 10 ^ 70 + 8181489014901295560214727460762189581933796784585502324203203279957553) * 10 ^ 70 + 6514044193797210967814903631511872195382932372039615246967179225175255) * 10 ^ 70 + 724289700253890786434586525829533030257334096413601872378788030627082)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_155 : Polynomial.coeff recurrence5Scalar0Main 155 = (((2909056236263223513729116323782230456981151139357241875029391812000398 * 10 ^ 70 + 8369958729283191916560734148606894660505659422032669613419220264937508) * 10 ^ 70 + 528371172038261586281805669088949781841090154132414000052782735773233) * 10 ^ 70 + 8630140702779821197564253960706742841322404876170679838081522873132987) * 10 ^ 70 + 4654319048979767940207253752577930240177850652094652069005958883209711

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_156 : Polynomial.coeff recurrence5Scalar0Main 156 = -((((7520572654274674671257253596031278924022392712489139732959833687102582 * 10 ^ 70 + 3885319078434985870585302338426201698364724911774992916530825304166030) * 10 ^ 70 + 7754727698490252356593096789836604050169137979650766813574684926651191) * 10 ^ 70 + 5354674593100887521873148906791716312357922102581010682250650944415378) * 10 ^ 70 + 3877252189429716588082543750455162879143108288270597897849309882599835)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_157 : Polynomial.coeff recurrence5Scalar0Main 157 = ((((1 * 10 ^ 70 + 9084936545731163807218094130696158204407017360634405735219728891925975) * 10 ^ 70 + 3171357660809740735261240116124268790019519499514428874545064801362814) * 10 ^ 70 + 8677981524912378291578855960821789747203128985379735113305146290958493) * 10 ^ 70 + 9787186894136041609354826371324129548441844946380234165363683373611534) * 10 ^ 70 + 411726861138507674908441206562061667795135291477333603869949078020622

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_158 : Polynomial.coeff recurrence5Scalar0Main 158 = -(((((4 * 10 ^ 70 + 7545199729977250356424490726246032804442755582728320213928317446624523) * 10 ^ 70 + 3883628122003297085524667625468070190238568170789619516309666030089177) * 10 ^ 70 + 2282369574230705965495504971047855452906474548013088617312764466468822) * 10 ^ 70 + 4932345727935099734518443454709684405028390823192978907173419363233884) * 10 ^ 70 + 4168663152200611627899520135247517535051062579026310167693439831464024)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_159 : Polynomial.coeff recurrence5Scalar0Main 159 = ((((11 * 10 ^ 70 + 6287499652161919905186382859097921915432335820176581976601126973962925) * 10 ^ 70 + 6060254621181428983657371194260463346570439723517376032120480982209657) * 10 ^ 70 + 9200634315842859086685773748858056905634314193163352798838105020316339) * 10 ^ 70 + 5986688808600045552243562533725276595492052607414863463589080500529979) * 10 ^ 70 + 3010714292518946128539430273366441291827238858806901736058840356610512