Recurrence 4 lookup certificate: Scalar0Exceptional 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.recurrence4Scalar0Exceptional_coeff_134 : Polynomial.coeff recurrence4Scalar0Exceptional 134 = ((47763096393046966685884359799814303642657786001592 * 10 ^ 70 + 8969391716348441645893971542678961174336093218513802036406374016560620) * 10 ^ 70 + 4350975209801212652274802898295335107526191653058730973992086658106575) * 10 ^ 70 + 4540988790572020404497411278417854065338601659974611843026244911992664

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_135 : Polynomial.coeff recurrence4Scalar0Exceptional 135 = -(((161213524782424362703085321835058623602274352724574 * 10 ^ 70 + 2035172578985495423137310262837074819517151646093489613887429078636547) * 10 ^ 70 + 7152759762296390008171945726647926754290658489403133123555170033692409) * 10 ^ 70 + 9643055830729231472224868240706527329729266233214433577879622563623639)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_136 : Polynomial.coeff recurrence4Scalar0Exceptional 136 = ((125612065636566058455422828800565949800781729773626 * 10 ^ 70 + 561971946041638789472202416207121329764902925838425566076956989682001) * 10 ^ 70 + 8428290278427726168577671208517658108898359706473905382759377567938219) * 10 ^ 70 + 1501810930649171631930653670260744872987299057504557721999156359208658

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_137 : Polynomial.coeff recurrence4Scalar0Exceptional 137 = ((4283043648719447761357491637727189374419294741592820 * 10 ^ 70 + 5190717051403148626409132978489132754983579003383865106621292461963104) * 10 ^ 70 + 1757924924997234811796612569449626211029456565197851607371582990621439) * 10 ^ 70 + 1579824231569839522145711644368614748107973684569481207164147503747248

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_138 : Polynomial.coeff recurrence4Scalar0Exceptional 138 = -(((52673895886521179602344910122713018640239807223161501 * 10 ^ 70 + 6418882031356429437537339609453848063534017363359103672390919496261302) * 10 ^ 70 + 8100573480863198401916963210974373935702092280881860423029212237649237) * 10 ^ 70 + 9966422519753780600711132895205204096606135519432203450536351070942028)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_139 : Polynomial.coeff recurrence4Scalar0Exceptional 139 = ((442848551413180929781468438597108472926345456878182482 * 10 ^ 70 + 4875956425569666669032559642940653775883157046159689282525210035927450) * 10 ^ 70 + 8923929796994872616205845422046698817957026632311736263518782996378303) * 10 ^ 70 + 6332992697002331195204366922412935776799566650093243352246319806516571

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_140 : Polynomial.coeff recurrence4Scalar0Exceptional 140 = -(((3145915483574172278958642503879437363342841808090823514 * 10 ^ 70 + 7001964527301286217810584613729038236187572130773429798742276857920443) * 10 ^ 70 + 6753101120747353083684449888716279428922482041906223752198930922066380) * 10 ^ 70 + 6112948334945032640158123660753266550849215595471099592530924167599072)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_141 : Polynomial.coeff recurrence4Scalar0Exceptional 141 = ((20029807525468573673095854505877717499383366485728590038 * 10 ^ 70 + 1951473618203195954202257884779359126917426970781082719640939805246985) * 10 ^ 70 + 8487889932136423594364223749323191249898593722196039306091666634851089) * 10 ^ 70 + 7770960312030406472109287928376568861219462646726106298666225909029108

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_142 : Polynomial.coeff recurrence4Scalar0Exceptional 142 = -(((116872711540229834420293128828853277794078154853294128955 * 10 ^ 70 + 120564395675232979208437153386537797630504793970856960917043736423755) * 10 ^ 70 + 6732589832860876932307656518834812079128034820696499166789963799394623) * 10 ^ 70 + 5086504329710150389535734133440007310084986016584067574962692524337215)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_143 : Polynomial.coeff recurrence4Scalar0Exceptional 143 = ((629270593699390696506071980796419353092656636026443772054 * 10 ^ 70 + 3566189280359871307372172225705326845890217099565010657729848871360371) * 10 ^ 70 + 6297632568551388593807868537769178999876875592469933753962698064883223) * 10 ^ 70 + 359342042060080411817145644922521109789363351931658906647823136391673

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_144 : Polynomial.coeff recurrence4Scalar0Exceptional 144 = -(((3113876518362729966360085546451145380861417279957085850810 * 10 ^ 70 + 6145208829062698832144870681378402950079596375135987765305563633568345) * 10 ^ 70 + 4641308360483792885334536002421557566519898546216350988153836590561741) * 10 ^ 70 + 9433632911767766266774319152402232717836794282746407351767504138453532)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_145 : Polynomial.coeff recurrence4Scalar0Exceptional 145 = ((13906003788195898884993877312145735978448430249026364845098 * 10 ^ 70 + 4757850078323162709893276741781579979646143950897022068881715027787201) * 10 ^ 70 + 828701428296131400498272619975530128280969387120579743611873323540685) * 10 ^ 70 + 7695496543945508258143839733768900618832779620223259208270179451250226

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_146 : Polynomial.coeff recurrence4Scalar0Exceptional 146 = -(((53321778639349609961287241189123102540014629649399522039028 * 10 ^ 70 + 8891680059861608691207636679954485307779522487762966551332525277795377) * 10 ^ 70 + 8636309461250488692825104168330951223146752609353784940776180924924508) * 10 ^ 70 + 8771915103389334599339321339255776611276276195592535087316935737816433)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_147 : Polynomial.coeff recurrence4Scalar0Exceptional 147 = ((148145192193389347716013658010403925038102193913856346225680 * 10 ^ 70 + 1560537361128273093550957520857430231110597135740125148388973571368776) * 10 ^ 70 + 4885844824201729070653552994776399465017865099173426060353330206777405) * 10 ^ 70 + 308394708458831923331008385156745425828179760109259522168691370929740

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_148 : Polynomial.coeff recurrence4Scalar0Exceptional 148 = ((8858747902837176838704712798569762352939469395143398933900 * 10 ^ 70 + 8280211110271643345161436345777067009308801675654160697897882996975494) * 10 ^ 70 + 5391089062755268912123088702627185643997978693510019839138322274597551) * 10 ^ 70 + 2004744027546858163710666695318766797525951779013543454637971749299348

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_149 : Polynomial.coeff recurrence4Scalar0Exceptional 149 = -(((4345144879657225118539848697355361739566843503862784901319806 * 10 ^ 70 + 6290233092450183977823466558858892762794997858703524869153001305553772) * 10 ^ 70 + 7958764228324722811107379493810780552445447004037214627995881506038043) * 10 ^ 70 + 6283078241518594093328971582140090614238811194460699091276407471825284)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_150 : Polynomial.coeff recurrence4Scalar0Exceptional 150 = ((44534335499011274792604743045930267129177137180162788617543768 * 10 ^ 70 + 68069610850980754333242364965829710808966152439445759459382942848765) * 10 ^ 70 + 3587747062143021056714337505715646503549474661910456187704152622063592) * 10 ^ 70 + 6687547193123782501385249941110770090043206636563833858690009805391967

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_151 : Polynomial.coeff recurrence4Scalar0Exceptional 151 = -(((335290507815370934650229541441363389548201767353752431193511274 * 10 ^ 70 + 8306408390490167899504338814505005517610757530137443914365720958254720) * 10 ^ 70 + 8321693785495510927331645056637808657428971400375224215409584419013827) * 10 ^ 70 + 2589903423515495271249578241483337757626799028038829833153017903784586)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_152 : Polynomial.coeff recurrence4Scalar0Exceptional 152 = ((2193870983886661790925920221629841434854485026128524925417653166 * 10 ^ 70 + 7951616129378018835180668424760967946164948388398977986403822231406428) * 10 ^ 70 + 4278218557086371705572989465299262827144914496443897736870108071156127) * 10 ^ 70 + 6603365652896664040322143849889522098513842774340936547471744760085657

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_153 : Polynomial.coeff recurrence4Scalar0Exceptional 153 = -(((13161394934085108466223315810808078006569805766675765052579229549 * 10 ^ 70 + 8599850835324190702009663564515654147876901377560956015610992963537316) * 10 ^ 70 + 1192062474865468266969381828545008690737200303939453725754437836583974) * 10 ^ 70 + 7358075154952499031957517795312882758519055439669690988797088945318290)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_154 : Polynomial.coeff recurrence4Scalar0Exceptional 154 = ((74167697810815651415083232815949558049967740848435852090576524847 * 10 ^ 70 + 9710610866411192545347358971086419433412805216419166331878955742923742) * 10 ^ 70 + 7036100261718348202348963031742165944938472189454611249380504734036832) * 10 ^ 70 + 668144809474936176658558478923103239740517737175364850418028128142263

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_155 : Polynomial.coeff recurrence4Scalar0Exceptional 155 = -(((397805529588867740913474872140290253186183076461235921392950154851 * 10 ^ 70 + 2865092389462095592929729717041502436981139979076052254558232846865099) * 10 ^ 70 + 4180435967559718269250144506155658490340117808682980166916676895978152) * 10 ^ 70 + 3566218679380197345597127794297647713739655403252360592985889886749184)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_156 : Polynomial.coeff recurrence4Scalar0Exceptional 156 = ((2047206273230705790819385109938306737199141344915158681206307074166 * 10 ^ 70 + 3506200099616538713024519091444996779112609511765131991602606171780174) * 10 ^ 70 + 5607798394034262742331855681397184351129812077465801699308764837259409) * 10 ^ 70 + 6373643341299680519837676877719150318213611105147442089123332408857412

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_157 : Polynomial.coeff recurrence4Scalar0Exceptional 157 = -(((10162398113327776408312379863997450968344995430850942305630404562101 * 10 ^ 70 + 7302727169540122690417075004432607153229204497165300767546030700740652) * 10 ^ 70 + 1310912976492229977251095403762429857453200134409292489774953883902168) * 10 ^ 70 + 1862437975728570097421106006652071620553497308604915514288582861314676)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_158 : Polynomial.coeff recurrence4Scalar0Exceptional 158 = ((48842167668840109419002202072065562814549164566763521347223340262143 * 10 ^ 70 + 3791061348325837339739704496126071095545471719907404791145463423011695) * 10 ^ 70 + 4972156574639744868971426985405984848218827951207711615655009547937820) * 10 ^ 70 + 7555892063773609110152598959042519819085257053298977159749341957084843

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_159 : Polynomial.coeff recurrence4Scalar0Exceptional 159 = -(((227901929488198334198612273911713756897984482569408746819611155251972 * 10 ^ 70 + 7369001310465130014298550932208806868275839194721745052286337316227968) * 10 ^ 70 + 6059376065421138377729242657593467567186865450497104381570004471979041) * 10 ^ 70 + 9594723396884536294663173934180604559203152286181971012776371212920903)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_160 : Polynomial.coeff recurrence4Scalar0Exceptional 160 = ((1034575260172772363413031636265294649458159822056242723780325810137194 * 10 ^ 70 + 3838575377344030497171939041073602174846864821622651235806862010984082) * 10 ^ 70 + 380497451877477990646187267024395383610135140299907813216697425683213) * 10 ^ 70 + 2275991645400432229643842009823919049922568719079418839732081305998983