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_277 : Polynomial.coeff recurrence4B3A3 277 = -((3063651656732604211931989007504 * 10 ^ 70 + 8821460794853623261748518383760504603639349093530628470920505606808284) * 10 ^ 70 + 8436074289495589486318098692498506688810772608650235061229075114649265)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_278 : Polynomial.coeff recurrence4B3A3 278 = (1709176358855942704205178355329 * 10 ^ 70 + 9228204533384163457438416703750733016285572122389797574863418398685927) * 10 ^ 70 + 1300246899587191090477217816277164482093420137997879455051817548426010

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_279 : Polynomial.coeff recurrence4B3A3 279 = -((801147130009384020618825547386 * 10 ^ 70 + 3384774184793584637731471728151228670129775938948204110430095284262357) * 10 ^ 70 + 1250899189525791480968042486754863592372502836456232193911782024611796)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_280 : Polynomial.coeff recurrence4B3A3 280 = (339179497499419693617083899494 * 10 ^ 70 + 6425093802959113444218645521649656109621986585807042680211337433004152) * 10 ^ 70 + 6215236772323427575931174630477379364882483837851500186219313823304389

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_281 : Polynomial.coeff recurrence4B3A3 281 = -((133190659108577635940029708535 * 10 ^ 70 + 6835320184426083940406224530836709265143116703511565673039553877469120) * 10 ^ 70 + 1070449264324448178078715136777499277835829410408785305942192839574596)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_282 : Polynomial.coeff recurrence4B3A3 282 = (49031773633884792131835172574 * 10 ^ 70 + 7454786701153031625403563860699162773246916175170811686368867488296252) * 10 ^ 70 + 3041837531041888075027175934168485101258264203697113873993999471617251

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_283 : Polynomial.coeff recurrence4B3A3 283 = -((16978750780142487890119737826 * 10 ^ 70 + 720901926555055758829143557725270029240180294182084290913288632108050) * 10 ^ 70 + 4293809757832141302902741395482247706464040242046966311080045081270291)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_284 : Polynomial.coeff recurrence4B3A3 284 = (5526842971956288697142434053 * 10 ^ 70 + 8569973776412740312385409982023582807410943730304274362747837814448506) * 10 ^ 70 + 8044970602600506499891346933016253273795549931567798039268871369546909

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_285 : Polynomial.coeff recurrence4B3A3 285 = -((1685606205006759946960790779 * 10 ^ 70 + 4218867824196998946947767262050240663511676631514378027382519343780279) * 10 ^ 70 + 9386792345057666886504606019726924097576680070135560231390144846147590)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_286 : Polynomial.coeff recurrence4B3A3 286 = (478955227310155733241131323 * 10 ^ 70 + 7172297284239046692392327528609962012712645648550711403420907004687714) * 10 ^ 70 + 3940198073388137765520109405860044411877002591683946503767859610189159

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_287 : Polynomial.coeff recurrence4B3A3 287 = -((125709655530770064706833005 * 10 ^ 70 + 3490715603479332490538587187558571837112261798616703308644435780844321) * 10 ^ 70 + 46386678468713309637799838077092320801128109939715597694704142069848)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_288 : Polynomial.coeff recurrence4B3A3 288 = (30066174556095157827243164 * 10 ^ 70 + 7815569250913873012062614953916381949550821820039958577660321790998972) * 10 ^ 70 + 9174081438140080194781560108797129404114080645833170059728055185882545

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_289 : Polynomial.coeff recurrence4B3A3 289 = -((6396769395637929617154799 * 10 ^ 70 + 4054541302359559238336997338798252960016243702243017246587611196711258) * 10 ^ 70 + 4916431666051763183123924191976475984273789705999791196404551918605344)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_290 : Polynomial.coeff recurrence4B3A3 290 = (1149855075532106373516040 * 10 ^ 70 + 4116231966957138585357307762417312344701604172279026162432603749489475) * 10 ^ 70 + 2868756569194190615448928419156656566254246937429596290460986620536581

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_291 : Polynomial.coeff recurrence4B3A3 291 = -((149492074201183622626066 * 10 ^ 70 + 7092673970349745060612034193432626500298481088107006303383143081567518) * 10 ^ 70 + 4285457614298897929220476327952912565513967774449908198556546312991054)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_292 : Polynomial.coeff recurrence4B3A3 292 = (2310863282441633168343 * 10 ^ 70 + 5097995218192528181573689083502830314371505372323888962229542278053170) * 10 ^ 70 + 1156912850446579355231826632400343669061269185446656961972967925633931

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_293 : Polynomial.coeff recurrence4B3A3 293 = (6844578954536399796171 * 10 ^ 70 + 6925907995225189375411758483674778964318883670176607919924697107454371) * 10 ^ 70 + 8378479116060402428801027098280737070398018451357885423415691289066869

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_294 : Polynomial.coeff recurrence4B3A3 294 = -((2956069200742632456701 * 10 ^ 70 + 2147764307613124254444039858617045863883342978850775216297496817613031) * 10 ^ 70 + 5841735085765825622915159570975109207479414320795764221526823765111214)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_295 : Polynomial.coeff recurrence4B3A3 295 = (870463065307669976209 * 10 ^ 70 + 9924430033750371947490872649364115957609363990778996431765871283925917) * 10 ^ 70 + 6870985715470045270258853762957585820397381655631213666758576294845962

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_296 : Polynomial.coeff recurrence4B3A3 296 = -((209872530106294757837 * 10 ^ 70 + 9508733645923161354756432881216644717124154641033818686188618474267640) * 10 ^ 70 + 5110145524214885722985553024847240506109532426575008730504772331571607)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_297 : Polynomial.coeff recurrence4B3A3 297 = (43516867137414699092 * 10 ^ 70 + 3167129813217262308436733305191692792148502684136719213449845843121985) * 10 ^ 70 + 7017136040254022174678727506478562807393863338948378660822320631526181

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_298 : Polynomial.coeff recurrence4B3A3 298 = -((7866253970758043417 * 10 ^ 70 + 1799269104689798149037990025698064781859136744944736599495809267643557) * 10 ^ 70 + 3969200786285292168444630464988156043496344409129462665128293108177167)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_299 : Polynomial.coeff recurrence4B3A3 299 = (1233903994902497876 * 10 ^ 70 + 2200949330310554560123335973404324361199910170726345507067738412404599) * 10 ^ 70 + 4354936693994909323612160624056089242541212241680219342610653274844897

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_300 : Polynomial.coeff recurrence4B3A3 300 = -((163988216554949817 * 10 ^ 70 + 7964662426214741568124438932673535959171430755294027278630207733805385) * 10 ^ 70 + 2654800770372968718797656712696447174099893601045529716210971809486967)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_301 : Polynomial.coeff recurrence4B3A3 301 = (17302811959230617 * 10 ^ 70 + 3894058452425437158367066360170527996863967229047720962562189218292499) * 10 ^ 70 + 4549702522998601085762099844005158194248926024238317779875767144768401

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_302 : Polynomial.coeff recurrence4B3A3 302 = -((1143697874910713 * 10 ^ 70 + 6961772480468243862613104142830179591142036128080228182474243386491921) * 10 ^ 70 + 7235862396504512062945989919835827551131423260547023664347101947967249)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_303 : Polynomial.coeff recurrence4B3A3 303 = -((39295102318857 * 10 ^ 70 + 9992680937142435765781366218922630690955520077741894351317769929803997) * 10 ^ 70 + 1690159937192549586444237592428039360600414417553110369042186070434024)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_304 : Polynomial.coeff recurrence4B3A3 304 = (27991659528431 * 10 ^ 70 + 2888596701217408354133141710232438641022667867666763285905441413656586) * 10 ^ 70 + 4513527522427673216788378706273016369345849204745451416026700147501060

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_305 : Polynomial.coeff recurrence4B3A3 305 = -((5448650536836 * 10 ^ 70 + 5972417674086851264059059431640001481936400607469313418183315756684390) * 10 ^ 70 + 8080739776317967253156821909674125634979532845884868504528015646102053)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_306 : Polynomial.coeff recurrence4B3A3 306 = (727971978323 * 10 ^ 70 + 6508392178501471832604505405032515649747854927909989323056868229341904) * 10 ^ 70 + 1420052777402634375950724648765213686586369607387258019826775821705251

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_307 : Polynomial.coeff recurrence4B3A3 307 = -((73066202703 * 10 ^ 70 + 2856636195979743732789888768640893069461042326915435148111306088134810) * 10 ^ 70 + 8536465098498926588670274543134803354826655738492801095572266172370193)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_308 : Polynomial.coeff recurrence4B3A3 308 = (5296178052 * 10 ^ 70 + 9208862000220236101772512738676544777532709762259015995377642046828864) * 10 ^ 70 + 1773118394559484636539528732473897541113505688387358090306667430526649

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_309 : Polynomial.coeff recurrence4B3A3 309 = -((209026623 * 10 ^ 70 + 9837187814469460978081572231658942296423526286412745437169449597844258) * 10 ^ 70 + 5652777586221937589372208864760764834447375594920394554024591131053420)