Recurrence 5 lookup certificate: ExceptionalProduct 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.recurrence5ExceptionalProduct_coeff_170 : Polynomial.coeff recurrence5ExceptionalProduct 170 = ((176564060583295611604591346318625106725055219499825040330 * 10 ^ 70 + 4311395446618950385148756435469563827994376123261116803808973539793133) * 10 ^ 70 + 7450697376499682758376590821083131179744805037185951791978427560713403) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_171 : Polynomial.coeff recurrence5ExceptionalProduct 171 = -((122095297299354422595413866811002513004141910232334714109 * 10 ^ 70 + 2173954020130588154403437378640252392005803436981662526291412380356352) * 10 ^ 70 + 8882722709217834684122577362160592486945399753427084683172824918220986) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_172 : Polynomial.coeff recurrence5ExceptionalProduct 172 = ((65808060524211987551615109281848226305117130223416970161 * 10 ^ 70 + 3148372953984118496872489855845525600133869539712863826348448900394651) * 10 ^ 70 + 1094052620195265718891481597077037092631057351437286862347966880978781) / 2730860674060914803335210

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_173 : Polynomial.coeff recurrence5ExceptionalProduct 173 = -((86363853837619794731915528394531319203005152424113120054 * 10 ^ 70 + 6912194550332070183592907182306930704864968520968069099479663540561191) * 10 ^ 70 + 4156022628600593228675986512244790722559828591326802645910907191640133) / 2730860674060914803335210

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_174 : Polynomial.coeff recurrence5ExceptionalProduct 174 = ((1103355831416844124742610914949931851491677648313367330106 * 10 ^ 70 + 6354161326213061715261308245346437249958262813854223340055267898555851) * 10 ^ 70 + 3291987024348595938789346664524575102392874848620853078834811684130191) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_175 : Polynomial.coeff recurrence5ExceptionalProduct 175 = -((1371438345241220324024992749611403721730980142714055388592 * 10 ^ 70 + 3706816958764843625513008084685754286053355621861176987036460506173540) * 10 ^ 70 + 8474773833730530570658853377667790755964796784068286487782231723100443) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_176 : Polynomial.coeff recurrence5ExceptionalProduct 176 = ((828638485308582983235121437431536479603052756204480959416 * 10 ^ 70 + 352047508018954799901421893251403802711200100843414827438663022107082) * 10 ^ 70 + 8558274038482928575180451907697782308302032529169398891184173265066629) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_177 : Polynomial.coeff recurrence5ExceptionalProduct 177 = -((1945215798171370786464324163657833102787814564705650558401 * 10 ^ 70 + 6463497225329630560829037895876832862861399649243878975772204021983706) * 10 ^ 70 + 4560439004073791180890331711254338124621639770066397676376464598019657) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_178 : Polynomial.coeff recurrence5ExceptionalProduct 178 = ((443002590431115668398707689841739076855829403289814010585 * 10 ^ 70 + 528759041013192065964354275660567964189957780929457397868845436074218) * 10 ^ 70 + 9292853463455867974045137776169834054169829054956315793738938848966961) / 5461721348121829606670420

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_179 : Polynomial.coeff recurrence5ExceptionalProduct 179 = -((1221562967672802961089957298333343708165130611542022618209 * 10 ^ 70 + 5837985738665287338485504192554824297216042917033519650425618019590301) * 10 ^ 70 + 8762130811768545462669858009520584403864628376145559782750938461128621) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_180 : Polynomial.coeff recurrence5ExceptionalProduct 180 = ((651207205728594260480570320535550700690782226578979486023 * 10 ^ 70 + 8016577757701386190820253392762998563995022863988043719049884233679798) * 10 ^ 70 + 5049826568197174914172736797563160700019527782163623102994629643856966) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_181 : Polynomial.coeff recurrence5ExceptionalProduct 181 = -((669251808165016205327247363065153920736835213375274524789 * 10 ^ 70 + 8073235569276777733861894083622825935364038960205904031939308177363045) * 10 ^ 70 + 2420545700008655367761028030490304687806909451558232978189391753524748) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_182 : Polynomial.coeff recurrence5ExceptionalProduct 182 = ((528261533663734782633860999341333974659999155638381523538 * 10 ^ 70 + 5170819237029227152054777054212571763081925504400393584613786016488533) * 10 ^ 70 + 2194635478964658452035684409335582659509061450764804552054403806617671) / 5461721348121829606670420

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_183 : Polynomial.coeff recurrence5ExceptionalProduct 183 = -((2487179144664415611742669124747685104173729820099333626129 * 10 ^ 70 + 2252810607839689286025731925025230967162594617568964511088694534261504) * 10 ^ 70 + 444572697051892550208617634430079342355798793485460668807132972605861) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_184 : Polynomial.coeff recurrence5ExceptionalProduct 184 = ((2214276576701147336802474906325754461461971638289451016394 * 10 ^ 70 + 5585913134055381300447168964238942065879309953865553084821575050160782) * 10 ^ 70 + 2433884989393620914093999554526180283984260775644749085324279948818401) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_185 : Polynomial.coeff recurrence5ExceptionalProduct 185 = -((916863540417391722879918751811456488849053750227917024268 * 10 ^ 70 + 520243116029827609131381333172965513442721854897020527526128694467559) * 10 ^ 70 + 2532738767783782106938292849529525880581923631983127575053196211893059) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_186 : Polynomial.coeff recurrence5ExceptionalProduct 186 = ((683950969215806748418808178790105242544553548055927159363 * 10 ^ 70 + 3639784736659159194289388431064675986933975523573184021360724484866959) * 10 ^ 70 + 3649910756205729903732855942479894269641421510645697330116545748603491) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_187 : Polynomial.coeff recurrence5ExceptionalProduct 187 = -((424286096974893387615709684638877864314873121653578603807 * 10 ^ 70 + 5155880973545304995314378277716101877906778809672919746242714403473727) * 10 ^ 70 + 5403564051527112202637670230720703097363199817664504622858366616910451) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_188 : Polynomial.coeff recurrence5ExceptionalProduct 188 = ((12544508487834933400907522683583430027988390550752681463 * 10 ^ 70 + 2924749271379776924163513194322285223421628010787181945275036753099547) * 10 ^ 70 + 6779705604719281409887257033025227930252598370300711721577696016428527) / 1092344269624365921334084

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_189 : Polynomial.coeff recurrence5ExceptionalProduct 189 = ((197301636642598366452060541627438512638104171507439095492 * 10 ^ 70 + 127501301820653256257309105678513767204822242598366418095378435258116) * 10 ^ 70 + 5602259231092925416859896822803090416099074962067507580014529766617751) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_190 : Polynomial.coeff recurrence5ExceptionalProduct 190 = -((4374029744452872475865386704037260510387444672680260656 * 10 ^ 70 + 5842828160546004297591603542754554023963243913675994458234974924153199) * 10 ^ 70 + 4229535555505574395473146108686690173887604568617608903438482351191921) / 184517613112223973198325

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_191 : Polynomial.coeff recurrence5ExceptionalProduct 191 = ((1006877411572929582254531550321539548469443238815478176090 * 10 ^ 70 + 859630988459197028039777522672647573758352260475341343511410678437778) * 10 ^ 70 + 9419579973932852010500184714309745433559216260105128290319373054922527) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_192 : Polynomial.coeff recurrence5ExceptionalProduct 192 = -((314138060283410746178108028676687659872419826587144831886 * 10 ^ 70 + 1217657696357426356217934503345142913951762031960781327667022660080758) * 10 ^ 70 + 2004406158315837955460344247418354299690593203930027932632783851889629) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_193 : Polynomial.coeff recurrence5ExceptionalProduct 193 = ((1389109641408994380267292878955575699243593714259234330688 * 10 ^ 70 + 9767767804055476755130414622201662827994982660939564192458665960868715) * 10 ^ 70 + 9705348319231037038264974689278692232984950689339210077501512951460363) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_194 : Polynomial.coeff recurrence5ExceptionalProduct 194 = -((352314912723856538046496057057963255891085998633299383448 * 10 ^ 70 + 2574295906640118844349483789015432543938466210710074379454835796767263) * 10 ^ 70 + 4794855422879194036522647585516351687279081838511485855636651871643958) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_195 : Polynomial.coeff recurrence5ExceptionalProduct 195 = ((1332011959701253856120909787744141744190322509676221586801 * 10 ^ 70 + 1863106261209456619746331343222381455286263430728916402356832507693479) * 10 ^ 70 + 3172595603775803240214514300242401777059242594024027351274656833194269) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_196 : Polynomial.coeff recurrence5ExceptionalProduct 196 = -((294941212171164783351540503702674942053384825290463566398 * 10 ^ 70 + 8172520745952389855161809842669732172310657943559495071870506024199042) * 10 ^ 70 + 5382253714154790346605350804585892515776231270841121891344354109791439) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_197 : Polynomial.coeff recurrence5ExceptionalProduct 197 = ((978735930169395159834751928266862236771698522536953472339 * 10 ^ 70 + 4899330785092837244333672116906080537695627192834630621394331234929028) * 10 ^ 70 + 5464754744799691927279966230152364689157536144474214463106211442328729) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_198 : Polynomial.coeff recurrence5ExceptionalProduct 198 = -((188839752835450207643961579913655377279618970153533426669 * 10 ^ 70 + 2005874554173731559645633475499807673342488981662596968396362715031088) * 10 ^ 70 + 5409939165848410477384378720922637737211025251638245799291553472005157) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_199 : Polynomial.coeff recurrence5ExceptionalProduct 199 = ((106640007935848387859526792803514552818133277505449914953 * 10 ^ 70 + 9097750536455730268454781913075797988466191321404145415899063069542128) * 10 ^ 70 + 8607571643561780489766845550613420495576108803045796809044351243767673) / 5461721348121829606670420

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_200 : Polynomial.coeff recurrence5ExceptionalProduct 200 = -((165389314995804490270744810209392437888966292175427914427 * 10 ^ 70 + 9721969581295321166945579199838550370226641763590108474515130142079379) * 10 ^ 70 + 3529348488476148827114437081824787039088949810750610176344721512897643) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_201 : Polynomial.coeff recurrence5ExceptionalProduct 201 = ((32093440296294080387453470996170135917109519825858727763 * 10 ^ 70 + 2497049294282258551589897991832705799720519572007057976555278011819260) * 10 ^ 70 + 2641483014428493453556650245920088836758130618037450148344533893956793) / 5461721348121829606670420

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_202 : Polynomial.coeff recurrence5ExceptionalProduct 202 = -((7107105732437074804307072951582324083416016657198051393 * 10 ^ 70 + 5945822564512927759720359293427205517833907745707109148706199700651194) * 10 ^ 70 + 7222869598263770585231528412677288242656505001894448762530287757711088) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_203 : Polynomial.coeff recurrence5ExceptionalProduct 203 = -((64614152578022965381822761971222665974277444415571169218 * 10 ^ 70 + 9351085342118233218195372256713401913937348167727047806513394072573979) * 10 ^ 70 + 1985372292258607857409949777959635688720477349326584563560241469671477) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_204 : Polynomial.coeff recurrence5ExceptionalProduct 204 = ((61036359811801735833932818398556882083641078147441089066 * 10 ^ 70 + 3259063203373194620569825815016722739083058893297276799049619836990334) * 10 ^ 70 + 6732848526981150274578907698750735314747436122325485062871385825927599) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_205 : Polynomial.coeff recurrence5ExceptionalProduct 205 = -((5999184678583558489745402789712247427225573008141357044 * 10 ^ 70 + 6309128267709248839419160173096222734915811986187898244692388533410639) * 10 ^ 70 + 3172767198466575935017161071140888509872991402609955026935617090670487) / 1092344269624365921334084

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_206 : Polynomial.coeff recurrence5ExceptionalProduct 206 = ((77768609187864365056909926365518623453124299692423242508 * 10 ^ 70 + 6918914250081443007298244645206525079180526699666881140985545887400525) * 10 ^ 70 + 1790656499761870169284942855724785697764915142529251415233256904074761) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_207 : Polynomial.coeff recurrence5ExceptionalProduct 207 = -((145928667040997265593647979055774383961762168667709801504 * 10 ^ 70 + 2565807343539096135822997262541196502242340804568676340050709009731938) * 10 ^ 70 + 3880979238964481798594881796919090503849117400874635217191014833547573) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_208 : Polynomial.coeff recurrence5ExceptionalProduct 208 = ((63744454961156101618997382866366671275022237167234475753 * 10 ^ 70 + 8194008547233149987367657898139429206726003389790815353393421656079585) * 10 ^ 70 + 4282728141109854800489971719892710307697652494365469811977746238293231) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_209 : Polynomial.coeff recurrence5ExceptionalProduct 209 = -((2844551217047169228062096504368828618905588949464472094 * 10 ^ 70 + 3982769411649052373870180496429162545129096349083553794511841553779576) * 10 ^ 70 + 7629428166312386711238809056713733599942229588911555510800007890186449) / 738070452448895892793300

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_210 : Polynomial.coeff recurrence5ExceptionalProduct 210 = ((41398964653295608844094650420697524363965139747955737250 * 10 ^ 70 + 9663198511029406992623727178667339659886042013413185434991837409071285) * 10 ^ 70 + 984254130971308898965489078950227833397184399714633110032721811239071) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_211 : Polynomial.coeff recurrence5ExceptionalProduct 211 = -((62388009182437979225359372710959813529240276402824406644 * 10 ^ 70 + 6562816422491793255783444839172018435396474075185400527084706084436761) * 10 ^ 70 + 5545496820281874327373606857657653724551032067727549854517137519856443) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_212 : Polynomial.coeff recurrence5ExceptionalProduct 212 = ((11291819889088520304926013963041297316061500035955696859 * 10 ^ 70 + 4621023304462993028386680273596003627557217125166339658972146255068982) * 10 ^ 70 + 1329063142426577457429798190925311120480029715231412865838472482698058) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_213 : Polynomial.coeff recurrence5ExceptionalProduct 213 = -((31475689477903277185047671605095951840568482305085407332 * 10 ^ 70 + 3435073824786003063365134055900121639798564056732323167313042164195723) * 10 ^ 70 + 7568718400337067265758282010736812831776511597267793789707634835668751) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_214 : Polynomial.coeff recurrence5ExceptionalProduct 214 = ((21129697979458854234216058213218062337239788240186420732 * 10 ^ 70 + 185557606096761426769099316109085021364531674841234540118431046461528) * 10 ^ 70 + 7652132539580782660363228604020573706896550810618666524053349334900971) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_215 : Polynomial.coeff recurrence5ExceptionalProduct 215 = -((3415400207133351596665287948288100077742193614386964947 * 10 ^ 70 + 3878972704720941573073551157712403519841095718958159359594927786388995) * 10 ^ 70 + 3488943248055889863565938622966744676080951581788141059354874086204099) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_216 : Polynomial.coeff recurrence5ExceptionalProduct 216 = ((1699397976093900413393487945077241043013702642031945175 * 10 ^ 70 + 6722502256974818605494011830398896170054455077767423602568446619537424) * 10 ^ 70 + 5784557996733020767866555827537766038584203607122163472854891246060329) / 5461721348121829606670420