Recurrence 5 lookup certificate: Scalar0Exceptional 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.recurrence5Scalar0Exceptional_coeff_0 : Polynomial.coeff recurrence5Scalar0Exceptional 0 = 0

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_1 : Polynomial.coeff recurrence5Scalar0Exceptional 1 = 0

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_2 : Polynomial.coeff recurrence5Scalar0Exceptional 2 = -(538000971000222526023099986872709245460965839709009246890 * 10 ^ 70 + 5914668940727449095618428256487521505390691735831997868913614705139712)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_3 : Polynomial.coeff recurrence5Scalar0Exceptional 3 = 3617506695558775387638654376070688667426555733514652752458064 * 10 ^ 70 + 3516342332940159548117154844687965247214767964349635282427593398947840

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_4 : Polynomial.coeff recurrence5Scalar0Exceptional 4 = -(6699034275103313356815201423867427782629190598396949183901124269 * 10 ^ 70 + 1110624575690006187557888489738127669865544766170693701416965750877696)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_5 : Polynomial.coeff recurrence5Scalar0Exceptional 5 = -(3653220561713706855103240485869352463366773356620649940127230780325 * 10 ^ 70 + 4590478004418990190515830997895892017902258334763746262135060444474624)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_6 : Polynomial.coeff recurrence5Scalar0Exceptional 6 = (3 * 10 ^ 70 + 3768552033177016279832190430990478296088024345132460163586850203927423) * 10 ^ 70 + 884737422108211693482334990415333842620748732859908243228756685911264

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_7 : Polynomial.coeff recurrence5Scalar0Exceptional 7 = -((5864 * 10 ^ 70 + 7710879988983015271644594812299220267344301860405400300154119623673601) * 10 ^ 70 + 1227670080803979943531886184036855529530669879314202104993063723418976)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_8 : Polynomial.coeff recurrence5Scalar0Exceptional 8 = (5066226 * 10 ^ 70 + 7993987427972346832851552501891333049799747413473808455865029116187903) * 10 ^ 70 + 2346340290384469090773484789549019007274798506868140231788401244116176

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_9 : Polynomial.coeff recurrence5Scalar0Exceptional 9 = -((2200165667 * 10 ^ 70 + 3353861575373893620838243080896701055012391647871764129893071484755234) * 10 ^ 70 + 6417573856162263213679379744986105658291207771721047768368325431478128)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_10 : Polynomial.coeff recurrence5Scalar0Exceptional 10 = (276527202373 * 10 ^ 70 + 1562962866431948933644148051463618488167600959673613581653516203814650) * 10 ^ 70 + 6228271664169954634000726708472111591473626951746121225510443957801632

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_11 : Polynomial.coeff recurrence5Scalar0Exceptional 11 = (180684372346260 * 10 ^ 70 + 5406121072172603055148901972991276543500608960286617814622817568771923) * 10 ^ 70 + 6904455596995797811807451952194570256697673362838909861118100493360412

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_12 : Polynomial.coeff recurrence5Scalar0Exceptional 12 = -((179579990156086408 * 10 ^ 70 + 3998539696821475469186885522166655518281021635379471467400613352830030) * 10 ^ 70 + 1267155405289642675777852927315043773326854324490337096034108883684000)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_13 : Polynomial.coeff recurrence5Scalar0Exceptional 13 = (163289835815767154124 * 10 ^ 70 + 9452632346451610881302173413352782087928967813764353730889654092829658) * 10 ^ 70 + 7216576741913544341647487689721995398675370794255810367814657304618704

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_14 : Polynomial.coeff recurrence5Scalar0Exceptional 14 = -((115873763077851828110317 * 10 ^ 70 + 4965122081691287834015992627630497053202197073712485752726928603183958) * 10 ^ 70 + 2296204846614804174373995062953352279209407717210445155390056141193340)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_15 : Polynomial.coeff recurrence5Scalar0Exceptional 15 = (52489659643440519367059318 * 10 ^ 70 + 2133136509790277109600109440354657308673903933599310692431449096103260) * 10 ^ 70 + 6892466301626458082509814417051689156921919984081476104975936251125668

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_16 : Polynomial.coeff recurrence5Scalar0Exceptional 16 = -((13831323499198478770936354899 * 10 ^ 70 + 3312353411257484007593964321014883520336760336236413095154209775498405) * 10 ^ 70 + 8574140169845363902494573197175609942302095711058122049254268111232628)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_17 : Polynomial.coeff recurrence5Scalar0Exceptional 17 = (936850284944755624462024749833 * 10 ^ 70 + 9092071642342065373637953531246609479511522221176028488352056287717995) * 10 ^ 70 + 1177116416803022591680157054615569190668073847356200589047407820678716

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_18 : Polynomial.coeff recurrence5Scalar0Exceptional 18 = (1244485000916126334934579976428467 * 10 ^ 70 + 3135020951457323166301293054357906837971062244644325437710966738607249) * 10 ^ 70 + 5603993186678067138045795020330204076037594118135067049541303059605740

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_19 : Polynomial.coeff recurrence5Scalar0Exceptional 19 = -((1060205822275267879667310996093696166 * 10 ^ 70 + 3127322816703293884690011470246595902144452232068775897954525576142205) * 10 ^ 70 + 5225098674691851556038011381427228396359022235969930482035582639665524)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_20 : Polynomial.coeff recurrence5Scalar0Exceptional 20 = (619590058863651411553223231229187044665 * 10 ^ 70 + 1151509663967371639948452991309845809862836723026895069099620102200327) * 10 ^ 70 + 4302883703598019488572731799265053810166687013361267788585251881819160

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_21 : Polynomial.coeff recurrence5Scalar0Exceptional 21 = -((271199866147298166073225229775392534502050 * 10 ^ 70 + 7977589290892998179328257988532444803861434328636656953833996413557399) * 10 ^ 70 + 6497530098658128065958546186280929661832524625086842477986085873725841)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_22 : Polynomial.coeff recurrence5Scalar0Exceptional 22 = (81080387603024936528036946303101554666763192 * 10 ^ 70 + 4284913739250858390767852219782763667635311998075422088537957002838348) * 10 ^ 70 + 6233080168951918563793616683762059503655714766228095525720872722551112

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_23 : Polynomial.coeff recurrence5Scalar0Exceptional 23 = -((11341995685042719015187743107499671011865285115 * 10 ^ 70 + 2634786580072517599897140809030936711506472121321875109658267188657470) * 10 ^ 70 + 6904036258355055063212050450801942401988162356485962076891209317259858)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_24 : Polynomial.coeff recurrence5Scalar0Exceptional 24 = -((3282511049652482731533783287758974515956488573501 * 10 ^ 70 + 685691895641960761554391745497812446917487624765916534739418047853431) * 10 ^ 70 + 8132724890153811153225689832787160600885916018186410345950977574537385)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_25 : Polynomial.coeff recurrence5Scalar0Exceptional 25 = (2862072889068071674210045255727970842028186246089007 * 10 ^ 70 + 5916039940795999000561858422640961404659354530185412848931489759541152) * 10 ^ 70 + 7040024386434664980561118997405685132037513193865627487010284959691062

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_26 : Polynomial.coeff recurrence5Scalar0Exceptional 26 = -((1126985691976915644451624797610203436375417556913890998 * 10 ^ 70 + 7529612570741438986802925737922872951692179935836443987320753657182389) * 10 ^ 70 + 351661836812330999301508973858672522020387884260468952964502282792004)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_27 : Polynomial.coeff recurrence5Scalar0Exceptional 27 = (314965039712125468008125860861616961576275700367694368366 * 10 ^ 70 + 6317446253764715110763031523636336255568059379821285714500440222534359) * 10 ^ 70 + 2870928367006208703795552420409928752093936460260891719166040712029328

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_28 : Polynomial.coeff recurrence5Scalar0Exceptional 28 = -((68588353936599551484828428397700076609126591924479806798405 * 10 ^ 70 + 5217248654270375757241105094937511452382003317776832808226841507530262) * 10 ^ 70 + 7371738982929979599883837060201987308883315323036719495496930992522732)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_29 : Polynomial.coeff recurrence5Scalar0Exceptional 29 = (11976228480232776364729109890479819511667699067336493634410539 * 10 ^ 70 + 5808542448093581259323881620756834422394844013943466682880211647707252) * 10 ^ 70 + 6838076447007028254356641086306084127634266758941151331511364191868598

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_30 : Polynomial.coeff recurrence5Scalar0Exceptional 30 = -((1671361558171939307099440723507793180663073130787906686138702388 * 10 ^ 70 + 9569575459713648004798110248069536774916898255749327917645941613689743) * 10 ^ 70 + 9789424675654940433591431679393044340888270468683640805900150258816959)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_31 : Polynomial.coeff recurrence5Scalar0Exceptional 31 = (178114286427088143879641699037467422891108574577284140890885524149 * 10 ^ 70 + 9343219699947422507651112954689734231576295950486956075386947405476043) * 10 ^ 70 + 6377739912505370649057702379761368039662794204833113249159718921404057

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_32 : Polynomial.coeff recurrence5Scalar0Exceptional 32 = -((11973278142559817394182790326549452804691446540555453949357447024083 * 10 ^ 70 + 7823207266707598376862494246872879575042666343136373052354594815817841) * 10 ^ 70 + 9270593149718615419814288431617212459385531713831315991259085832078477)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_33 : Polynomial.coeff recurrence5Scalar0Exceptional 33 = -((173274601121097714831164684916590392318120028883450643943253257991107 * 10 ^ 70 + 4110634225802260491320597680549338121839133159561364360803586836293266) * 10 ^ 70 + 363766135921866633271430645694813921829604575260292991624471808977205)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_34 : Polynomial.coeff recurrence5Scalar0Exceptional 34 = ((20 * 10 ^ 70 + 1529416061383284918708521620177679071039556230146428418888695890940826) * 10 ^ 70 + 1662829930132661886007641857946937446305160046514432588123918774371547) * 10 ^ 70 + 8792959835603535930855595724651459696967971648696004778870356355328365

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_35 : Polynomial.coeff recurrence5Scalar0Exceptional 35 = -(((3670 * 10 ^ 70 + 9437605485986858546251097980499724901576136366932358565911279768674243) * 10 ^ 70 + 5274477491035284188448309896176986608673477352595893590499358587836393) * 10 ^ 70 + 659933528907273252045714204122111978870479402641885956497178401826005)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_36 : Polynomial.coeff recurrence5Scalar0Exceptional 36 = ((445583 * 10 ^ 70 + 1568310390155226840729455489322716337074391783851678904848346630416401) * 10 ^ 70 + 9797563830270806932899796287078175400361289806466578946443965519986096) * 10 ^ 70 + 676048376380360369082938748845222493881174464688213863046689187860098

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_37 : Polynomial.coeff recurrence5Scalar0Exceptional 37 = -(((40322609 * 10 ^ 70 + 4951314707360470244198424729006183312950836079853094151899551503694918) * 10 ^ 70 + 9579658605990197386203276436120672642836773214765996135325386602575807) * 10 ^ 70 + 400794012010589640170081855717625435661237557280187070927810531082964)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_38 : Polynomial.coeff recurrence5Scalar0Exceptional 38 = ((2586503180 * 10 ^ 70 + 8670001222149190371552547320290572968522796228003690432997186653263918) * 10 ^ 70 + 2095500004694679716655786206298237573548090888417512429042833519901191) * 10 ^ 70 + 7840820414386737651137326718293773759978028786227067291554682670515691

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_39 : Polynomial.coeff recurrence5Scalar0Exceptional 39 = -(((70001680479 * 10 ^ 70 + 5529428532250010739147462214612634252938111065589003434528040633306441) * 10 ^ 70 + 6081650524184888698002240234070184779442707263814673111090578959244140) * 10 ^ 70 + 8447670050743256329749394541025708602916058848118486326042934696821637)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_40 : Polynomial.coeff recurrence5Scalar0Exceptional 40 = -(((9749812583661 * 10 ^ 70 + 9053164348342049375383446007135097067948022548169428167497975461691886) * 10 ^ 70 + 5523560033244076906767234194285176771819941894580120472777922557686780) * 10 ^ 70 + 5165841980105888565503526634936609909152014105846746167895845250060848)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_41 : Polynomial.coeff recurrence5Scalar0Exceptional 41 = ((2013361118058735 * 10 ^ 70 + 9930458481532514618889720036267125068167042576212495316225013233089042) * 10 ^ 70 + 5761464103577329185657674402833491178094801573029072075966330456051237) * 10 ^ 70 + 5606676922711627881365829881750361914989344150926217791986477869945448

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_42 : Polynomial.coeff recurrence5Scalar0Exceptional 42 = -(((233004559971632552 * 10 ^ 70 + 5418692781372980581315989544215597994170500994657381663353105163882444) * 10 ^ 70 + 7678458985624289279117099078874868334172702742287044497834567336335199) * 10 ^ 70 + 7041826520229418252378593270964095163377861973320683232665968840958700)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_43 : Polynomial.coeff recurrence5Scalar0Exceptional 43 = ((21023322956308088453 * 10 ^ 70 + 7530319071968596149898923455050271140256881127607746079891975456020499) * 10 ^ 70 + 5856819365294926299780874157595544212564665443378377030709465507132842) * 10 ^ 70 + 9192460830028936231861010214290487632815739812135143604140353827749122

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_44 : Polynomial.coeff recurrence5Scalar0Exceptional 44 = -(((1605514884205629072821 * 10 ^ 70 + 7075067318477241828357096956599544745291772231557413587300943709480354) * 10 ^ 70 + 3229347642341054893885097570122656470346028949626145166710966589784747) * 10 ^ 70 + 1731211228145771420145490119168269107015289331944038136546115629013428)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_45 : Polynomial.coeff recurrence5Scalar0Exceptional 45 = ((107406300075911229481305 * 10 ^ 70 + 3488997512318510256300625671934628044098515696500940981631095200479205) * 10 ^ 70 + 6500728821384189607624801781146326232772269543335444908480988681753694) * 10 ^ 70 + 6710164853413985823468204438817086357815584274757876969715536839516567

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_46 : Polynomial.coeff recurrence5Scalar0Exceptional 46 = -(((6409064810098680407619719 * 10 ^ 70 + 5908972503182696250884693509655512032646993952742875545032840954609224) * 10 ^ 70 + 4333262846698301563518671517084907966060116253270798323535058979082483) * 10 ^ 70 + 7373628999738762827859274594732388440801754725359658360152270538214065)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_47 : Polynomial.coeff recurrence5Scalar0Exceptional 47 = ((344818650390064565908828301 * 10 ^ 70 + 9062662522283365931136118931548555627721208947581660265799350397360883) * 10 ^ 70 + 1743939503761998007522878887750812450035697212488173511217058665756920) * 10 ^ 70 + 9352432318306665301155855726705382161450258438096668881147610736695388

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_48 : Polynomial.coeff recurrence5Scalar0Exceptional 48 = -(((16842662095524403584910823439 * 10 ^ 70 + 1168175528336898332868858200577881314705259702287837213667821501506706) * 10 ^ 70 + 2056857947649016020745526513243203492880748887265616392352553684893936) * 10 ^ 70 + 4919518374400151455767063551417338856923490872728223496949663291973389)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_49 : Polynomial.coeff recurrence5Scalar0Exceptional 49 = ((750255279966315855130034924904 * 10 ^ 70 + 8366066028093816926152887350773870683289915006154457978708369093178677) * 10 ^ 70 + 3094097283722634977745712311245448021327191801544491083281169207067912) * 10 ^ 70 + 7697769165904901055374686112881588077548145775611868097461366699248008

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_50 : Polynomial.coeff recurrence5Scalar0Exceptional 50 = -(((30563913003230962885513164616270 * 10 ^ 70 + 1327588849004040806665848723468977485863223300129093724421756377821618) * 10 ^ 70 + 5049940932844524355276806049035277764060934452031716683549538320483955) * 10 ^ 70 + 9327246868699546523618887855668521760564800279787830057107018480334057)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_51 : Polynomial.coeff recurrence5Scalar0Exceptional 51 = ((1140346612421750933729817280606938 * 10 ^ 70 + 4812966334751104240673996425896328876777097624944902267383465138792906) * 10 ^ 70 + 2260125157796421527337242282566568027261250611951720662923627296196348) * 10 ^ 70 + 8765689235328912512608652977997695527413984414871813047719853935487270

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_52 : Polynomial.coeff recurrence5Scalar0Exceptional 52 = -(((38971373896345884122287432115019008 * 10 ^ 70 + 8070516981705009289862786667328951004352868343609376919422634006284107) * 10 ^ 70 + 4901420578290565711889378299703142331324232388473779069353194804040809) * 10 ^ 70 + 1557216257531427695647721989421190274948687449308815816547269014547603)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_53 : Polynomial.coeff recurrence5Scalar0Exceptional 53 = ((1218247219893383399182317526449509671 * 10 ^ 70 + 772307663412478244001113859214312610243242401907492537906418500582844) * 10 ^ 70 + 4168746454336101965727865558433025576467044087908297635021196273331140) * 10 ^ 70 + 5732138486965859757798305727839074410951690549272407160602635066330355

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_54 : Polynomial.coeff recurrence5Scalar0Exceptional 54 = -(((34716333155889776196639590913075236917 * 10 ^ 70 + 4186448855641548323971818420059973986209463857976758564755476393041084) * 10 ^ 70 + 7864953154377871901138326973569200561576768798961834720400347057628640) * 10 ^ 70 + 5934389946852785267597019437342791483244679661604140104091354058221983)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_55 : Polynomial.coeff recurrence5Scalar0Exceptional 55 = ((896028240591634567187914489465761641546 * 10 ^ 70 + 1400425723973908706286382562594517834846707742157171675042602456880100) * 10 ^ 70 + 6918456028003943417173304566863854569453450241498774018153226951120720) * 10 ^ 70 + 2878249923387998892027689123768360076967346432351512290430108922509586

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_56 : Polynomial.coeff recurrence5Scalar0Exceptional 56 = -(((20695845420363236165753566417660407723297 * 10 ^ 70 + 1316441307794716589061687725482824522035385331720559838064069451966674) * 10 ^ 70 + 7951606744728594752195559320927199018778796292778331311238896984817585) * 10 ^ 70 + 3916986802836374005727997286169513742129312797355529181423666031756088)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_57 : Polynomial.coeff recurrence5Scalar0Exceptional 57 = ((417824740165427309152138832248803939020823 * 10 ^ 70 + 532459202325053129746329967778898954760958876910975355710916968455961) * 10 ^ 70 + 6372999761338292395755422990478821455966351129632737906327999686197447) * 10 ^ 70 + 5139973658065730981492035164120539990182732229169749419966799899856979

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_58 : Polynomial.coeff recurrence5Scalar0Exceptional 58 = -(((6987655759957842243180554534748124837208396 * 10 ^ 70 + 3954215576825023668033493873498284263209385751062856087742393204104095) * 10 ^ 70 + 6588417471175409891849087421854147769724045409184695479307338714502) * 10 ^ 70 + 392500816601493408292241130077565208243510710567193854401562545068189)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_59 : Polynomial.coeff recurrence5Scalar0Exceptional 59 = ((81518411565188954823433605296168575935611040 * 10 ^ 70 + 1093114814095042906880680204478578669205263471694015837057359429870344) * 10 ^ 70 + 421493316141488325658703783558114658631969226272494357973718378274265) * 10 ^ 70 + 4160050584269723657101248306670621236668788286607397038314253624476100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_60 : Polynomial.coeff recurrence5Scalar0Exceptional 60 = ((8103382484867436662262510996383236650417205 * 10 ^ 70 + 9734343203977549140809546925998774546592692000870896777771265323895208) * 10 ^ 70 + 9045187518253650238570543949890663130095271191083639039434002470967684) * 10 ^ 70 + 7701469475244426657499392629596619747356732436424497395999088313340278

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_61 : Polynomial.coeff recurrence5Scalar0Exceptional 61 = -(((36090541611761511710502715476300188148826975861 * 10 ^ 70 + 9539542209695898513885428375520272723947595314795759066955760463075420) * 10 ^ 70 + 4124009167991090887925643244684859441597238498050298410940431215294006) * 10 ^ 70 + 6513284540566325897849422333458506735072205002623879206554444312319155)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_62 : Polynomial.coeff recurrence5Scalar0Exceptional 62 = ((1341482452000576320551586085346376259128245782634 * 10 ^ 70 + 4649426934443742539998450142741942247392393713002748889071770414778688) * 10 ^ 70 + 5296056330753754099899611251664655474243749200965903938358920460006466) * 10 ^ 70 + 2983808033954638981672118034370852438115170339075307170868305356250315

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_63 : Polynomial.coeff recurrence5Scalar0Exceptional 63 = -(((34335581959609386353570146807837356698633415158004 * 10 ^ 70 + 5207066998560978725489589469811449588899792213477744794003030173296508) * 10 ^ 70 + 7031401936644318072261790072783576517285969761604069993216246247697520) * 10 ^ 70 + 1077616122966407534404682051816381911745891055605155154731252205777813)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_64 : Polynomial.coeff recurrence5Scalar0Exceptional 64 = ((707530649574841726355371679971567854427796678178996 * 10 ^ 70 + 4081302444159043141787599194366442551551644528963333518348751379599866) * 10 ^ 70 + 4790679003680610036962776698854645083782174174907905944673465903781766) * 10 ^ 70 + 3306286236117332270287544989585259187820740148382312655466665130529656

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_65 : Polynomial.coeff recurrence5Scalar0Exceptional 65 = -(((12088055171850373819384709826156677208617986176073213 * 10 ^ 70 + 1590118405415567584480818614691448345357752087886712129062376796125072) * 10 ^ 70 + 5723458346556968843136703028276059232414830559978472940534605840603893) * 10 ^ 70 + 4182023806207137532285639283689526303490145817886733533943919173447406)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_66 : Polynomial.coeff recurrence5Scalar0Exceptional 66 = ((166297967652198994901526539148821573594218348012148747 * 10 ^ 70 + 8715177920934788783162150998501653440668192585831805580237838932952012) * 10 ^ 70 + 186750373318022061586149564219124298873414201000560868597626254975954) * 10 ^ 70 + 3555229542902547315848176629134396689778360507740013024591876737776024

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_67 : Polynomial.coeff recurrence5Scalar0Exceptional 67 = -(((1579342057799743233057402064548043170099269868157381560 * 10 ^ 70 + 9977459390863069746688160942524346468876817630656157369820651507900067) * 10 ^ 70 + 4130357585881138903405757547322766751260720025535311824029270178504232) * 10 ^ 70 + 6231895986945837928626139475529432556572888794741330928022162231957644)