Recurrence 5 lookup certificate: Scalar1Second 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.recurrence5Scalar1Second_coeff_313 :
Polynomial.coeff recurrence5Scalar1Second 313 = (((371834719738054444094502886692588216050571107502938195010843 * 10 ^ 70 + 3835040054944701274539126390631053351721154953289689319189057338925077) * 10 ^ 70 + 6672469764519947497062810896670906580790123312864855682568367198916030) * 10 ^ 70 + 7960061838914315616896508135943415438074584220394718553504475825442136) * 10 ^ 70 + 6216649162656010769908561383097006756322451340852174820275114878072244
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_314 :
Polynomial.coeff recurrence5Scalar1Second 314 = -((((177507602910461013637224763724988037637233669981703304399881 * 10 ^ 70 + 7319938681601143041318316195702810385766665879884599326872802339879167) * 10 ^ 70 + 4695122184111924141993357239079880744411769693823872574078281300927820) * 10 ^ 70 + 6255410805532866430465823256050427036213699994295935274784556037507897) * 10 ^ 70 + 6234220833146489178072601543191649017131514171563001604291783465294868)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_315 :
Polynomial.coeff recurrence5Scalar1Second 315 = (((81984773373159359630707702317499426127859248433625150965062 * 10 ^ 70 + 558216272346159698749341018288284757318536944724633583092550614675564) * 10 ^ 70 + 6699666339290067658917426042034355339444184387671003449542724507147637) * 10 ^ 70 + 8839464487938377363826236550952141039026471198937698297669052135689300) * 10 ^ 70 + 6544523912380558559443070074512337711626909674355894478456574303375652
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_316 :
Polynomial.coeff recurrence5Scalar1Second 316 = -((((36708586584393915271825808620380502367107978649706848455316 * 10 ^ 70 + 1265362642352816977990748756115640925423105164004158432540504683888093) * 10 ^ 70 + 8082686479320100446630601633971980464476033265985428919964933596751827) * 10 ^ 70 + 4522457304957968357904507153296103825338612044817052332392580588319814) * 10 ^ 70 + 4242379799310427643861331054446953319444977889125003608379272999831384)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_317 :
Polynomial.coeff recurrence5Scalar1Second 317 = (((15949488319001086746067107223350996962628542249589361957748 * 10 ^ 70 + 4588414723283039812189081176727793031037283000227354419115050616821477) * 10 ^ 70 + 8381037600503636717754673503097418313453946223746702742204052284083730) * 10 ^ 70 + 293821439950232774525954612102668809245315732945491881512985657257405) * 10 ^ 70 + 6658278276157499338020783822105063399646221205575268084556324426930968
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_318 :
Polynomial.coeff recurrence5Scalar1Second 318 = -((((6725388598180566579070652854606044984060843451971034555456 * 10 ^ 70 + 2436869464098807226635782097042827108807855993180589291075569768025871) * 10 ^ 70 + 3783913092475798704824865492072340193269024512390861227171819971810476) * 10 ^ 70 + 6301222487246808775494029389483307490235100500595193706264622156925606) * 10 ^ 70 + 6414666612112388322332386845007263049307980482185036604236203970247011)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_319 :
Polynomial.coeff recurrence5Scalar1Second 319 = (((2750203127528861247934827898385430120446721454530324238733 * 10 ^ 70 + 5771627232336358332134584354232831353161649632326631145415000663005372) * 10 ^ 70 + 4465770284058463109286184076051107738358093542802183889425926597788737) * 10 ^ 70 + 7059031956316939471074659475808843774305782608333065863635166577567196) * 10 ^ 70 + 4692461114695525963533338345949505434106781332891887625624477616605
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_320 :
Polynomial.coeff recurrence5Scalar1Second 320 = -((((1088900000501486070304411951160644874878116852013645714258 * 10 ^ 70 + 762598206768866447954309957348173747229286388343734761549928088604539) * 10 ^ 70 + 1550238279381474588325510609351849187834543406946511697517440599009166) * 10 ^ 70 + 8157559547736819268892751128490603499568282106075833161252807073182516) * 10 ^ 70 + 8651001053705641173530492642382152760888524576302131154008101338588434)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_321 :
Polynomial.coeff recurrence5Scalar1Second 321 = (((416312306207089145211688256445271782946561170969725031859 * 10 ^ 70 + 6959684250739117688956435991114784448895975248928989212703963899826862) * 10 ^ 70 + 1924964945700986214686426044844115891247001013616346152542947843388498) * 10 ^ 70 + 7033740069828252222402936197046403898855995964848920326428898307333727) * 10 ^ 70 + 594704526839482031568353767610018440621954652280549840576594626973778
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_322 :
Polynomial.coeff recurrence5Scalar1Second 322 = -((((153054841661330134813535394679392618328113375580062251839 * 10 ^ 70 + 4373069189388828934173484640169492106143446519198957307768803760621982) * 10 ^ 70 + 2892390283795357182699165381262347379356491949919858357793173226705577) * 10 ^ 70 + 8387642207423861011353288619068697905283494432000885960275736890088343) * 10 ^ 70 + 6117765015910464615372454134592896075463685776054920353304599032186528)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_323 :
Polynomial.coeff recurrence5Scalar1Second 323 = (((53758709389451455276748321217364881520828664616024584891 * 10 ^ 70 + 2705831840540353460594388705718743627181322002882041707530287729001893) * 10 ^ 70 + 4594127682012560227220880938962871177996827293287966841282882307827705) * 10 ^ 70 + 3517710408288316120211938326238317576340360538779477077524902872119627) * 10 ^ 70 + 3802630356969652083630893208994631579294035465877817849612048591724174
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_324 :
Polynomial.coeff recurrence5Scalar1Second 324 = -((((17848121292177343208672838772466027451845748273154659950 * 10 ^ 70 + 8506756300437992487683319509861512256570317415592816757503430360641551) * 10 ^ 70 + 6270359437080820459320205584420550520929325817798658957038208532273224) * 10 ^ 70 + 4001833878970443388659647319045355487696185660807487296855522102377495) * 10 ^ 70 + 7158875250547590459638346885558842665396882202097984803753600373755716)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_325 :
Polynomial.coeff recurrence5Scalar1Second 325 = (((5494263070768968859006623384828314199564831227244713402 * 10 ^ 70 + 2949654569765502573525179346879861078055508078916475982638121942441118) * 10 ^ 70 + 498899352185584956231338225170670092964317115319911794091691407594258) * 10 ^ 70 + 8098983089856391282214674782027426848800424761485566860677775648139233) * 10 ^ 70 + 6513781730676131960403975179098819593722110868978680507202239555181655
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_326 :
Polynomial.coeff recurrence5Scalar1Second 326 = -((((1505571554160591367493920475053265348868448398220830693 * 10 ^ 70 + 5087889756400908502109937949429410160686500558902726207247643631923390) * 10 ^ 70 + 9638631821599033450285073520623829683651782726679728691818401104014089) * 10 ^ 70 + 3204801767399537169117095499029626514585960309985190445444233826424891) * 10 ^ 70 + 5476046233900889547622676339470348654543635052844261861492574466184932)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_327 :
Polynomial.coeff recurrence5Scalar1Second 327 = (((327516982504030173552587967116212527413060418755711797 * 10 ^ 70 + 3338574089468287695996826863424824267267450088604513462252142158487994) * 10 ^ 70 + 4147656411634880837412309006339267929242533207366262799341809163352403) * 10 ^ 70 + 9625351966189714070957047403609957072591819333434403565410901435513424) * 10 ^ 70 + 1964159484952507170125508715559630949157855124663676439678215981041394
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_328 :
Polynomial.coeff recurrence5Scalar1Second 328 = -((((27646967760087116145390054605607495358212899851712060 * 10 ^ 70 + 2059751239202216454815772662800343748091022579536553165691792391557187) * 10 ^ 70 + 4778965747338864590179193595168452143944827772864601123598241074266795) * 10 ^ 70 + 7358085516990910945664890649246849765144461574502103266334909721401153) * 10 ^ 70 + 4625364414457159055831618251438656190210512551015738036390501098431386)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_329 :
Polynomial.coeff recurrence5Scalar1Second 329 = -((((25916699635544732248801953050603069415530300815673858 * 10 ^ 70 + 1872142744779414415241074207055014667747353880921129029052646732636319) * 10 ^ 70 + 755813598577956214660502886580057330898553708926666361998836089227109) * 10 ^ 70 + 4475251235132167281633112721386109992656984953655669402441973612523113) * 10 ^ 70 + 5488344709534422207591880985718849145302852891437832317307082559194900)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_330 :
Polynomial.coeff recurrence5Scalar1Second 330 = (((22972729033562199436671074680158377329426355898657826 * 10 ^ 70 + 1628979571894024677733366705654024221855981595807509666614626386101098) * 10 ^ 70 + 4098724761689429606592988816047131423636133963214904473623836013529793) * 10 ^ 70 + 9803882449475159251799734562228869277985655786018640696086397897299443) * 10 ^ 70 + 4128585027743002723763012814399349833626006109911473040374035487681804
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_331 :
Polynomial.coeff recurrence5Scalar1Second 331 = -((((13296036062477631952671158061407299105239202299006503 * 10 ^ 70 + 1339788225127190106685395092958828225516187776211937815853204254253009) * 10 ^ 70 + 435771328164312164469174102880255207670152541904349469261031176585403) * 10 ^ 70 + 4179528129304302336546682260538689344290229680607067855945007774855914) * 10 ^ 70 + 1411686713135647120354759002790863886580813010571332402335800853668066)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_332 :
Polynomial.coeff recurrence5Scalar1Second 332 = (((6602150596631818407269041897399009679289274863152224 * 10 ^ 70 + 5891857188228177152372479821434509261443089466150627475289565823858362) * 10 ^ 70 + 3433718691687042638565587862783810602409812011247219707555874736224463) * 10 ^ 70 + 3694668462452937983346979187845432282169332090614724024214224298430756) * 10 ^ 70 + 418166451091328889451348131474903646728013157842624469852188478884019
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_333 :
Polynomial.coeff recurrence5Scalar1Second 333 = -((((3028142953401653330234505335733666491471209195500936 * 10 ^ 70 + 8568092471288498628114681953366454772406938797366731048662113702771931) * 10 ^ 70 + 3661371020014994612293365331764823723106660749260730495444926643486870) * 10 ^ 70 + 3842101376768259411981054500431035985981627325624295387070640067014987) * 10 ^ 70 + 528342779370547850073261899788819320875211156076531774490999767155350)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_334 :
Polynomial.coeff recurrence5Scalar1Second 334 = (((1324804971982629346927573974915605508498522664878683 * 10 ^ 70 + 1758429417627581466061929863369146798399981900804159783601550545892801) * 10 ^ 70 + 4397796099621108613116766282388197125046810332965062646268577115282078) * 10 ^ 70 + 8958783659342848804636931103700876707854971527145626213774253642106814) * 10 ^ 70 + 5291505268827630689668339538931286574632043399323195732252603451707156
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_335 :
Polynomial.coeff recurrence5Scalar1Second 335 = -((((562358636115556575648827387778285915231530328612444 * 10 ^ 70 + 9782926018583052534156190096777046889683715962870330888926401030833264) * 10 ^ 70 + 3838476269317402553372214306217006062836972676416562568645426743986872) * 10 ^ 70 + 7840811744304902392343779859111132107152994644342412325199520329574126) * 10 ^ 70 + 4161460169827091515488081783235126501831890113629980261325336023884972)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_336 :
Polynomial.coeff recurrence5Scalar1Second 336 = (((233821476619915351287719971031453447436881297864855 * 10 ^ 70 + 5892809704236996860710724292756064068393008800632043120600582489656925) * 10 ^ 70 + 9391301992198802285293181945981798873117861831986622064852651257267665) * 10 ^ 70 + 7026677443207661426588399966677103599061525017834025935431469088996329) * 10 ^ 70 + 924818141655611076945270205059583372454066838857987123103959127962584
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_337 :
Polynomial.coeff recurrence5Scalar1Second 337 = -((((95685220416366701224991670523065027753388680144316 * 10 ^ 70 + 8678621836812182541478551377629219564960759985410247997880333239374885) * 10 ^ 70 + 4197745600059924079361060268591268754825172016121608920332530052054247) * 10 ^ 70 + 3337117072717385915525035336996815187820203465783831721172498912226768) * 10 ^ 70 + 3668579989167954566801165223432256268112531324273471720448589209008783)