{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["2"]},{"denominator":["1"],"numerator":["1"]}],"shape":"euler_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["1","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","1","-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"Triangle of coefficients of polynomials u(n,x) jointly generated with A112351; see the Formula section."},"identifying_rows":2,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["0","-9","-162","36","2430","-4275","1980"],["0","-6","-185","26","3721","-7100","3544"],["0","-1","-71","-79","2137","-4290","2304"],["0","0","-9","-55","560","-1136","640"],["0","0","0","-9","57","-112","64"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","0","-27","-486","108","7290","-12825","5940"],["0","0","-18","-555","78","11163","-21300","10632"],["0","0","-3","-213","-237","6411","-12870","6912"],["0","0","0","-27","-165","1680","-3408","1920"],["0","0","0","0","-27","171","-336","192"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0","0","-9","-162","36","2430","-4275","1980"],["0","0","0","-6","-185","26","3721","-7100","3544"],["0","0","0","-1","-71","-79","2137","-4290","2304"],["0","0","0","0","-9","-55","560","-1136","640"],["0","0","0","0","0","-9","57","-112","64"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["-4","-82","-300","-2","1252","-864"],["-4","-116","-314","1232","2860","-2608"],["-1","-56","-185","1060","1396","-2688"],["0","-9","-64","308","288","-1024"],["0","0","-9","30","32","-128"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-12","-246","-900","-6","3756","-2592"],["0","-12","-348","-942","3696","8580","-7824"],["0","-3","-168","-555","3180","4188","-8064"],["0","0","-27","-192","924","864","-3072"],["0","0","0","-27","90","96","-384"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["0","0","-4","-82","-300","-2","1252","-864"],["0","0","-4","-116","-314","1232","2860","-2608"],["0","0","-1","-56","-185","1060","1396","-2688"],["0","0","0","-9","-64","308","288","-1024"],["0","0","0","0","-9","30","32","-128"]]},"deriv_order":2,"shift":1},{"coeff":{"coeffs":[["4","43","66","-277","164"],["4","74","19","-880","600"],["1","45","13","-786","768"],["0","9","28","-304","384"],["0","0","9","-48","64"]]},"deriv_order":0,"shift":2},{"coeff":{"coeffs":[["0","12","129","198","-831","492"],["0","12","222","57","-2640","1800"],["0","3","135","39","-2358","2304"],["0","0","27","84","-912","1152"],["0","0","0","27","-144","192"]]},"deriv_order":1,"shift":2},{"coeff":{"coeffs":[["0","0","4","43","66","-277","164"],["0","0","4","74","19","-880","600"],["0","0","1","45","13","-786","768"],["0","0","0","9","28","-304","384"],["0","0","0","0","9","-48","64"]]},"deriv_order":2,"shift":2}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0,1],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["1"],["1","4"]],"recurrence":{"denominator":{"coeffs":[["0","3","0","3","-12"],["0","2","15","152","88"],["1","-9","61","-114","0"],["0","9","-44","80","-128"],["0","0","9","-48","64"]]},"terms":[{"coeff":{"coeffs":[["0","1","4","36","32","-61","-12"],["0","2","9","30","-69","-12","40"],["0","1","17","-35","-145","162","0"],["0","0","9","-17","-104","240","-128"],["0","0","0","9","-57","112","-64"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["0","2","44","210","676","256"],["0","0","54","272","292","48"],["1","2","17","68","-436","-384"],["0","9","-8","-68","-32","0"],["0","0","9","-30","-32","128"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["1"],"operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["2"]},{"denominator":["1"],"numerator":["1"]}],"shape":"euler_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["1","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","1","-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_leader_shift":2,"parent_valid_from_base":0,"quotients":[{"differentiations":[{"coeff":{"coeffs":[["0","0","0","108","3105","29484","65340","-437184","-1235898","5410800","3055644","-40350636","83073249","-86763420","51464160","-16581888","2267136"],["0","0","0","432","12285","102816","-19305","-3243402","-2874285","45788652","-26736399","-284436522","794229192","-984494952","663571008","-237399552","35500032"],["0","0","0","675","19926","150849","-438453","-7110180","5914782","125803125","-221978313","-688775157","2884238010","-4323568752","3341257344","-1334486016","218972160"],["0","0","0","513","17118","124686","-694548","-7510509","18932778","154148508","-493142580","-701192214","5127546456","-9401102784","8373459456","-3746525184","675938304"],["0","0","0","189","8316","64584","-474525","-4489641","17514873","101838789","-472794084","-343312749","4935800664","-10880597376","11101860864","-5560455168","1105035264"],["0","0","0","27","2187","20844","-151632","-1596834","6935382","41371803","-220519341","-151326468","2762725536","-6837032448","7755816960","-4301144064","944898048"],["0","0","0","0","243","3672","-16227","-324405","989172","10779561","-48638880","-77058864","883488384","-2256906240","2728083456","-1622605824","382205952"],["0","0","0","0","0","243","891","-29619","-7047","1388988","-4068144","-16873920","125535744","-311205888","382205952","-233570304","56623104"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","324","9315","88452","196020","-1311552","-3707694","16232400","9166932","-121051908","249219747","-260290260","154392480","-49745664","6801408"],["0","0","0","0","1296","36855","308448","-57915","-9730206","-8622855","137365956","-80209197","-853309566","2382687576","-2953484856","1990713024","-712198656","106500096"],["0","0","0","0","2025","59778","452547","-1315359","-21330540","17744346","377409375","-665934939","-2066325471","8652714030","-12970706256","10023772032","-4003458048","656916480"],["0","0","0","0","1539","51354","374058","-2083644","-22531527","56798334","462445524","-1479427740","-2103576642","15382639368","-28203308352","25120378368","-11239575552","2027814912"],["0","0","0","0","567","24948","193752","-1423575","-13468923","52544619","305516367","-1418382252","-1029938247","14807401992","-32641792128","33305582592","-16681365504","3315105792"],["0","0","0","0","81","6561","62532","-454896","-4790502","20806146","124115409","-661558023","-453979404","8288176608","-20511097344","23267450880","-12903432192","2834694144"],["0","0","0","0","0","729","11016","-48681","-973215","2967516","32338683","-145916640","-231176592","2650465152","-6770718720","8184250368","-4867817472","1146617856"],["0","0","0","0","0","0","729","2673","-88857","-21141","4166964","-12204432","-50621760","376607232","-933617664","1146617856","-700710912","169869312"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","108","3105","29484","65340","-437184","-1235898","5410800","3055644","-40350636","83073249","-86763420","51464160","-16581888","2267136"],["0","0","0","0","0","432","12285","102816","-19305","-3243402","-2874285","45788652","-26736399","-284436522","794229192","-984494952","663571008","-237399552","35500032"],["0","0","0","0","0","675","19926","150849","-438453","-7110180","5914782","125803125","-221978313","-688775157","2884238010","-4323568752","3341257344","-1334486016","218972160"],["0","0","0","0","0","513","17118","124686","-694548","-7510509","18932778","154148508","-493142580","-701192214","5127546456","-9401102784","8373459456","-3746525184","675938304"],["0","0","0","0","0","189","8316","64584","-474525","-4489641","17514873","101838789","-472794084","-343312749","4935800664","-10880597376","11101860864","-5560455168","1105035264"],["0","0","0","0","0","27","2187","20844","-151632","-1596834","6935382","41371803","-220519341","-151326468","2762725536","-6837032448","7755816960","-4301144064","944898048"],["0","0","0","0","0","0","243","3672","-16227","-324405","989172","10779561","-48638880","-77058864","883488384","-2256906240","2728083456","-1622605824","382205952"],["0","0","0","0","0","0","0","243","891","-29619","-7047","1388988","-4068144","-16873920","125535744","-311205888","382205952","-233570304","56623104"]]},"deriv_order":2}],"shift":0}],"row_annihilation":{"kind":"system","system":{"generators":[{"annihilator":{"terms":[{"coeff":{"coeffs":[["-3","-3","0"],["-2","0","-16"],["3","-20","32"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","15","-36","48"],["-1","-2","40","-64"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","1","3","-36","32"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["3"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","-63","-144","16092","114408","-239994","-1967976","5566428","5078808","-42992127","82731384","-83373696","48301056","-15298560","2064384"],["0","0","0","0","-279","1188","97119","445086","-2909853","-10085796","55212921","-2533410","-370437300","904476708","-1055702160","684878976","-238316544","34873344"],["0","0","0","0","-486","5877","214731","491814","-9242802","-13001067","185719527","-170632116","-1175584266","3835183572","-5263579872","3857331456","-1483130880","236224512"],["0","0","0","0","-414","9387","231174","18864","-12507102","2398815","279359118","-526066434","-1745584992","8058973968","-13162377600","10982532096","-4694482944","817496064"],["0","0","0","0","-171","6939","131625","-256347","-8424252","13002120","211341636","-618471828","-1356555114","9037052208","-17517337344","16677218304","-7963582464","1525874688"],["0","0","0","0","-27","2421","40095","-129753","-3026970","6986898","88972074","-326974266","-653023944","5545094976","-12334648320","13216628736","-7033356288","1493434368"],["0","0","0","0","0","324","6426","-13896","-604620","1061748","22419234","-80604288","-215309664","1807066368","-4353675264","5102272512","-2971533312","688914432"],["0","0","0","0","0","0","486","1782","-59238","-14094","2777976","-8136288","-33747840","251071488","-622411776","764411904","-467140608","113246208"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","-693","-14922","-89316","38304","1320210","-136404","-8551116","976752","59326587","-139481010","154774872","-95262912","31486464","-4386816"],["0","0","0","0","0","-2853","-53766","-188451","1425348","6406317","-16844058","-48041613","117169632","216058536","-992972772","1427203296","-1042027776","392914944","-61046784"],["0","0","0","0","0","-4608","-75357","-59769","3521556","5452434","-66605517","-29922669","524002446","-312468732","-1954226664","4385914560","-4020539904","1778208768","-313196544"],["0","0","0","0","0","-3636","-51723","111654","3297816","-2472264","-81156519","118717650","723132738","-1964524644","248371776","4384680192","-6128547840","3400335360","-701890560"],["0","0","0","0","0","-1395","-17991","93483","1445409","-4321098","-42729714","158777226","350956908","-2467539180","4077420192","-1775890944","-1777029120","2058043392","-579207168"],["0","0","0","0","0","-207","-2943","23013","318357","-1629018","-11404422","73847808","48167460","-1252881648","3742565760","-5097793536","3456073728","-1028063232","70778880"],["0","0","0","0","0","0","-162","2142","34038","-299970","-1430892","16953084","-14831424","-286320960","1298253312","-2528796672","2575761408","-1342439424","283115520"],["0","0","0","0","0","0","0","324","1188","-39492","-9396","1851984","-5424192","-22498560","167380992","-414941184","509607936","-311427072","75497472"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","-279","-6354","-42876","-16272","634374","503820","-5255172","-1032480","37709145","-83415114","90153144","-54627264","17865216","-2469888"],["0","0","0","0","0","0","-1143","-23382","-108513","483696","3576951","-4337226","-36364383","50939388","198435744","-683981676","913287744","-642263040","236482560","-36126720"],["0","0","0","0","0","0","-1836","-33975","-86967","1368720","4977558","-24830631","-65886723","273324510","201966048","-1933292448","3383557632","-2825183232","1185841152","-201719808"],["0","0","0","0","0","0","-1440","-24849","-18198","1407960","2513916","-35466741","-28937898","460218726","-343200564","-2196118944","5639827968","-5764386816","2798567424","-534380544"],["0","0","0","0","0","0","-549","-9693","2457","692703","555030","-22027626","7664058","327116340","-669929616","-834549120","4243857408","-5526503424","3157327872","-684195840"],["0","0","0","0","0","0","-81","-1953","-1593","173511","166698","-6883866","6228468","114064416","-350371008","19643904","1339416576","-2295005184","1568931840","-396361728"],["0","0","0","0","0","0","0","-162","-918","18558","44190","-916596","860112","16673472","-61191936","40089600","160137216","-353894400","273678336","-75497472"]]},"deriv_order":2}],"step_multiplier":{"coeffs":[["0","0","0","27","486","1701","-8100","-17739","113238","-202581","176904","-77760","13824"],["0","0","0","81","1215","486","-44226","-243","552339","-1414260","1547424","-808704","165888"],["0","0","0","81","972","-3402","-49572","127089","680400","-2943216","4261248","-2737152","663552"],["0","0","0","27","243","-2187","-14175","94284","151632","-1736640","3608064","-2985984","884736"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","9","9","-2043","-9747","49059","95067","-803817","1810863","-2108808","1388736","-493056","73728"],["0","0","0","63","234","-10071","-36720","364689","207522","-5666409","16224516","-22284720","16776576","-6681600","1105920"],["0","0","0","162","711","-21717","-52326","956664","-580581","-14559669","54220212","-88513344","76640256","-34430976","6340608"],["0","0","0","198","819","-24912","-30726","1175850","-2057589","-16997256","84530736","-164471040","164081664","-83312640","17104896"],["0","0","0","117","396","-14742","-2376","701001","-1977372","-8952336","61532352","-142414848","163086336","-93192192","21233664"],["0","0","0","27","63","-3519","2997","165456","-628128","-1741824","16803072","-45563904","59277312","-37748736","9437184"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-9","-45","1575","10575","-29511","-134487","577773","-691227","-81540","974736","-987264","433152","-73728"],["0","0","0","-36","-234","4680","25506","-173772","-416934","3028752","-3942162","-3065256","12773952","-13432320","6377472","-1179648"],["0","0","0","-54","-432","5562","31536","-256770","-508032","5406750","-6148224","-19577376","60583680","-67405824","34947072","-7077888"],["0","0","0","-36","-342","3384","25452","-172476","-549126","4716792","-2126304","-42180480","122047488","-147234816","84344832","-18874368"],["0","0","0","-9","-99","927","8847","-56322","-255744","2037312","-34560","-27800064","86851584","-117374976","75497472","-18874368"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","9","189","729","-6543","-29241","135351","172179","-1691685","3789828","-4356864","2833920","-995328","147456"],["0","0","0","0","27","486","405","-27972","-37179","719766","-387909","-7529112","24140592","-34407936","26376192","-10616832","1769472"],["0","0","0","0","27","405","-1134","-30726","43983","912465","-2354508","-8331984","45925056","-85045248","78962688","-37158912","7077888"],["0","0","0","0","9","108","-810","-9540","46089","291600","-1709856","-1347840","25069824","-64512000","75202560","-42467328","9437184"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","-9","-63","882","3186","-40149","17037","648540","-2410992","3979584","-3488256","1585152","-294912"],["0","0","0","-54","-279","6300","12798","-293922","367713","4440420","-19575216","35626176","-33744384","16404480","-3244032"],["0","0","0","-108","-405","13716","10530","-651240","1416123","9036360","-50757840","105463296","-110536704","58392576","-12386304"],["0","0","0","-90","-252","11736","-3132","-560574","1745496","6911136","-51152256","121568256","-141631488","81985536","-18874368"],["0","0","0","-27","-63","3519","-2997","-165456","628128","1741824","-16803072","45563904","-59277312","37748736","-9437184"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","9","45","-1116","-2610","52353","-35775","-850014","2970324","-3970080","1841472","769536","-1069056","294912"],["0","0","0","27","162","-3132","-9936","148959","-12474","-2690982","7531056","-3843936","-12842496","23224320","-15040512","3538944"],["0","0","0","27","216","-2862","-15444","147339","249156","-3623616","4427136","23618304","-81644544","104620032","-61931520","14155776"],["0","0","0","9","99","-927","-8847","56322","255744","-2037312","34560","27800064","-86851584","117374976","-75497472","18874368"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","-9","-162","-135","9324","12393","-239922","129303","2509704","-8046864","11469312","-8792064","3538944","-589824"],["0","0","0","0","-18","-270","756","20484","-29322","-608310","1569672","5554656","-30616704","56696832","-52641792","24772608","-4718592"],["0","0","0","0","-9","-108","810","9540","-46089","-291600","1709856","1347840","-25069824","64512000","-75202560","42467328","-9437184"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["-2","9","-4"],["1","-11","-8"],["3","-20","32"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","12","-24","12"],["-1","10","-14","32"],["-1","-2","40","-64"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","1","6","-15","8"],["0","1","3","-36","32"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","63","-180","-19143","-63702","879381","2455596","-15832449","-1191942","116276148","-272320956","303939936","-186782976","60917760","-8257536"],["0","0","0","0","216","-2115","-81837","-84681","4527756","4038687","-94390353","92816685","625097682","-2024887032","2713470336","-1919766528","705724416","-106463232"],["0","0","0","0","270","-5139","-127197","147960","8002701","-6193800","-186184764","393729687","1150224570","-5551428528","9034114176","-7406097408","3082862592","-519045120"],["0","0","0","0","144","-4977","-91989","293445","6428691","-14184774","-163742418","544227174","965279376","-7208713728","14153849856","-13428965376","6339428352","-1193803776"],["0","0","0","0","27","-2097","-32940","146016","2605059","-7745409","-75934314","313388082","496648152","-4853462976","10999968768","-11833344000","6286049280","-1328283648"],["0","0","0","0","0","-324","-5940","18108","567900","-1252152","-20771640","80304912","188326080","-1698375168","4144324608","-4880203776","2847670272","-660602880"],["0","0","0","0","0","0","-486","-1782","59238","14094","-2777976","8136288","33747840","-251071488","622411776","-764411904","467140608","-113246208"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","693","12006","21735","-522360","-1886697","5236326","16459065","-31270428","-102335724","371933352","-493529184","338529024","-120195072","17547264"],["0","0","0","0","0","2160","32688","-23823","-1906470","-2072610","36590832","21313881","-275020002","-10979712","1534359888","-2923317504","2486145024","-1039122432","173998080"],["0","0","0","0","0","2448","32409","-113697","-2295027","2667069","57004182","-81797040","-507835872","1118310408","824305824","-4620231936","5482100736","-2828943360","556793856"],["0","0","0","0","0","1188","14346","-89460","-1187820","3955932","34479810","-129294252","-280750320","1846212912","-2574211968","22966272","2790162432","-2292645888","580386816"],["0","0","0","0","0","207","2781","-22167","-289611","1481076","10027854","-64166688","-42295932","1060423056","-3096176256","4075370496","-2591391744","651755520","-4718592"],["0","0","0","0","0","0","162","-1818","-31878","267930","1332828","-15483960","13431744","263647872","-1199066112","2343223296","-2393505792","1250426880","-264241152"],["0","0","0","0","0","0","0","-324","-1188","39492","9396","-1851984","5424192","22498560","-167380992","414941184","-509607936","311427072","-75497472"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","279","5517","22977","-132255","-831717","1201959","8472411","-11515797","-53354862","180896832","-242916768","172323072","-64051200","9879552"],["0","0","0","0","0","0","864","15273","29349","-664236","-2003706","12112497","27463401","-123528078","-110914596","972493776","-1710216576","1441207296","-610983936","104988672"],["0","0","0","0","0","0","972","15786","-1404","-936360","-1092276","23521266","11072052","-292417668","215716608","1540721088","-3975814656","4101525504","-2009235456","386924544"],["0","0","0","0","0","0","468","7659","-8991","-558999","-94239","17537796","-12378258","-251642700","547045488","692507520","-3593097216","4725817344","-2714959872","589824000"],["0","0","0","0","0","0","81","1791","189","-159651","-85626","6247368","-6997752","-101328192","323450496","-26044416","-1244971008","2158755840","-1486356480","377487360"],["0","0","0","0","0","0","0","162","918","-18558","-44190","916596","-860112","-16673472","61191936","-40089600","-160137216","353894400","-273678336","75497472"]]},"deriv_order":2}],"step_multiplier":{"coeffs":[["0","0","0","27","486","1701","-8100","-17739","113238","-202581","176904","-77760","13824"],["0","0","0","81","1215","486","-44226","-243","552339","-1414260","1547424","-808704","165888"],["0","0","0","81","972","-3402","-49572","127089","680400","-2943216","4261248","-2737152","663552"],["0","0","0","27","243","-2187","-14175","94284","151632","-1736640","3608064","-2985984","884736"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","18","126","-2250","-14634","58914","151578","-1083726","2358450","-2699676","1758816","-619776","92160"],["0","0","0","135","1017","-14085","-78327","514377","641331","-8807535","23413995","-30985308","22772448","-8914176","1456128"],["0","0","0","387","2709","-39951","-168345","1695789","293355","-27669249","90714681","-138991680","115376256","-50245632","9031680"],["0","0","0","558","3348","-60876","-170640","2768094","-2297268","-42747696","175356576","-310711680","290589696","-140451840","27721728"],["0","0","0","432","2070","-50508","-73872","2369196","-4310118","-33795792","177609888","-363267072","380768256","-202899456","43646976"],["0","0","0","171","603","-21267","-4887","1006884","-2837376","-12735360","88715520","-208825344","243818496","-142147584","33030144"],["0","0","0","27","63","-3519","2997","165456","-628128","-1741824","16803072","-45563904","59277312","-37748736","9437184"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-18","-144","2124","16884","-44280","-210492","932148","-1274724","341226","940860","-1139040","527616","-92160"],["0","0","0","-81","-702","7695","54324","-279045","-783918","5217777","-7613352","-1418634","15163200","-17093376","8294400","-1548288"],["0","0","0","-144","-1341","11997","87282","-516726","-1328265","10770489","-13108284","-26358912","88016256","-97606656","50061312","-10027008"],["0","0","0","-126","-1251","10332","85302","-482490","-1659339","12055716","-5959440","-82790208","226566144","-259301376","142147584","-30670848"],["0","0","0","-54","-567","4833","44307","-253935","-1104840","7847280","139968","-88542720","249302016","-307224576","182255616","-42467328"],["0","0","0","-9","-99","927","8847","-56322","-255744","2037312","-34560","-27800064","86851584","-117374976","75497472","-18874368"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","18","405","2133","-8199","-58563","182655","398223","-2651373","5432589","-5932512","3722112","-1271808","184320"],["0","0","0","0","63","1242","3321","-54144","-154143","1261170","300807","-14295852","39299904","-51835392","37711872","-14598144","2359296"],["0","0","0","0","81","1377","-324","-86670","-30375","2351997","-3130326","-23390208","94206240","-153861120","131715072","-58392576","10616832"],["0","0","0","0","45","648","-2322","-50508","104733","1508220","-4849200","-12457152","86303232","-177905664","180486144","-92012544","18874368"],["0","0","0","0","9","108","-810","-9540","46089","291600","-1709856","-1347840","25069824","-64512000","75202560","-42467328","9437184"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","-18","-234","9","2727","-40608","28404","772929","-3006369","5026968","-4410432","1995264","-368640"],["0","0","0","-117","-1053","7623","33966","-416907","303075","6991569","-28522044","50305968","-46664064","22311936","-4349952"],["0","0","0","-270","-1710","27009","67068","-1272888","1743822","19289421","-91548900","177201216","-177389568","90611712","-18726912"],["0","0","0","-288","-1287","34056","36666","-1604232","3464181","22093992","-127834416","274675968","-298414080","163528704","-35979264"],["0","0","0","-144","-459","18261","-621","-866457","2605500","10694160","-78335424","187978752","-222363648","130940928","-30670848"],["0","0","0","-27","-63","3519","-2997","-165456","628128","1741824","-16803072","45563904","-59277312","37748736","-9437184"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","18","144","-1287","-2007","92880","-66366","-1485135","5068197","-6776028","3541680","540288","-1281024","368640"],["0","0","0","63","504","-5328","-21834","268947","-67608","-4985874","15479154","-13800888","-10188864","28251648","-19648512","4718592"],["0","0","0","81","702","-7344","-44064","352917","577530","-7898958","12242016","30339360","-121326336","157870080","-93339648","21233664"],["0","0","0","45","441","-4311","-34299","228798","804870","-6754104","2160864","69980544","-208899072","264609792","-159842304","37748736"],["0","0","0","9","99","-927","-8847","56322","255744","-2037312","34560","27800064","-86851584","117374976","-75497472","18874368"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","-18","-351","-864","15867","41634","-375273","-42876","4201389","-11836692","15826176","-11625984","4534272","-737280"],["0","0","0","0","-45","-756","351","48456","7857","-1328076","1957581","13083768","-54757296","91104768","-79017984","35389440","-6488064"],["0","0","0","0","-36","-513","1944","40266","-90072","-1204065","4064364","9679824","-70994880","149557248","-154165248","79626240","-16515072"],["0","0","0","0","-9","-108","810","9540","-46089","-291600","1709856","1347840","-25069824","64512000","-75202560","42467328","-9437184"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["0","0","0","27","486","1701","-8100","-17739","113238","-202581","176904","-77760","13824"],["0","0","0","81","1215","486","-44226","-243","552339","-1414260","1547424","-808704","165888"],["0","0","0","81","972","-3402","-49572","127089","680400","-2943216","4261248","-2737152","663552"],["0","0","0","27","243","-2187","-14175","94284","151632","-1736640","3608064","-2985984","884736"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["0","-1","1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-1","-2"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"shift":2}]},"statement":"w(n) E = sum_nu H_nu S^nu L' (with any remainder removed by row annihilators of the parent), where L' is the parent rule at P'_n = P_(n+0) (valid from base 0) and E the input rule gauged by lambda(n)/delta(n) and composed with (or conjugated through) T = f(n, theta) = 1 + (2) theta + (1) theta^2; so the candidate rows satisfy the input rule at every base n >= 0 (the exceptional bases checked exactly), and agreement on the 2 identifying rows gives Q_n = lambda(n) T_n(P_(n+0)) for every n >= 0"},"method":"operator_division"},"status":"certified"},"input_first_index":0,"interlacing":{"from_index":1,"justification":"the parent theorem (LiuWangDerivativeLag) proves P_(m-1) strictly interlacing P_m for every m >= 1; T = f(n, theta) = 1 + (2) theta + (1) theta^2 is independent of n and maps every real-rooted polynomial to a real-rooted polynomial or zero, so by the Hermite--Kakeya--Obreschkoff theorem (both directions) T(P_(m-1)) and T(P_m) have weakly interlacing zeros; the nonzero gauge does not move zeros, so Q_(n-1) and Q_n interlace weakly (orientation not determined) for every n >= 1","kind":"weak","orientation":"unordered","status":"claimed"},"lean_declarations":["RealRooted.isMultiplierSequence_eval_of_roots_nonpos","RealRooted.isPFMultiplierSequence_eval_of_roots_nonpos","RealRooted.isMultiplierSequence_iff_preserves"],"lift_summary":{"hypotheses":[{"evidence":"the polynomial with ascending coefficients [1, 2, 1] is fixed; exact check: real-rooted = true, coefficients of one sign = true","name":"euler_polynomial_roots_nonpositive","statement":"the polynomial in theta is real-rooted with every root <= 0 for every n >= n0","status":{"kind":"verified"}},{"evidence":"lambda(n) = 1","name":"gauge_finite_nonzero","statement":"lambda(n) is finite and nonzero for every n >= n0","status":{"kind":"verified"}},{"evidence":"delta(n) != 0 for every integer n in [0, +inf) (exact; Taylor shift: the coefficients of delta(n) at n = 0 + u have one sign)","name":"operator_coefficients_defined","sign_decision":{"certificate":{"condition":"nonzero","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1"]},"numerator":["1"],"range":{"first":"0","last":null}},"decision":"holds"},"statement":"the operator coefficients are finite at every n >= n0 (their denominators do not vanish)","status":{"kind":"verified"}}],"identity":{"method":"forward_division","status":"certified"},"input_first_index":0,"input_interlacing":{"interlacing":{"from_index":1,"justification":{"premises":["the parent theorem (LiuWangDerivativeLag) proves P_(m-1) strictly interlacing P_m for every m >= 1; T = f(n, theta) = 1 + (2) theta + (1) theta^2 is independent of n and maps every real-rooted polynomial to a real-rooted polynomial or zero, so by the Hermite--Kakeya--Obreschkoff theorem (both directions) T(P_(m-1)) and T(P_m) have weakly interlacing zeros; the nonzero gauge does not move zeros, so Q_(n-1) and Q_n interlace weakly (orientation not determined) for every n >= 1"],"theorem":"Hermite--Kakeya--Obreschkoff theorem (N. Obreschkoff, Verteilung und Berechnung der Nullstellen reeller Polynome, 1963; see S. Fisk, Polynomials, Roots, and Interlacing, arXiv:math/0612833): real polynomials f, g have weakly interlacing zeros iff alpha f + beta g is real-rooted or zero for all real alpha, beta; a linear T independent of n that maps every real-rooted polynomial to a real-rooted polynomial or zero therefore maps interlacing pairs to pairs with weakly interlacing zeros (orientation not determined)"},"kind":"weak","orientation":"unordered"},"status":"proved"},"lean_replay":"not_attempted","operation":{"description":"f(n, theta) = 1 + (2) theta + (1) theta^2","kind":"preserver_image","operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["2"]},{"denominator":["1"],"numerator":["1"]}],"shape":"euler_polynomial"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["1","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","1","-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"relation":"Q_n = lambda(n) T_n(P_(n+0)) with T = f(n, theta) = 1 + (2) theta + (1) theta^2, for every n >= 0"},"parent_proof":{"route":"liu_wang_derivative_lag","statement":"every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign","status":"proved"},"root_transfer":{"input_conclusion":"every Q_n, n >= 0, is zero or real-rooted with roots in (-inf, 0]","input_root_region":{"upper":{"closed":true,"value":"0"}},"parent_hypothesis":"every parent row used is zero or real-rooted with all roots in (-inf, 0] (coefficients of one sign)","parent_root_region":{"upper":{"closed":true,"value":"0"}},"theorem":"Laguerre's theorem on multiplier sequences: if f is a real polynomial whose roots are all real and <= 0, then (f(k))_(k >= 0) is a multiplier sequence, so x^k -> f(k) x^k maps every real-rooted polynomial to a real-rooted polynomial or zero (Laguerre; see T. Craven and G. Csordas, Multiplier sequences for fields, Illinois J. Math. 21 (1977); Polya--Schur, Theorem 40 of P. Branden, arXiv:1410.6601: sum_k f(k) x^k / k! = f(theta) e^x = C e^x x^m prod (1 + x/a_j), a_j > 0); f(k) has one sign for k >= 0, so coefficients of one sign stay of one sign; applied to f(n, .) for each n"},"verdict":"proved"},"notes":["the division remainder is removed by row annihilators of the shifted parent"],"parent_interlacing_report":{"conclusion":{"first_index":0,"interlacing":"strict","interlacing_from":1,"root_region":{"upper":{"closed":false,"value":"0"}},"simple_roots":true,"statement":"every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0) (so its coefficients have one sign); for n >= 1, P_n has simple roots and P_(n-1) strictly interlaces P_n (no common root), and deg P_n = deg P_(n-1) + 1 for n >= 2"},"hypotheses":[{"evidence":"checked exactly","name":"seed_roots_negative","statement":"P_0 and P_1 are nonzero and real-rooted with every root < 0","status":{"kind":"verified"}},{"evidence":"degrees 0 and 1, leading coefficients of one sign","name":"seed_degree_step","statement":"deg P_1 = deg P_0 + 1, with leading coefficients of one sign","status":{"kind":"verified"}},{"evidence":"Bezout test, exact","name":"seed_strict_interlacing","statement":"P_0 strictly interlaces P_1 (simple real roots, no common root)","status":{"kind":"verified"}},{"evidence":"shared degree-law certificate, route recurrence (RealRooted RealRooted.LinRec.natDegree_eq_and_leadingCoeff_pos_of_ratio, RealRooted.ScalarRec.pos_of_ratio): the degree law deg P_n = 0 + 1 (n - 0) with positive leading coefficient for n >= 0 (route recurrence, induction from n = 2); every row is nonzero; lead P_n = 1 for every n >= 0; degree steps {1} from n = 1; the certificate is recomputed when the report is replayed","name":"degree_law","statement":"deg P_n = deg P_(n-1) + 1 with leading coefficients of one sign for every n >= 1","status":{"kind":"verified"}},{"evidence":"[x^0] c_1 and [x^0] c_2 are zero polynomials","name":"multipliers_vanish_at_zero","statement":"V_n(0) = 0 and W_n(0) = 0 for every n >= 2","status":{"kind":"verified"}},{"evidence":"A_n(0) = 1 > 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of A_n(0) = 1 at n = 2 + u have one sign)","name":"constant_term_positive","sign_decision":{"certificate":{"condition":"positive","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1"]},"numerator":["1"],"range":{"first":"2","last":null}},"decision":"holds"},"statement":"A_n(0) > 0 for every n >= 2","status":{"kind":"verified"}},{"evidence":"V_n = 0","name":"derivative_coefficient_nonpositive","statement":"V_n(x) <= 0 for every x < 0 and every n >= 2","status":{"kind":"verified"}},{"evidence":"W_n(x) = gamma(n) w(x) / f(n) with w(x) = -x^2 + x, which is negative on (-inf, 0) (no root there, exact): gamma(n)/f(n) = 1 >= 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of gamma(n)/f(n) = 1 at n = 2 + u have one sign)","name":"lag_coefficient_nonpositive","sign_decision":{"certificate":{"condition":"nonnegative","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1"]},"numerator":["1"],"range":{"first":"2","last":null}},"decision":"holds"},"statement":"W_n(x) <= 0 for every x < 0 and every n >= 2","status":{"kind":"verified"}},{"evidence":"W_n(x) = gamma(n) w(x) / f(n) with w(x) = -x^2 + x, which is negative on (-inf, 0) (no root there, exact): gamma(n)/f(n) = 1 > 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of gamma(n)/f(n) = 1 at n = 2 + u have one sign)","name":"derivative_or_lag_coefficient_negative","sign_decision":{"certificate":{"condition":"positive","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1"]},"numerator":["1"],"range":{"first":"2","last":null}},"decision":"holds"},"statement":"for every n >= 2 and x < 0, V_n(x) < 0 or W_n(x) < 0 (V_n < 0 on (-inf, 0) for every n, or W_n < 0 there for every n)","status":{"kind":"verified"}}],"lean_declarations":["RealRooted.threeTerm_interlaces_of_nonnegCoeffs","RealRooted.LiuWang.strictInterl_nonpos_lag_sequence"],"lean_replay":"not_attempted","lean_route":"sign","normal_form":"P_n = A_n(x) P_(n-1) + V_n(x) P'_(n-1) + W_n(x) P_(n-2) for n >= 2, with A_n(x) = (1) + (2) x, V_n(x) = 0, W_n(x) = (1) x + (-1) x^2","recurrence":{"first_index":0,"initial_polynomials":[["1"],["1","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","1","-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"reference":"L. L. Liu and Y. Wang, A unified approach to polynomial sequences with only real zeros, Adv. in Appl. Math. 38 (2007) 542-560, Theorem 2.1 with the interlacers f' and the lag row (strict form, as in the derivative-lag theorems of the RealRooted library, https://github.com/PerAlexandersson/RealRooted), with nonnegativity of the coefficients replaced by an exact induction keeping every root in (-inf, 0)","schema":"polytool.recurrence-real-rootedness-theorem.v1","status":"proved","theorem":"liu_wang_derivative_lag"},"parent_proof":{"attempts":[{"detail":"the rule is not P_(n+k) = c(x) P_n with c free of n","route":"periodic_product","success":false,"variant":"P_(n+k) = c(x) P_n"},{"detail":"not applicable: expected one nonzero lag term","route":"product_recurrence","success":false,"variant":"product_recurrence"},{"detail":"no theorem matched (weighted_renewal_window: support must satisfy offset = 1 + ell * t_degree; fixed_delay_predecessor_window: more than one weighted lag)","route":"paper_theorem","success":false,"variant":"match_recurrence_theorems"},{"detail":"not applicable: c_2(n, x) = gamma(n) w(x) with w neither constant nor a constant times a square (x + v_0)^2","route":"three_term_recurrence","success":false,"variant":"three_term_recurrence"},{"detail":"not applicable: the rule is not f(n) P_n = c_0(n, x) P_(n-1) + c_1(n, x) P'_(n-1)","route":"liu_wang","success":false,"variant":"liu_wang"},{"detail":"P_n = A_n(x) P_(n-1) + V_n(x) P'_(n-1) + W_n(x) P_(n-2) for n >= 2, with A_n(x) = (1) + (2) x, V_n(x) = 0, W_n(x) = (1) x + (-1) x^2: every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0) (so its coefficients have one sign); for n >= 1, P_n has simple roots and P_(n-1) strictly interlaces P_n (no common root), and deg P_n = deg P_(n-1) + 1 for n >= 2","route":"liu_wang_derivative_lag","success":true,"variant":"liu_wang_derivative_lag"}],"conditional_on":[],"interlacing":{"from_index":1,"justification":{"premises":["every hypothesis of the theorem is verified exactly for every index: P_n = A_n(x) P_(n-1) + V_n(x) P'_(n-1) + W_n(x) P_(n-2) for n >= 2, with A_n(x) = (1) + (2) x, V_n(x) = 0, W_n(x) = (1) x + (-1) x^2","every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0) (so its coefficients have one sign); for n >= 1, P_n has simple roots and P_(n-1) strictly interlaces P_n (no common root), and deg P_n = deg P_(n-1) + 1 for n >= 2"],"theorem":"liu_wang_derivative_lag: L. L. Liu and Y. Wang, A unified approach to polynomial sequences with only real zeros, Adv. in Appl. Math. 38 (2007) 542-560, Theorem 2.1 with the interlacers f' and the lag row (strict form, as in the derivative-lag theorems of the RealRooted library, https://github.com/PerAlexandersson/RealRooted), with nonnegativity of the coefficients replaced by an exact induction keeping every root in (-inf, 0)"},"kind":"strict","orientation":"previous_interlaces_next"},"route":"liu_wang_derivative_lag","rows_checked":10,"statement":"every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign","status":"proved"},"rows_compared":16,"schema":"polytool.recurrence-preserver-image.v1","statement":"proved: Q_n = lambda(n) T_n(P_(n+0)) with T = f(n, theta) = 1 + (2) theta + (1) theta^2 for every n >= 0, the side conditions hold for every n, and every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign; so every Q_n, n >= 0, is zero or real-rooted with roots in (-inf, 0]"},"kind":"preserver_image"}