Recurrence 4 lookup certificate: Scalar1Left 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.recurrence4Scalar1Left_coeff_246 :
Polynomial.coeff recurrence4Scalar1Left 246 = (((9719087326442950558228533302 * 10 ^ 70 + 6589787323404326136174104684876222348361504102973813862242731138698878) * 10 ^ 70 + 6406744565314147301648071654116580419039059883077068286747754522934568) * 10 ^ 70 + 73440188579454672369972597801907755895750374249058299762624644626311) * 10 ^ 70 + 6124070852169662929664389758038934925096829825471931339347963183492091
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_247 :
Polynomial.coeff recurrence4Scalar1Left 247 = -((((9634996602866077532714534660 * 10 ^ 70 + 5267139533126966537071205425565210125338713335201857264473390840153406) * 10 ^ 70 + 3947258355707970722553833745279543310379194606758828844910486504204509) * 10 ^ 70 + 2537591840077230145926626938760525444848151553999748978980194490049687) * 10 ^ 70 + 5921259785127590234363481617480024540768725994661013837337872654698236)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_248 :
Polynomial.coeff recurrence4Scalar1Left 248 = (((9307808523144226131515577154 * 10 ^ 70 + 5649505778907938966863767559715810252804382302350006580557633994119747) * 10 ^ 70 + 4788417554644314355913921366891431295022429697580589478765437872318802) * 10 ^ 70 + 6077450539152915596181664486747945860961781795746988423378863475037541) * 10 ^ 70 + 6175256397872287130290747603121194918542443809453781657921229577690897
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_249 :
Polynomial.coeff recurrence4Scalar1Left 249 = -((((8736328953892618777356563721 * 10 ^ 70 + 6238067337036506735869655601997002704221793711856729689923390040753833) * 10 ^ 70 + 9869915958972138952715096722383629872556099846010259513268001999333415) * 10 ^ 70 + 2014462718243004656945838747135230658830569191223119901922548682371696) * 10 ^ 70 + 4442055081350312107873035716044065547610304266431845215928467591671815)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_250 :
Polynomial.coeff recurrence4Scalar1Left 250 = (((7933618040210027699333668721 * 10 ^ 70 + 8075522651564127238691989941150947544634790731622267609810271649476933) * 10 ^ 70 + 5888271902283696182590603865398115427554757641460525321802733955320291) * 10 ^ 70 + 3783532743854801477892580926417117377193617649333217592558715127834294) * 10 ^ 70 + 8685082008183215517963885405733570262822629643840292816511611556139083
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_251 :
Polynomial.coeff recurrence4Scalar1Left 251 = -((((6927006485844067499077555738 * 10 ^ 70 + 3670945552187489121940778102263477564976756254139092009141412864456664) * 10 ^ 70 + 420404113153994001056989456326612771546264012553258124969360402897009) * 10 ^ 70 + 9494038003476360264967765597739000960269252044042225576620842032155457) * 10 ^ 70 + 6871271939208836707408937439899117360304388515146549402097480131965411)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_252 :
Polynomial.coeff recurrence4Scalar1Left 252 = (((5756856498159478080310862742 * 10 ^ 70 + 7543541759099436637558456954522754928570442619928716839395544838265599) * 10 ^ 70 + 1831498224524220623973394741889907765667399326156810641418164004610012) * 10 ^ 70 + 7118430165560821796071418712602298929336812187700675270908479478373810) * 10 ^ 70 + 5532200792004812209801897812391702411345497723221724927848214880682640
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_253 :
Polynomial.coeff recurrence4Scalar1Left 253 = -((((4474112496266397701996713678 * 10 ^ 70 + 7791851918717842417967037380516367078945702608541309905981271114664692) * 10 ^ 70 + 4188337643880820721714110707532663775704785332377292097845113883204251) * 10 ^ 70 + 7629322432835036552469547508267233329990333515422570781035389170927942) * 10 ^ 70 + 9318841293043741356878377871701766869706583508875269631891364243233960)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_254 :
Polynomial.coeff recurrence4Scalar1Left 254 = (((3136829348427769520657254701 * 10 ^ 70 + 7460575219655912961616723825361012260932794612945604315403069803552592) * 10 ^ 70 + 4000971698506462063741499823976873838835871876767857073925502622052110) * 10 ^ 70 + 1704720678103511573318156467561193201297766971715726276103419373178223) * 10 ^ 70 + 2384326379296277133908233965086663967125385218475821362851819600920291
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_255 :
Polynomial.coeff recurrence4Scalar1Left 255 = -((((1805992531907459880646408051 * 10 ^ 70 + 1378541113181113314919039266947942816439793584770143362912270130442441) * 10 ^ 70 + 7083732299116445151882022038896417151858713134033689678425853209224773) * 10 ^ 70 + 6401799438134711786131943436201348417308812113381400922135084274610977) * 10 ^ 70 + 8412276650537283713296875293453105130217786008900490910725836196561184)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_256 :
Polynomial.coeff recurrence4Scalar1Left 256 = (((541036366578576034310583309 * 10 ^ 70 + 4925297556997894761055432049545984899600671106977482222303573856187130) * 10 ^ 70 + 2666649359237018319381423465444736422222579577276223210266072600905183) * 10 ^ 70 + 4684422495571062950007179796693163313355295936893253321557089878688233) * 10 ^ 70 + 8283114609679712699955257554309051774291071548489586547313464668157775
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_257 :
Polynomial.coeff recurrence4Scalar1Left 257 = (((604490970864071608605352423 * 10 ^ 70 + 5118704746486471947459957353477318600488786137540121650394066271915943) * 10 ^ 70 + 6805431984186432270781622063686058041216584751171092081748523203267665) * 10 ^ 70 + 7886925217983304624860430276261296561925900522472732799098993538797808) * 10 ^ 70 + 9799634438398554895966590872567988917240021886119264525318004229901371
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_258 :
Polynomial.coeff recurrence4Scalar1Left 258 = -((((1586680836797053520714582298 * 10 ^ 70 + 1181771622422485648467312444203179605178675087520037272664099903480924) * 10 ^ 70 + 6513330748328245425679444428575843575593921597357443526169361584997080) * 10 ^ 70 + 7596402529393918124462238391473073870190180187636260612059908008326388) * 10 ^ 70 + 9287632713379171453637695518743939904439839035432398509736452192998713)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_259 :
Polynomial.coeff recurrence4Scalar1Left 259 = (((2374070175360243059399651697 * 10 ^ 70 + 1223868900887043581883110307086785931313785772241191578689209206811929) * 10 ^ 70 + 9828421757374502821979276929319939208230953965472172467824740021059190) * 10 ^ 70 + 7504460624568642565908757768401636126573335047635678034364843291257111) * 10 ^ 70 + 225517292201114885826160022261180745006244178278691285004332593595950
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_260 :
Polynomial.coeff recurrence4Scalar1Left 260 = -((((2949249059872805588854129842 * 10 ^ 70 + 1922338246337094916945350284852356916797634701209351346911592014455409) * 10 ^ 70 + 1814964674181483434247470213909425619137384395529126602890756998144180) * 10 ^ 70 + 4495431946067174211675041431879166360956119946029549326079200672736364) * 10 ^ 70 + 9655670284996585047745891237283281518036400734253940764226561011736007)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_261 :
Polynomial.coeff recurrence4Scalar1Left 261 = (((3309162028234923841189522528 * 10 ^ 70 + 5495066075840522302971643728961779269496999275555087009959625999882305) * 10 ^ 70 + 3461832015689901105224031396650670800039133859210835576795921495450653) * 10 ^ 70 + 4917634941172765224169622141419756175822614122977866396049025229402171) * 10 ^ 70 + 8056583828493648659440119790565116107981355636251570020540819233276045
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_262 :
Polynomial.coeff recurrence4Scalar1Left 262 = -((((3464147294611502928550534691 * 10 ^ 70 + 3212038989379478256823539323597946177001021441801013891470305649510576) * 10 ^ 70 + 4140976021295187694392710453732732113896779730186852058548848031311982) * 10 ^ 70 + 9644196543065535604596096403092772991152786890214837026228093087959733) * 10 ^ 70 + 5900641183320379131521043156824832917555416929777164271848024258370112)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_263 :
Polynomial.coeff recurrence4Scalar1Left 263 = (((3435896743722092576699822692 * 10 ^ 70 + 4874381345018449957159769298514501139722413345980655689126030248640244) * 10 ^ 70 + 6322435710161061148260724982420658380148550617997558728936658147546323) * 10 ^ 70 + 2804878761260167395599789854066531232216143074631042717653148049925777) * 10 ^ 70 + 1574605642781189900389196917047833706690671839445864016767646107706412
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_264 :
Polynomial.coeff recurrence4Scalar1Left 264 = -((((3254627119080472140953501394 * 10 ^ 70 + 6835263084512342073791449499003023786048822707107209629564331611800638) * 10 ^ 70 + 65935875862900435352040498243550979177891398717327320195731272192281) * 10 ^ 70 + 8332011526277798634416213453130963242960982944770731446665148860686167) * 10 ^ 70 + 8074978489818245937707110212787300416804235543868339091963826364100891)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_265 :
Polynomial.coeff recurrence4Scalar1Left 265 = (((2955816345700090159822779913 * 10 ^ 70 + 9323463551720500986780480543344711373153425037542952090977903866309391) * 10 ^ 70 + 8502463321585417432925038575629364783295618190263312874390580418289622) * 10 ^ 70 + 9742162592146316325312714203927760934785674367748335702448993352251615) * 10 ^ 70 + 3914199659862565434742793855418746087617410041391643314435255408377914
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_266 :
Polynomial.coeff recurrence4Scalar1Left 266 = -((((2576873232289360510631625789 * 10 ^ 70 + 7964430774688375858116968248778220997238544105727288286132663059779535) * 10 ^ 70 + 8617820164626329222441504276030776168998712188922849586408408026299282) * 10 ^ 70 + 7193398376715435018032947623385200473027485730277242620586810675000138) * 10 ^ 70 + 6332624753984012204004501977512870755520943495288566336898590905426579)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_267 :
Polynomial.coeff recurrence4Scalar1Left 267 = (((2154076342018371345042222019 * 10 ^ 70 + 6526783476919404825749304446591595145323419183336420620808581632068033) * 10 ^ 70 + 1809275756767208563992825875007513365047890095346040617055586772947330) * 10 ^ 70 + 9432781046244196997108075980661907051086645296816098049749159923903028) * 10 ^ 70 + 5371257929221378132996534696267629939521220561769716949345163288689228
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_268 :
Polynomial.coeff recurrence4Scalar1Left 268 = -((((1720047734557428837083072656 * 10 ^ 70 + 9830981548104226022505837348132070650130019696009235002753420329900172) * 10 ^ 70 + 9784547553267853538184181221228080411869315560716825042856700850379194) * 10 ^ 70 + 5427825224353713519208717944330109215853213200461879653305109559821361) * 10 ^ 70 + 1998328271444855841707090843592475765755871657520988808771480595363404)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_269 :
Polynomial.coeff recurrence4Scalar1Left 269 = (((1301933263640915454046416562 * 10 ^ 70 + 1047765517288697629922192428361121009171910745415604408111396462056079) * 10 ^ 70 + 1650049774484133381600892861410014899407282923006876974869457869387360) * 10 ^ 70 + 6730468170955694546646052992320668255169034566112229168654302315383417) * 10 ^ 70 + 6045311848026358311869646845904133507688561111154883678175115199845418
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_270 :
Polynomial.coeff recurrence4Scalar1Left 270 = -((((920358764350887398259341869 * 10 ^ 70 + 5063340318057849730090473893284667107205107962256002815983684742864199) * 10 ^ 70 + 1587710836110412952142533190566810286516054200790266650205383145158984) * 10 ^ 70 + 4309923243996374311601742843224472833495944163407112403674152994229249) * 10 ^ 70 + 9712774156468948091606606211657018095719445920626592571381410684473132)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_271 :
Polynomial.coeff recurrence4Scalar1Left 271 = (((589135595178670083182027202 * 10 ^ 70 + 6732462447171459339575856492477783970101177568330814336564975926662045) * 10 ^ 70 + 8999398474510218759175567444756595095746123673145659372678521274616432) * 10 ^ 70 + 7424100551177898165927566746125474827138892748727656463330358450024849) * 10 ^ 70 + 1918321316201057021928986953950284358376585381012710213029816198900085