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_184 : Polynomial.coeff recurrence4B3A3 184 = (113171357813573950029975782630233896998737132963321864896592971 * 10 ^ 70 + 5972410495284659864547159101339884584795235558985699148257501958973724) * 10 ^ 70 + 5655015987922850811718250067782403951354097118814902569087202455715532

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_185 : Polynomial.coeff recurrence4B3A3 185 = -((113060425448399150664858913237556636669612210870477656391975524 * 10 ^ 70 + 7754915411513624202775706966982110777383089819480021462997009530541413) * 10 ^ 70 + 8080622430977139820059212745698185773587937937123407161249983548811691)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_186 : Polynomial.coeff recurrence4B3A3 186 = (106704165114835408531240882077335676792561919986853009003467663 * 10 ^ 70 + 3164708833286604918219342486144870758836419445222230658113364053718330) * 10 ^ 70 + 9054762632962938489054918593850882555106615184685456772197205485716388

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_187 : Polynomial.coeff recurrence4B3A3 187 = -((96184965345712154891924560528894021245427013903824133248530608 * 10 ^ 70 + 9175145628660905803320755582886972632407754180019608384617982936903078) * 10 ^ 70 + 1635862036428235757571239533723779194471663416602226783248272836041689)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_188 : Polynomial.coeff recurrence4B3A3 188 = (83362218142121391397465085058050048214687956334729897151783092 * 10 ^ 70 + 8405385533790710086465529109863579992341454926552229478545811502727275) * 10 ^ 70 + 9434857686432379232643198312714597573523483377477697002020535680719191

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_189 : Polynomial.coeff recurrence4B3A3 189 = -((69764252155390454113487667006300811408164643888885399705519543 * 10 ^ 70 + 7286533273005139095129217462913667868675629238677408524525884464242284) * 10 ^ 70 + 1898311328450451518536880192323182678176432417401941821313443661425722)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_190 : Polynomial.coeff recurrence4B3A3 190 = (56540935632121238641848571015336562433580747698590452896949606 * 10 ^ 70 + 1819632301460745558106075039296667651073055524725811880938175212038598) * 10 ^ 70 + 6466919295902065022875042579064147496931631510919679155296014161035484

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_191 : Polynomial.coeff recurrence4B3A3 191 = -((44467559576407088195268251142493473334797129406777160804676677 * 10 ^ 70 + 9333562912241234723334536209885829291320171028949800821015934574473755) * 10 ^ 70 + 7251177132119429937104201541999395587382153344023722218495422131453991)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_192 : Polynomial.coeff recurrence4B3A3 192 = (33986092081925008565846876917621049165900123558429043195986225 * 10 ^ 70 + 4799590961192246642111778503520286078759922076608844823456778061357601) * 10 ^ 70 + 8731135101630147492606278760007807221415115398882603077227079883444114

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_193 : Polynomial.coeff recurrence4B3A3 193 = -((25268602793160933642251063219001753480140246866619741344676877 * 10 ^ 70 + 9402261576839353143764652841663657713401729851980842985849801195663185) * 10 ^ 70 + 9008521347829888782046312765053484187873463954581297822742471889593514)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_194 : Polynomial.coeff recurrence4B3A3 194 = (18288967781046788902414493066718040844951539623674398090167696 * 10 ^ 70 + 4546834295197137134370928034124214907243681969427411736628627608653406) * 10 ^ 70 + 9486505797335529251033758612277368150703282946685387943192898598012253

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_195 : Polynomial.coeff recurrence4B3A3 195 = -((12891953855153549625074647631668512727748685306359169061897547 * 10 ^ 70 + 5685104670147324045471014965521584040197795356784135598047619906319179) * 10 ^ 70 + 191062346176860198004113820653780180312234069011712735920910400731184)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_196 : Polynomial.coeff recurrence4B3A3 196 = (8852480409377533299524655350663498611927748471545276161100326 * 10 ^ 70 + 6943120275809733975712501557947777026437375591953709398319070266409687) * 10 ^ 70 + 5795247362223650799128851326810205762581753584726604375876633876444428

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_197 : Polynomial.coeff recurrence4B3A3 197 = -((5921455875539114779872850154741270858508783254019853550744011 * 10 ^ 70 + 6390402028477755461600231985230964705955778075175882741357766618421047) * 10 ^ 70 + 9920889258238172443333756753496399979705586460000592267786465261244599)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_198 : Polynomial.coeff recurrence4B3A3 198 = (3857539466379532151650620041924524152847204589114163770918022 * 10 ^ 70 + 4520138938511170616467135812790883446544321245065000984953321213713651) * 10 ^ 70 + 9784390062808683493347943929676433346730869441872620520512255379736948

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_199 : Polynomial.coeff recurrence4B3A3 199 = -((2446228391240631055490017012588555209745046608919956219517279 * 10 ^ 70 + 1892512408252918813684404965923089204105412926682448015241790309127819) * 10 ^ 70 + 7975538030529776333180523414913854724122092494525760480218707095941909)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_200 : Polynomial.coeff recurrence4B3A3 200 = (1508800124841817404050897658898034517413217817627155028316172 * 10 ^ 70 + 3383949962592361381659816615094390988434245551751534749839543531280995) * 10 ^ 70 + 2671763119188454470097243496152939697034393595537051306240767811139654

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_201 : Polynomial.coeff recurrence4B3A3 201 = -((903996703770029739680713048585932128140456348367239058874132 * 10 ^ 70 + 7313278216770068125484681176565860192287366351740040368123968455049628) * 10 ^ 70 + 7450551220840892806797100812026024980630069796719683658236640378956733)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_202 : Polynomial.coeff recurrence4B3A3 202 = (525150741921324509368020946664079149176732231913057630249029 * 10 ^ 70 + 9149740436661558376633160755738037129480193568144778966084619462111238) * 10 ^ 70 + 7506589683577138639349931582270261889446792485120391890898059324578639

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_203 : Polynomial.coeff recurrence4B3A3 203 = -((294956720890109109404730676545591314804267945982988723519879 * 10 ^ 70 + 671047023152533318122568268667613387769858272516197027859224113440988) * 10 ^ 70 + 1899078434866223502281705322139496231640998521946709697078207211789194)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_204 : Polynomial.coeff recurrence4B3A3 204 = (159483917391400096478418615366203989918328629514558912882445 * 10 ^ 70 + 3219445844903859297253408601767546848785945249869208655820391710870958) * 10 ^ 70 + 6214996875412214014053635403927949791900240045996754247460714825744793

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_205 : Polynomial.coeff recurrence4B3A3 205 = -((82447410340927915174384568246747905766109263020094969084827 * 10 ^ 70 + 3500184093687356386666159166899130383608804501828388185094849611051151) * 10 ^ 70 + 7261206963073100089508812076515585865503526529265488992020447798309082)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_206 : Polynomial.coeff recurrence4B3A3 206 = (40278431210591330038978782491176221296392765191375823101231 * 10 ^ 70 + 935625162439395971485758266310002282291243982204473305419610585947732) * 10 ^ 70 + 5782572400867866439904700723209819706710027656291449847500826081577062

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_207 : Polynomial.coeff recurrence4B3A3 207 = -((18192494151158807057540755928625671247556640030326097395172 * 10 ^ 70 + 6786727229362711895805279323672605876030334188179118231308426557831742) * 10 ^ 70 + 131220477425069131925667858932198697405287785727530336759106924781994)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_208 : Polynomial.coeff recurrence4B3A3 208 = (7237121988889727827123907283157273326195835080558229982532 * 10 ^ 70 + 6286461056226720838223738474691436279566548017716781235885498976507144) * 10 ^ 70 + 6777094799929393366393770768252171153487451328852005837512627392444331

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_209 : Polynomial.coeff recurrence4B3A3 209 = -((2186403073294317144569723141105770260063448220271144075502 * 10 ^ 70 + 3894151978612049893429395711647164113061176098872085308876190505756319) * 10 ^ 70 + 6192451514067043900407908555737226559296843240377843875341644906799440)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_210 : Polynomial.coeff recurrence4B3A3 210 = (107181253281934974758011012804139024742540675373802052941 * 10 ^ 70 + 9999613064532315399534367668505541752752399171411698643622616534724425) * 10 ^ 70 + 8416536067708894507427512289095794400349113018740130701931674829872680

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_211 : Polynomial.coeff recurrence4B3A3 211 = (576345983622770222408220894421502738234676428911671738980 * 10 ^ 70 + 3270547910367098539127651706594415642514683772183259627544371337848025) * 10 ^ 70 + 5235146082585063713786259586687256211235051332136340370946653487814969

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_212 : Polynomial.coeff recurrence4B3A3 212 = -((668212724200391626704139195026111524371485038639654328674 * 10 ^ 70 + 857112843976209795468326771587503374667793567044057479148312626288568) * 10 ^ 70 + 4018235844929937115708469450876846482119976724796935306138391976399990)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_213 : Polynomial.coeff recurrence4B3A3 213 = (552581326976597178010152827646448533026036717150633541010 * 10 ^ 70 + 4686918170684869905782767754083194719256178244971599047458018955673845) * 10 ^ 70 + 9022616849221678957156647127252050742828990876872203675911117027160901

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_214 : Polynomial.coeff recurrence4B3A3 214 = -((396514273561228305149263889446241818881727151869099717091 * 10 ^ 70 + 963378481865147420251067178425322056074214793370053673628799521621852) * 10 ^ 70 + 3502586174085354056486443600476881533679284384646802082949019280603456)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_215 : Polynomial.coeff recurrence4B3A3 215 = (261688463192346639277298366685416834299094369877645314046 * 10 ^ 70 + 1780751041369909840544549745545474104504856627191243527900077271114752) * 10 ^ 70 + 1127677630388275401403717776953134169044057440621934199083012326177612