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_217 : Polynomial.coeff recurrence5ExceptionalProduct 217 = -((5070482550850203078757624800799395027124366673431084398 * 10 ^ 70 + 5858877902872864847497375410745638099225299708758369648007854245644003) * 10 ^ 70 + 8607354239109623600758278273469459396379415496204811880332909405738081) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_218 : Polynomial.coeff recurrence5ExceptionalProduct 218 = ((288946140221074925913783390082056952946702886536472804 * 10 ^ 70 + 4638997073409385008221950124966986492483640276858667425328401300737121) * 10 ^ 70 + 8308355287633308925482140896481011148464186063813258407284250365241157) / 2730860674060914803335210

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_219 : Polynomial.coeff recurrence5ExceptionalProduct 219 = -((1559516856401783808406186144230137657870768244770491230 * 10 ^ 70 + 2948926274812916954570201417753754442402152552704736332975481179816899) * 10 ^ 70 + 7680543966009412916285024323748702945027163699196439380970303361384369) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_220 : Polynomial.coeff recurrence5ExceptionalProduct 220 = ((1061118122447802412630444742756542691473910135480887 * 10 ^ 70 + 7826072951798555441755181027171662204023356075100368137614807138732123) * 10 ^ 70 + 7340425228207280722650243811021154929728259084862971872364307572024337) / 36903522622444794639665

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_221 : Polynomial.coeff recurrence5ExceptionalProduct 221 = -((71516164987597372171854704023613009095388979897193528 * 10 ^ 70 + 4627430340472234704123218057773727569665220023571886134874111549869061) * 10 ^ 70 + 1346911174038669347925039254588694126585085364379535571581449415250293) / 5461721348121829606670420

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_222 : Polynomial.coeff recurrence5ExceptionalProduct 222 = ((34041848286384043762521429706262378453213306693785172 * 10 ^ 70 + 9785983990596136321416582957886693296263542855662638088960456994576071) * 10 ^ 70 + 7881450158943760747175128363264388882600382107440856525467726477085119) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_223 : Polynomial.coeff recurrence5ExceptionalProduct 223 = -((31219564227976864961831366254199310846357003887391946 * 10 ^ 70 + 5673241802178421516658400061156639407661607722330868037249474089340127) * 10 ^ 70 + 6106357901958565689552349648109630785920901025378035638535958275235207) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_224 : Polynomial.coeff recurrence5ExceptionalProduct 224 = -((11872846567389193413470497031519867128243835055286554 * 10 ^ 70 + 6919147666462503657688530328023650431612266644835666275137908391296640) * 10 ^ 70 + 798673164738884944454157513082499745481303623286154007875705710173717) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_225 : Polynomial.coeff recurrence5ExceptionalProduct 225 = ((6157685242010434365628491730243632301298246415445269 * 10 ^ 70 + 3451310266288562892339843868468404100695028336829783685201969584760785) * 10 ^ 70 + 8311663440871132358532572215369851221420168627390577390201586084112878) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_226 : Polynomial.coeff recurrence5ExceptionalProduct 226 = -((1209861510958004671729556997259003514982764991860935 * 10 ^ 70 + 8133334224523343868276514176284778434488021212196465600263991153867356) * 10 ^ 70 + 8817606629076077146761806650287141870943874923441669630680448919985936) / 1365430337030457401667605

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_227 : Polynomial.coeff recurrence5ExceptionalProduct 227 = ((9616808805340933970126087043298627335244162847631832 * 10 ^ 70 + 6254859993345707663407106735341956854986845694981038933154176150840821) * 10 ^ 70 + 6292026699940389650587206278211638042182967530301582460777518710547361) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_228 : Polynomial.coeff recurrence5ExceptionalProduct 228 = -((3420771113053639637790289276517521711030591344378825 * 10 ^ 70 + 7839993708115489144389044512896684141174007004193432664566241800644452) * 10 ^ 70 + 1156838249971625253441814005134668090344555251307120057933755120873908) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_229 : Polynomial.coeff recurrence5ExceptionalProduct 229 = ((2260152896061157399703049277372064059593330288716395 * 10 ^ 70 + 6570137826954742679323601984425689070828776806377581651741847202534283) * 10 ^ 70 + 6346041289306391795710037541684917129519317798176684848116195157022321) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_230 : Polynomial.coeff recurrence5ExceptionalProduct 230 = -((225736921729731441998231991095975373139839858189377 * 10 ^ 70 + 3343699235997929635298262226392363039038912780745612386532765440915634) * 10 ^ 70 + 4211557315627901200389381013012621726457552961628396575565138534013545) / 1092344269624365921334084

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_231 : Polynomial.coeff recurrence5ExceptionalProduct 231 = ((18146582467884456048353412200525823356689585103335 * 10 ^ 70 + 2888121975198876264967999864986031194466304787671201598824087388485251) * 10 ^ 70 + 6950385659116482529457847048270821039604404564449707518499381744705277) / 147614090489779178558660

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_232 : Polynomial.coeff recurrence5ExceptionalProduct 232 = -((382171355022271373833211197042595326594271197862386 * 10 ^ 70 + 7882333896203668333044827665040502047351242921797370991338974511475882) * 10 ^ 70 + 6951408239832536861212517906615307072991412000832859487853516357140957) / 5461721348121829606670420

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_233 : Polynomial.coeff recurrence5ExceptionalProduct 233 = ((260417267355248839517936601641377575194663733929112 * 10 ^ 70 + 6211626681524470531257082789794367560209995472042903887506069409404902) * 10 ^ 70 + 7398403726901102145027227738466523109587447384736328669451253169731939) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_234 : Polynomial.coeff recurrence5ExceptionalProduct 234 = -((271406562600918517635085534154738553383601079766841 * 10 ^ 70 + 7122006202770119533910551102058962644067774575243813647268326483349358) * 10 ^ 70 + 4353902174575727339951076634800977801578805018657461430052097239360051) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_235 : Polynomial.coeff recurrence5ExceptionalProduct 235 = ((67237834512160507410019014093707965404411483999835 * 10 ^ 70 + 773790645447431328526944681916904163405783201237509942728684010072473) * 10 ^ 70 + 2884240299691673962693483123378220299762812360874216173239104524960401) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_236 : Polynomial.coeff recurrence5ExceptionalProduct 236 = -((62670653259752800453199223162653886023486526404455 * 10 ^ 70 + 1775129100262826448401536487710406805055078910683123840615432966696890) * 10 ^ 70 + 3021831509520958775908271339745427582509024237772201466611807880763239) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_237 : Polynomial.coeff recurrence5ExceptionalProduct 237 = ((13438315060508488608279301390524427718846115926528 * 10 ^ 70 + 6766498062697574224264565640315551223228040894385418787734364865854257) * 10 ^ 70 + 6283013813836036364966356564323731392018027121231343279921293332607762) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_238 : Polynomial.coeff recurrence5ExceptionalProduct 238 = -((20171738999129629789301699712832224255262985289059 * 10 ^ 70 + 2171992953928730295996547079582311266178170997418417307463263893004249) * 10 ^ 70 + 8410229637261611869221372093115194911924053073290552710220336739727299) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_239 : Polynomial.coeff recurrence5ExceptionalProduct 239 = ((1129769227090160106100488426354442413089971739550 * 10 ^ 70 + 6906956482887005102704500546040606625177606203163176648594424552261926) * 10 ^ 70 + 9990452425232001292155302168950250539161039944215221073374775458356919) / 5461721348121829606670420

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_240 : Polynomial.coeff recurrence5ExceptionalProduct 240 = -((122152219531884218427113440220902802242390249059 * 10 ^ 70 + 7449332549416272631287998316883651207942245832021004698087404863818720) * 10 ^ 70 + 735802733304460727194765772759743566987856097293222465894509692496849) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_241 : Polynomial.coeff recurrence5ExceptionalProduct 241 = -((370904966307534017587460108639459106086401245916 * 10 ^ 70 + 8403616590041230864164232868809451362785569452885824158394300858641271) * 10 ^ 70 + 7383908865689453899514877263534274241238409719395191481401469659925846) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_242 : Polynomial.coeff recurrence5ExceptionalProduct 242 = ((15784082812049157810777464245359080510602259348 * 10 ^ 70 + 2286151442298619731119205583324520488622521043075338184535400665297786) * 10 ^ 70 + 4572602195774066960467242771036040002090300085042141119326998259238979) / 273086067406091480333521

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_243 : Polynomial.coeff recurrence5ExceptionalProduct 243 = -((122015221468542672921180328702166432479260408712 * 10 ^ 70 + 9850742315873242057282395396014234920013461415352489244329616519370543) * 10 ^ 70 + 4697166702067502333389898503183399054321039223371446939763692715757151) / 2730860674060914803335210

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_244 : Polynomial.coeff recurrence5ExceptionalProduct 244 = ((5548496032035726759335203390340142661739782148 * 10 ^ 70 + 3271141086842481731630062681853782238795212115388799619890763849877503) * 10 ^ 70 + 3969209827613241776684453713712559713009077795464302354464527190389239) / 184517613112223973198325

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_245 : Polynomial.coeff recurrence5ExceptionalProduct 245 = -((127125497143243129407538924425440360718545909359 * 10 ^ 70 + 7284877449811338283152334258922587408104364598894567979267028569565178) * 10 ^ 70 + 6151641250204998347996322349862251111839610821509466243532303142497021) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_246 : Polynomial.coeff recurrence5ExceptionalProduct 246 = ((74203125618687313903259117262728547938857609842 * 10 ^ 70 + 6358934865307055621807433518324937912152588868663021331962536573928498) * 10 ^ 70 + 4099839704290210865307772677347135189751342405164030292817022907132667) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_247 : Polynomial.coeff recurrence5ExceptionalProduct 247 = -((82686797307359042204723069303186694425426607502 * 10 ^ 70 + 5327214978265806138905103376657245045325169076155265988265153912229048) * 10 ^ 70 + 9895310045642778023768361616746165583760687317254457672151851997375607) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_248 : Polynomial.coeff recurrence5ExceptionalProduct 248 = ((88585692379919792742907096109898708932906179077 * 10 ^ 70 + 5645099785518199390541628389692728072835030342159082966874237808060853) * 10 ^ 70 + 2754103233917176718821291689122377802718040086762551602649928040309361) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_249 : Polynomial.coeff recurrence5ExceptionalProduct 249 = -((1238324342516331305356794521060059031034480149 * 10 ^ 70 + 4628662168613444311386649314750479009759117304220364646773065648125793) * 10 ^ 70 + 7966683968414895404085968538801698752804161623603446958228013792593903) / 738070452448895892793300

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_250 : Polynomial.coeff recurrence5ExceptionalProduct 250 = ((22939939938366466088059176593426439720420922153 * 10 ^ 70 + 3440116717252511477026977236486759652653493305568839600861297607646226) * 10 ^ 70 + 7767458404008077287797538797786194812149128550712661471048252581274053) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_251 : Polynomial.coeff recurrence5ExceptionalProduct 251 = -((1113385237852696679339597935472502150288223392 * 10 ^ 70 + 1525017169565626267655935659239549822713904855062757654047506822539600) * 10 ^ 70 + 9169706039579979550760373569825217091028178304820338283548963357877493) / 2730860674060914803335210

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_252 : Polynomial.coeff recurrence5ExceptionalProduct 252 = ((5241481104901005885139991478215545639776850401 * 10 ^ 70 + 6314797272855634812340508647428665860229403394277261775673728400363212) * 10 ^ 70 + 6866793710349891111000266523701940854005872949758958595859313619837891) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_253 : Polynomial.coeff recurrence5ExceptionalProduct 253 = -((2393298990011923877869085227606642614516930252 * 10 ^ 70 + 7214451142179188684550530218728104346949207770366909637667890725568428) * 10 ^ 70 + 3999080081048880086185082965354586222590356637847737616982258894260963) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_254 : Polynomial.coeff recurrence5ExceptionalProduct 254 = ((21185536398430754564553637156121286664315086 * 10 ^ 70 + 394777261858938948761455370259762680778608945313944298091102612154364) * 10 ^ 70 + 9399607009753644846493888351567309090646012033611245461321796136902611) / 546172134812182960667042

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_255 : Polynomial.coeff recurrence5ExceptionalProduct 255 = -((90785794088554341845199320272999388843294511 * 10 ^ 70 + 4702170730576612936893005097336649259097524448575612401950138060443751) * 10 ^ 70 + 3573233544156950576577118147435090670662503676404585971021641810231739) / 5461721348121829606670420

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_256 : Polynomial.coeff recurrence5ExceptionalProduct 256 = ((188002813533716024357331800438560400199256279 * 10 ^ 70 + 3688697403374588054999505196859235144117336319273719944800937641857792) * 10 ^ 70 + 7000462163146438801965175491478863906891343587182382506812220608442081) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_257 : Polynomial.coeff recurrence5ExceptionalProduct 257 = -((37532945857685448257140745965872449868773253 * 10 ^ 70 + 7478834001300284572535432565255152706076025976818969808304608334265196) * 10 ^ 70 + 2368860222121756099682831290588245623041147225234427704492006880190029) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_258 : Polynomial.coeff recurrence5ExceptionalProduct 258 = ((7198038623395290171273740478178289363570472 * 10 ^ 70 + 5033877273424564093303100998882632025720670205482127524189348718285761) * 10 ^ 70 + 5658430063075917950314014965359695761937325674428567638811190665721509) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_259 : Polynomial.coeff recurrence5ExceptionalProduct 259 = -((5277098359900864882986637346962308606269849 * 10 ^ 70 + 2107433341525904257105614030087988163342768820528635314061834998108668) * 10 ^ 70 + 5595669522968630980327599284644435524299037169326157080202661803951231) / 13654303370304574016676050