Recurrence 5 lookup certificate: B2A3 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.recurrence5B2A3_coeff_0 : Polynomial.coeff recurrence5B2A3 0 = 48 * 10 ^ 70 + 5488553144903175665120206907073313912963917670213803256214235831195648

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_1 : Polynomial.coeff recurrence5B2A3 1 = -(71860 * 10 ^ 70 + 8748545756422161630689437710719134893650026902786383886928396775923328)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_2 : Polynomial.coeff recurrence5B2A3 2 = 475601633 * 10 ^ 70 + 3464333537908235487004177863233805069182808753985003838970975213097312

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_3 : Polynomial.coeff recurrence5B2A3 3 = -(1726962002788 * 10 ^ 70 + 1292005783711536055456037897297303770959527799884135381984868578485976)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_4 : Polynomial.coeff recurrence5B2A3 4 = 3226649198797744 * 10 ^ 70 + 9836947142640043571596963739722694942547379738929405533485777398986784

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_5 : Polynomial.coeff recurrence5B2A3 5 = -(3433950756504242786 * 10 ^ 70 + 9376543253039455722708020998316686154759799587995090404015814059529288)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_6 : Polynomial.coeff recurrence5B2A3 6 = 2316982640853859198376 * 10 ^ 70 + 6656675301293842105653448829989713659688758452855734431287952069070576

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_7 : Polynomial.coeff recurrence5B2A3 7 = -(846522830234174383129751 * 10 ^ 70 + 94039609403273889180900424854522460193515952341276519887551685571304)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_8 : Polynomial.coeff recurrence5B2A3 8 = 1814661901860155652825507 * 10 ^ 70 + 3466322806800694012098968174000537739943418100225574623866423504917484

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_9 : Polynomial.coeff recurrence5B2A3 9 = 191262421756386795043687807210 * 10 ^ 70 + 6796811068091512270947097596984183818736119911780521578635581540912396

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_10 : Polynomial.coeff recurrence5B2A3 10 = -(143508277394368334398215557935094 * 10 ^ 70 + 1025754956157065888830120597734869484363685418683659569053675401311704)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_11 : Polynomial.coeff recurrence5B2A3 11 = 80685881368527806198379666664098436 * 10 ^ 70 + 4035342240146572400039066192550872076874122392851860523204138304134368

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_12 : Polynomial.coeff recurrence5B2A3 12 = -(39451015449839027205434463431274840070 * 10 ^ 70 + 9716122410057859279776305579854381767096470892876480623890894011579938)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_13 : Polynomial.coeff recurrence5B2A3 13 = 14928661738902549544953094388387568468356 * 10 ^ 70 + 6883653049926644637895520442782877172236196493175077762171229582860746

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_14 : Polynomial.coeff recurrence5B2A3 14 = -(3309403744765495708861557942693146273670796 * 10 ^ 70 + 6159674101069059350255221427915467761206445076674940799391699649547868)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_15 : Polynomial.coeff recurrence5B2A3 15 = -(266695074734179130285414578358011786241585914 * 10 ^ 70 + 3016397300599063812413042928649543960497272379335839931554174882005458)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_16 : Polynomial.coeff recurrence5B2A3 16 = 614321358346969485824895242220557397272142477977 * 10 ^ 70 + 8005604558773250322518125040849402463385742447285856402823528131632022

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_17 : Polynomial.coeff recurrence5B2A3 17 = -(314195368404515848429471610891023753735826610461419 * 10 ^ 70 + 9545312049223349189380267403576368536128157336408271952541323952780613)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_18 : Polynomial.coeff recurrence5B2A3 18 = 106506029613026494257547251918647662232821638580092036 * 10 ^ 70 + 6249968828713541226410404890527487393867124939936817945309672634442711

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_19 : Polynomial.coeff recurrence5B2A3 19 = -(27576801060988620893449676378842836398442859240049319111 * 10 ^ 70 + 9537037430399395302203761281193735904134672219966051812408990373029620)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_20 : Polynomial.coeff recurrence5B2A3 20 = 5733673844866061884909006543586937915191309921274851564495 * 10 ^ 70 + 4782054071966450144608348651265565145354699350858644712598536501537893

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_21 : Polynomial.coeff recurrence5B2A3 21 = -(977846365858285975221416536576756484776026272810307715609494 * 10 ^ 70 + 8660276690617959881947629708490276277159967019919713912792564598833164)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_22 : Polynomial.coeff recurrence5B2A3 22 = 137494637628474005371814005519534384935147387296005538996058131 * 10 ^ 70 + 7052803242039680305481700322557314369312626428283188402750142596183152

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_23 : Polynomial.coeff recurrence5B2A3 23 = -(15747755687208637018898151969676198149313028231363457459772032261 * 10 ^ 70 + 5487312527009765632789786906563643387408520972128431728434194258202157)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_24 : Polynomial.coeff recurrence5B2A3 24 = 1401178869028824310350100435205873648993531564273839038022093943923 * 10 ^ 70 + 3541897079684633738253899887100236752343235751112489595315618572144411

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_25 : Polynomial.coeff recurrence5B2A3 25 = -(80729945864207073787862589620022060395237496757766482683100071898472 * 10 ^ 70 + 4649883337031204430003582772259833642453701715590087657623122081172992)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_26 : Polynomial.coeff recurrence5B2A3 26 = -(685458418254170251958521924275991205798431261390594952311324579081041 * 10 ^ 70 + 1691281887654079901195401585657374861373126982618037563739558595611640)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_27 : Polynomial.coeff recurrence5B2A3 27 = (95 * 10 ^ 70 + 8488228708065530801037730098272777929732297956450098628946213172755678) * 10 ^ 70 + 6137250320034446471363334633000678755560390888189021223461995665786840

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_28 : Polynomial.coeff recurrence5B2A3 28 = -((15990 * 10 ^ 70 + 6825088928112687924426873402986047602908679404585280166732921870978978) * 10 ^ 70 + 2471067628452081328691830070051009703148434022590746299712608290818484)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_29 : Polynomial.coeff recurrence5B2A3 29 = (1852412 * 10 ^ 70 + 2861996398566083586988660263927469798467847644888293196268483499119348) * 10 ^ 70 + 1032265307118300882353272527781912502564709714134529180428925798997121

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_30 : Polynomial.coeff recurrence5B2A3 30 = -((174239510 * 10 ^ 70 + 6082551417134484622361297411955512406130827696915755165605975060380952) * 10 ^ 70 + 5672346138066992343828162825800217494855269315020561919096771992576336)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_31 : Polynomial.coeff recurrence5B2A3 31 = (14031464953 * 10 ^ 70 + 1371245153516668858050581109262726413370630177747171405326594451952540) * 10 ^ 70 + 3179714221935118406948300425105974761774480957645390600933449413556265

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_32 : Polynomial.coeff recurrence5B2A3 32 = -((992335319001 * 10 ^ 70 + 8034000792929107285560952625546017467406435450018877249397301258712263) * 10 ^ 70 + 2732032477133213195827142044127925392938597514376098677518357764790835)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_33 : Polynomial.coeff recurrence5B2A3 33 = (62549458729087 * 10 ^ 70 + 1341834616221783659696873183821881871002631283248008551874216703446149) * 10 ^ 70 + 6078265450893506898386312138058882500762472207318270839288670659636752

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_34 : Polynomial.coeff recurrence5B2A3 34 = -((3548035645242998 * 10 ^ 70 + 918756622190932849900342816491146675011589890318335143740921567656608) * 10 ^ 70 + 2008323112620156526600141886854791940256828111055310088504440802322774)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_35 : Polynomial.coeff recurrence5B2A3 35 = (182354433301505809 * 10 ^ 70 + 8361264038364665053283495101902422265222331281768094944841524017260876) * 10 ^ 70 + 7860932136983837819591171270710689912661797047802208232211379750866404

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_36 : Polynomial.coeff recurrence5B2A3 36 = -((8535306833022723299 * 10 ^ 70 + 2071568849653384531445940704057075889375642826967242745267730508134387) * 10 ^ 70 + 8715323126132868459715488936067555393515162340271124715720633152097752)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_37 : Polynomial.coeff recurrence5B2A3 37 = (365255099519345970312 * 10 ^ 70 + 7358596547880051862428906072201735347219998874546416393621948287548680) * 10 ^ 70 + 9318568870140124317498248759887091251163121033935787891470575782795204

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_38 : Polynomial.coeff recurrence5B2A3 38 = -((14334032742164091542144 * 10 ^ 70 + 4120349591932577704460624462199253620040739167549806102302161563242622) * 10 ^ 70 + 6975887052580517908442921147661138450482263156261695151825822206413498)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_39 : Polynomial.coeff recurrence5B2A3 39 = (517065464045379550986105 * 10 ^ 70 + 6684587621405328717152069896036235592423471429319941281872281283161428) * 10 ^ 70 + 5069132238244959650613293690277366727789207838312949259949623628592552

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_40 : Polynomial.coeff recurrence5B2A3 40 = -((17173341875379752338804592 * 10 ^ 70 + 3698070101467443981991421970372005984626735159405502606600253275098393) * 10 ^ 70 + 1454039409014537010463771320244836488039302322442573210096628938009274)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_41 : Polynomial.coeff recurrence5B2A3 41 = (525695150154541178255630283 * 10 ^ 70 + 149316001594625651076226193978683228352908107846271146200375403566744) * 10 ^ 70 + 1335343364649975590903557807723120677133160518549046327739570838936971

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_42 : Polynomial.coeff recurrence5B2A3 42 = -((14835008875467158119154052960 * 10 ^ 70 + 6269401344698947142370537162325283395605522054117850659654959199634540) * 10 ^ 70 + 7948588724912483994591438538993048391272673175301003230139551409601109)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_43 : Polynomial.coeff recurrence5B2A3 43 = (385649129273905323389381450642 * 10 ^ 70 + 4473483388104538775292049997248487501656860719491117442468406486743947) * 10 ^ 70 + 5078607917633829227617529128841548871455053053784317098410617695418697

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_44 : Polynomial.coeff recurrence5B2A3 44 = -((9215309380317180359133175785134 * 10 ^ 70 + 6074491273945046458528082566385906208131835283767867028468342766023483) * 10 ^ 70 + 2189987588228722994109628860189127712660304019496891398520392203047379)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_45 : Polynomial.coeff recurrence5B2A3 45 = (201525843956888587323508889382934 * 10 ^ 70 + 5474630331849431171751170260993451682017819490527492664233072453887897) * 10 ^ 70 + 6650090690301966940478011625634393132055881218421783015330315642498923

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_46 : Polynomial.coeff recurrence5B2A3 46 = -((3999740709430731059029178198875610 * 10 ^ 70 + 4687083221896339147690070660719371567390938053630678880590326470012882) * 10 ^ 70 + 6970225624712572489024964612312155634204490399722764316296261667179150)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_47 : Polynomial.coeff recurrence5B2A3 47 = (70885694384935330865497597691632143 * 10 ^ 70 + 2572129957067957361302052552132758270643187701393043414238804818838895) * 10 ^ 70 + 2502732739432198044862604498142151297041743628370798730610459891516291

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_48 : Polynomial.coeff recurrence5B2A3 48 = -((1083057228487426266443873357908744511 * 10 ^ 70 + 718229689710025696909028301209172306237384715658597587739790636674132) * 10 ^ 70 + 5679620637431603655388521990725582753618477268230525519261462839994232)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_49 : Polynomial.coeff recurrence5B2A3 49 = (12964182321997468363937438153776636331 * 10 ^ 70 + 7739128326263658601830694239071580926316688470265687877458239712675095) * 10 ^ 70 + 507034097716412651021015015102007123413511746388080994091774026209530

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_50 : Polynomial.coeff recurrence5B2A3 50 = -((74571863411455054022223223782457420399 * 10 ^ 70 + 1572634333139691897231476638866805312254533050745637054348835568870610) * 10 ^ 70 + 133859325995471086903139631392436530917873422713666536851786990599427)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_51 : Polynomial.coeff recurrence5B2A3 51 = -((1826279520946449755173278280292918037013 * 10 ^ 70 + 4411419700413374271156048249476942165040889130820821193235661746313950) * 10 ^ 70 + 9474771503535711425443127307831783767995182312526957074643519778896253)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_52 : Polynomial.coeff recurrence5B2A3 52 = (86418051567073191523246692440193689781506 * 10 ^ 70 + 1578440760912598640819801289858167816029779632145206363468191828195034) * 10 ^ 70 + 6547400551780831899670822190088427643140458553114840533165951086030849

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_53 : Polynomial.coeff recurrence5B2A3 53 = -((2312166781136500856358267741739788030149586 * 10 ^ 70 + 7779486647642006996555093639603342568471722961487010583173931608991073) * 10 ^ 70 + 9943392267667976899499772312596449179116698716646849931753528099961664)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_54 : Polynomial.coeff recurrence5B2A3 54 = (49872035807140515177544230343538163717710793 * 10 ^ 70 + 8421683544147173807643607111732609730047903306423411189486482123951776) * 10 ^ 70 + 4282733730730463739923806252551195782471463358156710799960123116232385

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_55 : Polynomial.coeff recurrence5B2A3 55 = -((942435953353534231086156762173287137607151128 * 10 ^ 70 + 4868248946724115503912894862025446614676845528610074159959416999983035) * 10 ^ 70 + 3290268126503778303481393203067129038612638684002158728862214788521380)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_56 : Polynomial.coeff recurrence5B2A3 56 = (16135651167445760787874831692758562324092926064 * 10 ^ 70 + 6411229352820321030411883293293137050405452100600401807261433771046154) * 10 ^ 70 + 6077280770288101990490757551568023349970197802399078124541066874732487

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_57 : Polynomial.coeff recurrence5B2A3 57 = -((254655380693056466298575389299573363085455791765 * 10 ^ 70 + 6361140825818979334081435409191081751507521015059499595994906992476558) * 10 ^ 70 + 1776418334357286977717575456342794170066240023556798388559923534588347)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_58 : Polynomial.coeff recurrence5B2A3 58 = (3742859011871154074604584766049186399285060705806 * 10 ^ 70 + 8595569232338882052251963125704264794897035198079463137860059382638700) * 10 ^ 70 + 7405685174267022020549552923907709955766393004907603809301090640587350

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_59 : Polynomial.coeff recurrence5B2A3 59 = -((51577909419328353931637335291841978755308123861753 * 10 ^ 70 + 8560480892925055943327869042831289328425418057437755329179739332156279) * 10 ^ 70 + 3026666901422395693332784849517596979761457155707853350233005931814902)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_60 : Polynomial.coeff recurrence5B2A3 60 = (669581922927763510539511648393454717366854141792100 * 10 ^ 70 + 6613890652061859599651440488446021297363200398949160687236489830425848) * 10 ^ 70 + 9229790378204767218950835868460360183808996175893309840146084732535578

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_61 : Polynomial.coeff recurrence5B2A3 61 = -((8218158921459420475367716338225249460983131096824068 * 10 ^ 70 + 3576643203806436971539790558677782799339301980013598243007352535729119) * 10 ^ 70 + 7848226924121081740367649062992989268471819062835206385358528981504802)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_62 : Polynomial.coeff recurrence5B2A3 62 = (95629589049018379852875611769524403946154274417105407 * 10 ^ 70 + 6389098692724101306007976632597971937585853463418929243917423695146460) * 10 ^ 70 + 284156988018670019718181681419881217526652791326172546526296429092050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_63 : Polynomial.coeff recurrence5B2A3 63 = -((1057415677724149559990071593310204482985466041363540000 * 10 ^ 70 + 3813898039713585130224462939021765073966091072710528211695854637379585) * 10 ^ 70 + 2057338180623653147955373006183954519373150474926784057754908159722503)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_64 : Polynomial.coeff recurrence5B2A3 64 = (11131734337061046244281591750857855137858474774782706155 * 10 ^ 70 + 9697793843522348909802288095765188325104281785466840465852660209523126) * 10 ^ 70 + 3176955364013101293712830231273900411679951246013163720366414240099824

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_65 : Polynomial.coeff recurrence5B2A3 65 = -((111751565360563411407318149986742080020952401624125830436 * 10 ^ 70 + 6380688002683559201141080373077972316571917141387880463171426761350791) * 10 ^ 70 + 6018801865618316169963265855028523372089080124996070806322307167887976)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_66 : Polynomial.coeff recurrence5B2A3 66 = (1071369020372226127107266097435160385187556350330011149112 * 10 ^ 70 + 7648565067747328953725959135564162481608917483057254949073694698299270) * 10 ^ 70 + 2852465176834899376099101167180102380211895700218596042852727588772103

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_67 : Polynomial.coeff recurrence5B2A3 67 = -((9821347808115563604478379294804228360554006520019848703959 * 10 ^ 70 + 9066552680274278321409025285189137696812222946137600482582319027850464) * 10 ^ 70 + 8033829487626532016389579342823453770202652693205570143812173446796321)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_68 : Polynomial.coeff recurrence5B2A3 68 = (86187942791056712528943664285048413792797863315912710673708 * 10 ^ 70 + 5428946713201534033508221621917554126998021371381152890119423264655152) * 10 ^ 70 + 3048495261081767307130521514253367641482647873070360148543455870713303

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_69 : Polynomial.coeff recurrence5B2A3 69 = -((724798989003673749815631843132870524112656855758406275650795 * 10 ^ 70 + 3809410770509986871118552488100890512532370997159058612753792636516) * 10 ^ 70 + 2972641387363191958028552870159786853226811560839164756097744868499262)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_70 : Polynomial.coeff recurrence5B2A3 70 = (5846548106794065843859610878115204129103614721729198227863848 * 10 ^ 70 + 9196463342247210029244737040210005954739129324972809936273164802474726) * 10 ^ 70 + 7357941188257369952113622150129761580696343655394950159521745830228341

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_71 : Polynomial.coeff recurrence5B2A3 71 = -((45276874517566439959353772420185342179460340419085055500131648 * 10 ^ 70 + 8936880353301685318808570710962552060851501598651454218844193877290202) * 10 ^ 70 + 3171288545247902542508102456778745788464218299662088539819561663218876)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_72 : Polynomial.coeff recurrence5B2A3 72 = (336903646885820320164661171112401015056728574502945368936666788 * 10 ^ 70 + 9881539970493366196374452980033323852665771203249574090456698990542814) * 10 ^ 70 + 3792953983950514804797215617977138082373352854328039417912056833970681

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_73 : Polynomial.coeff recurrence5B2A3 73 = -((2410580101900732468459372028230355345011916719177100966566554644 * 10 ^ 70 + 1943824822035791102735412525035222268515748367816959837930432250761343) * 10 ^ 70 + 4922148949013835977297474632536285369727002157117423649415089979411276)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_74 : Polynomial.coeff recurrence5B2A3 74 = (16597315064353635090714153365577401957607502167817364370396479865 * 10 ^ 70 + 8171145065651527744029872492217927316879021923558001131315185912016309) * 10 ^ 70 + 7250910307485037632131729420121214145759025170637290710853172348933478

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_75 : Polynomial.coeff recurrence5B2A3 75 = -((110039905017029298760169837877016084954566607247911876523631498787 * 10 ^ 70 + 9417518995913380914891061885278986793300525512166024964914032781329958) * 10 ^ 70 + 6456408848478379587280987005219004871491329211426091172887808651917760)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_76 : Polynomial.coeff recurrence5B2A3 76 = (702972000350013245955322613656681420735011716450894800331637068530 * 10 ^ 70 + 9932459131440250609378848032172728009529158280781031318529397197678776) * 10 ^ 70 + 6458615145672827241722160659682479245236959827493521224031724704885098

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_77 : Polynomial.coeff recurrence5B2A3 77 = -((4329779958212120427889606388769590092936593210974822576118738434559 * 10 ^ 70 + 9787853504913941047312639499886234495949304497384704722572927371021082) * 10 ^ 70 + 4023814944821354307048650852022256576623537249432971103321108063154259)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_78 : Polynomial.coeff recurrence5B2A3 78 = (25726727755711259928615227948949933269408442596649380201635480580418 * 10 ^ 70 + 3653182869829306341642238145845677137182405389995478589999462396073073) * 10 ^ 70 + 5455477974337891154805287620159983047761725058737732054422594757248919

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_79 : Polynomial.coeff recurrence5B2A3 79 = -((147547760890893234742435146994880816785167307189907949526463673641212 * 10 ^ 70 + 8061761067467296030504665484533220323287969878374286371995019838914557) * 10 ^ 70 + 2080461817471445660501560081726485878649441986355318724352096276902349)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_80 : Polynomial.coeff recurrence5B2A3 80 = (817215944845918193657488262389390617869336757206739980985387424743273 * 10 ^ 70 + 7546364863870498169625126528642392797366970325825961500870668556200647) * 10 ^ 70 + 5346101428303010693758358319081541116930518183465594404120427817939135

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_81 : Polynomial.coeff recurrence5B2A3 81 = -((4373338563714742736814613338819085156716484555195427998190817761868559 * 10 ^ 70 + 8104815553645428688311378913125416519839956992315012306353862573254423) * 10 ^ 70 + 4296558449170826347164408997946986199597732291633439264752195475682984)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_82 : Polynomial.coeff recurrence5B2A3 82 = ((2 * 10 ^ 70 + 2623883406746940439340840572603864290402844542982386231531447294142522) * 10 ^ 70 + 3092983837364800427354164866343468825792978895589724606573174856514150) * 10 ^ 70 + 5220550882845309025087734555257808950824646320059541234767589872823220

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_83 : Polynomial.coeff recurrence5B2A3 83 = -(((11 * 10 ^ 70 + 3186624618196334420906577025225258832269357545844569867965444142588878) * 10 ^ 70 + 7545366920438403989972896497892276989025539564554349368361095821258775) * 10 ^ 70 + 5942868168755347703207396778912200031554944390606235431151957854175558)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_84 : Polynomial.coeff recurrence5B2A3 84 = ((54 * 10 ^ 70 + 7878156494365697027448067278377545768932741217649356114883794378412025) * 10 ^ 70 + 3084057951068641410520469700013033624286311982876949446800855259241597) * 10 ^ 70 + 3998103025216453126052855011366259168168999081961075133816830154644924