{"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":1,"initial_polynomials":[["1"],["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["0","1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"reversal of Triangle T(n,k), 0 <= k <= n, read by rows, given by [0, 2, -1, 0, 0, 0, 0, 0, ...] DELTA [1, 0, 0, 0, 0, 0, 0, 0, ...] where DELTA is the operator defined in A084938."},"identifying_rows":2,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["0","-4","-33","-83","-15","-1"],["0","-4","-56","-148","-30","-2"],["0","-1","-32","-100","-14","-1"],["0","0","-6","-32","-2","0"],["0","0","0","-4","0","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","0","-12","-99","-249","-45","-3"],["0","0","-12","-168","-444","-90","-6"],["0","0","-3","-96","-300","-42","-3"],["0","0","0","-18","-96","-6","0"],["0","0","0","0","-12","0","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0","0","-4","-33","-83","-15","-1"],["0","0","0","-4","-56","-148","-30","-2"],["0","0","0","-1","-32","-100","-14","-1"],["0","0","0","0","-6","-32","-2","0"],["0","0","0","0","0","-4","0","0"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["-1","-7","-40","-80","-15","-1"],["-2","-22","-76","-124","-30","-2"],["-1","-21","-70","-78","-13","-1"],["0","-6","-30","-26","-2","0"],["0","0","-4","-4","0","0"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-3","-21","-120","-240","-45","-3"],["0","-6","-66","-228","-372","-90","-6"],["0","-3","-63","-210","-234","-39","-3"],["0","0","-18","-90","-78","-6","0"],["0","0","0","-12","-12","0","0"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["0","0","-1","-7","-40","-80","-15","-1"],["0","0","-2","-22","-76","-124","-30","-2"],["0","0","-1","-21","-70","-78","-13","-1"],["0","0","0","-6","-30","-26","-2","0"],["0","0","0","0","-4","-4","0","0"]]},"deriv_order":2,"shift":1},{"coeff":{"coeffs":[["1","3","7","-3","0"],["2","10","28","8","0"],["1","14","28","8","1"],["0","6","16","2","0"],["0","0","4","0","0"]]},"deriv_order":0,"shift":2},{"coeff":{"coeffs":[["0","3","9","21","-9","0"],["0","6","30","84","24","0"],["0","3","42","84","24","3"],["0","0","18","48","6","0"],["0","0","0","12","0","0"]]},"deriv_order":1,"shift":2},{"coeff":{"coeffs":[["0","0","1","3","7","-3","0"],["0","0","2","10","28","8","0"],["0","0","1","14","28","8","1"],["0","0","0","6","16","2","0"],["0","0","0","0","4","0","0"]]},"deriv_order":2,"shift":2}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[1,2],"index_shift":0,"input":{"first_index":1,"initial_polynomials":[["1"],["1"]],"recurrence":{"denominator":{"coeffs":[["1","-9","-1","-3","4"],["-2","26","-20","0","-4"],["1","-22","28","-4","1"],["0","6","-16","2","0"],["0","0","4","0","0"]]},"terms":[{"coeff":{"coeffs":[["0","0","1","-5","-5","1"],["0","0","0","4","-2","-2"],["0","1","-4","4","2","1"],["0","0","6","0","2","0"],["0","0","0","4","0","0"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["1","-1","-8","0","-9","1"],["-2","10","28","-4","2","-2"],["1","-15","-14","18","1","1"],["0","6","-2","-6","2","0"],["0","0","4","4","0","0"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":1,"multiplier":["1"],"operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["2"]},{"denominator":["1"],"numerator":["1"]}],"shape":"euler_polynomial"},"parent":{"first_index":1,"initial_polynomials":[["1"],["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["0","1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_leader_shift":2,"parent_valid_from_base":1,"quotients":[{"differentiations":[{"coeff":{"coeffs":[["0","0","0","0","0","0","-64","-1344","-11008","-45312","-101760","-114048","-4864","13056","3008","192","0"],["0","0","0","0","0","-96","-2048","-17440","-78976","-220736","-402048","-417984","-312704","-104800","-15232","-800","0"],["0","0","0","0","-48","-1104","-10576","-57392","-204448","-486560","-647200","-315360","2576","17392","-400","-752","-64"],["0","0","0","-8","-240","-3008","-21328","-97512","-288896","-453568","-162720","87208","90896","47232","13552","1864","96"],["0","0","0","-16","-368","-3824","-24096","-93472","-183632","-90336","85312","145840","46320","-6448","-5408","-896","-48"],["0","0","0","-8","-232","-2672","-15296","-43288","-43624","39392","88768","4552","-21176","-6256","-256","88","8"],["0","0","0","0","-48","-848","-5008","-9648","3872","17632","15840","-15200","-6640","-144","176","16","0"],["0","0","0","0","0","-32","-480","-1920","896","10560","-10560","-896","1920","480","32","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","-192","-4032","-33024","-135936","-305280","-342144","-14592","39168","9024","576","0"],["0","0","0","0","0","0","-288","-6144","-52320","-236928","-662208","-1206144","-1253952","-938112","-314400","-45696","-2400","0"],["0","0","0","0","0","-144","-3312","-31728","-172176","-613344","-1459680","-1941600","-946080","7728","52176","-1200","-2256","-192"],["0","0","0","0","-24","-720","-9024","-63984","-292536","-866688","-1360704","-488160","261624","272688","141696","40656","5592","288"],["0","0","0","0","-48","-1104","-11472","-72288","-280416","-550896","-271008","255936","437520","138960","-19344","-16224","-2688","-144"],["0","0","0","0","-24","-696","-8016","-45888","-129864","-130872","118176","266304","13656","-63528","-18768","-768","264","24"],["0","0","0","0","0","-144","-2544","-15024","-28944","11616","52896","47520","-45600","-19920","-432","528","48","0"],["0","0","0","0","0","0","-96","-1440","-5760","2688","31680","-31680","-2688","5760","1440","96","0","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","-64","-1344","-11008","-45312","-101760","-114048","-4864","13056","3008","192","0"],["0","0","0","0","0","0","0","-96","-2048","-17440","-78976","-220736","-402048","-417984","-312704","-104800","-15232","-800","0"],["0","0","0","0","0","0","-48","-1104","-10576","-57392","-204448","-486560","-647200","-315360","2576","17392","-400","-752","-64"],["0","0","0","0","0","-8","-240","-3008","-21328","-97512","-288896","-453568","-162720","87208","90896","47232","13552","1864","96"],["0","0","0","0","0","-16","-368","-3824","-24096","-93472","-183632","-90336","85312","145840","46320","-6448","-5408","-896","-48"],["0","0","0","0","0","-8","-232","-2672","-15296","-43288","-43624","39392","88768","4552","-21176","-6256","-256","88","8"],["0","0","0","0","0","0","-48","-848","-5008","-9648","3872","17632","15840","-15200","-6640","-144","176","16","0"],["0","0","0","0","0","0","0","-32","-480","-1920","896","10560","-10560","-896","1920","480","32","0","0"]]},"deriv_order":2}],"shift":0}],"row_annihilation":{"kind":"system","system":{"generators":[{"annihilator":{"terms":[{"coeff":{"coeffs":[["2","0"],["-6","2"],["2","-2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["1","15","-5","-3"],["-1","-5","5","1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","1","5","-5","-1"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["2"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","672","13856","107136","380288","614592","428736","136320","20864","1440","32"],["0","0","0","0","0","0","0","1136","22336","158864","472640","443296","-221760","-428704","-161600","-23056","-1024","16"],["0","0","0","0","0","0","696","13128","85928","202104","-36112","-630384","-610032","-193872","-56104","-17496","-2872","-168"],["0","0","0","0","0","180","3352","20688","32792","-123084","-473232","-490816","-111824","102108","90488","27888","3768","188"],["0","0","0","0","16","344","2272","312","-54096","-204832","-239424","-19728","230128","101016","-2976","-8104","-1456","-80"],["0","0","0","0","12","124","-528","-11096","-48004","-74412","-4096","140080","33540","-25436","-9712","-600","116","12"],["0","0","0","0","0","-40","-760","-5112","-13448","-5648","26448","35216","-23824","-12360","-728","232","24","0"],["0","0","0","0","0","0","-48","-720","-2880","1344","15840","-15840","-1344","2880","720","48","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","224","6720","80096","480000","1497024","2242944","1303232","363264","52064","3648","96"],["0","0","0","0","0","0","0","336","10576","128048","753008","2190496","2737056","797664","-191648","-118000","-15856","-272","48"],["0","0","0","0","0","0","168","5952","76400","458656","1321880","1594624","374048","-726336","-590632","-229184","-51088","-5984","-280"],["0","0","0","0","0","28","1380","20584","136712","439668","641884","167792","-902928","-640700","-11812","106152","36232","4780","228"],["0","0","0","0","0","104","2320","20200","85272","164864","28216","-402096","-357776","179944","140928","13640","-5384","-1232","-72"],["0","0","0","0","0","64","1184","7768","20248","7496","-70552","-150160","109552","84688","-2192","-7240","-904","40","8"],["0","0","0","0","0","0","48","688","2192","-6576","-30496","17632","50208","-18272","-13840","-1680","80","16","0"],["0","0","0","0","0","0","0","-32","-480","-1920","896","10560","-10560","-896","1920","480","32","0","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","96","2688","30368","175104","532928","785664","436032","116736","16352","1152","32"],["0","0","0","0","0","0","0","0","144","4208","48496","277328","803744","1046368","405216","40352","-4400","-208","176","16"],["0","0","0","0","0","0","0","72","2352","28992","172016","508776","693728","340416","-136992","-197736","-82192","-16896","-1744","-72"],["0","0","0","0","0","0","12","540","7864","52680","179060","310260","207120","-246736","-242636","-34236","19640","7560","972","44"],["0","0","0","0","0","0","40","896","8008","36456","86112","70616","-103920","-147696","11368","31536","6696","8","-112","-8"],["0","0","0","0","0","0","24","472","3480","11848","16928","-8976","-63184","6928","26712","6328","-328","-216","-16","0"],["0","0","0","0","0","0","0","32","512","2400","1024","-11456","0","11456","-1024","-2400","-512","-32","0","0"]]},"deriv_order":2}],"step_multiplier":{"coeffs":[["0","0","0","0","0","0","-64","-1152","-7104","-16128","-7104","-1152","-64"],["0","0","0","0","0","-96","-1632","-8928","-13536","13536","8928","1632","96"],["0","0","0","0","-48","-768","-3648","-2304","13536","-2304","-3648","-768","-48"],["0","0","0","-8","-120","-480","224","2640","-2640","-224","480","120","8"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","0","0","0","0","-64","-1152","-7104","-16128","-7104","-1152","-64"],["0","0","0","0","0","0","-32","-416","-672","9696","36768","17184","2848","160"],["0","0","0","0","0","48","896","5824","14208","4512","-15744","-8256","-1408","-80"],["0","0","0","0","40","600","2400","-1120","-13200","13200","1120","-2400","-600","-40"],["0","0","0","8","80","-120","-2624","-1520","15840","-12976","-1600","2280","592","40"],["0","0","0","-8","-112","-360","704","2416","-5280","2416","704","-360","-112","-8"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","-320","-5760","-35456","-79488","-28416","10368","6784","1152","64"],["0","0","0","0","0","0","-448","-7424","-38272","-43136","102144","32640","-28288","-14720","-2368","-128"],["0","0","0","0","0","-192","-2784","-9888","14208","75264","-85824","-27840","23424","11712","1824","96"],["0","0","0","0","-16","-96","1232","9568","3168","-53696","36512","15552","-7504","-4064","-624","-32"],["0","0","0","4","80","520","784","-3140","-4960","13424","-4960","-3140","784","520","80","4"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","-32","-736","-6272","-22912","-25536","25536","22912","6272","736","32"],["0","0","0","0","0","0","-48","-1056","-8304","-24960","-3936","76608","-3936","-24960","-8304","-1056","-48"],["0","0","0","0","0","-24","-504","-3624","-8328","10512","40272","-40272","-10512","8328","3624","504","24"],["0","0","0","0","-4","-80","-520","-784","3140","4960","-13424","4960","3140","-784","-520","-80","-4"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","0","0","16","256","1216","768","-4512","768","1216","256","16"],["0","0","0","0","8","88","-32","-2656","-4176","11664","-1312","-2912","-632","-40"],["0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","8","96","120","-1664","-1968","10560","-7696","-1152","1320","352","24"],["0","0","0","-8","-112","-360","704","2416","-5280","2416","704","-360","-112","-8"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","16","208","416","-3392","-9248","12768","7936","-4928","-3184","-560","-32"],["0","0","0","0","8","32","-824","-5200","1808","36096","-31024","-15712","8680","5216","872","48"],["0","0","0","0","-24","-264","24","6792","6672","-40272","23088","12048","-4728","-2856","-456","-24"],["0","0","0","4","80","520","784","-3140","-4960","13424","-4960","-3140","784","520","80","4"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","-16","-352","-2768","-8320","-1312","25536","-1312","-8320","-2768","-352","-16"],["0","0","0","0","0","-16","-336","-2416","-5552","7008","26848","-26848","-7008","5552","2416","336","16"],["0","0","0","0","-4","-80","-520","-784","3140","4960","-13424","4960","3140","-784","-520","-80","-4"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0"],["-4","4"],["6","-6"],["-2","2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","0","-18","-6"],["-1","-13","17","5"],["1","5","-5","-1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0","-2","-12","-2"],["0","-1","-5","5","1"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","0","0","0","192","3376","19184","26688","-83008","-227040","-188256","-64448","-10240","-720","-16"],["0","0","0","0","0","0","280","4848","26664","32016","-122544","-244672","-47312","100992","46488","6480","168","-16"],["0","0","0","0","0","124","2128","11128","6256","-90956","-153216","83312","241216","134404","47536","11416","1488","76"],["0","0","0","0","16","304","1664","-1400","-38048","-86872","36768","204080","155120","18784","-19232","-7864","-1120","-56"],["0","0","0","0","12","124","-448","-9272","-32404","-15276","76832","115312","-23836","-37724","-8032","72","164","12"],["0","0","0","0","0","-40","-760","-4952","-10824","7600","40080","-880","-25168","-6152","744","328","24","0"],["0","0","0","0","0","0","-48","-720","-2880","1344","15840","-15840","-1344","2880","720","48","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","64","1904","21504","112400","242048","-19872","-687872","-528352","-163776","-24784","-1792","-48"],["0","0","0","0","0","0","88","2744","31608","164552","341504","-55760","-925712","-674416","-168360","-22120","-4072","-728","-48"],["0","0","0","0","0","28","1092","14232","81224","193716","61932","-430512","-702352","-124860","139100","86808","21576","2540","116"],["0","0","0","0","0","104","2144","16664","58696","73696","-103320","-390416","-79728","213992","87664","-3080","-6360","-1072","-56"],["0","0","0","0","0","64","1184","7608","17624","-5528","-80408","-93776","139504","42384","-19984","-8168","-584","72","8"],["0","0","0","0","0","0","48","688","2256","-5552","-25632","20704","32160","-15200","-8976","-656","144","16","0"],["0","0","0","0","0","0","0","-32","-480","-1920","896","10560","-10560","-896","1920","480","32","0","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","48","1296","13840","72368","178912","126368","-174816","-159648","-50192","-7600","-560","-16"],["0","0","0","0","0","0","0","48","1408","15872","85152","209936","147584","-169984","-190016","-77104","-19200","-3328","-352","-16"],["0","0","0","0","0","0","12","460","6088","36872","105988","123652","-17872","-228688","-86828","28820","24712","6088","668","28"],["0","0","0","0","0","0","40","848","7016","28632","56768","19192","-121520","-68880","46376","28992","3272","-584","-144","-8"],["0","0","0","0","0","0","24","472","3416","10760","11040","-16912","-48208","21904","18776","440","-1416","-280","-16","0"],["0","0","0","0","0","0","0","32","512","2400","1024","-11456","0","11456","-1024","-2400","-512","-32","0","0"]]},"deriv_order":2}],"step_multiplier":{"coeffs":[["0","0","0","0","0","0","-64","-1152","-7104","-16128","-7104","-1152","-64"],["0","0","0","0","0","-96","-1632","-8928","-13536","13536","8928","1632","96"],["0","0","0","0","-48","-768","-3648","-2304","13536","-2304","-3648","-768","-48"],["0","0","0","-8","-120","-480","224","2640","-2640","-224","480","120","8"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","-64","-1088","-5952","-9024","9024","5952","1088","64"],["0","0","0","0","0","-96","-1536","-7296","-4608","27072","-4608","-7296","-1536","-96"],["0","0","0","0","-48","-720","-2816","2432","21792","-6816","-10368","-3072","-368","-16"],["0","0","0","-8","-112","-264","2240","9712","-672","-24656","5312","6936","1424","88"],["0","0","0","0","48","720","2880","-1344","-15840","15840","1344","-2880","-720","-48"],["0","0","0","8","112","360","-704","-2416","5280","-2416","-704","360","112","8"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","256","4800","31936","86976","83904","42048","10816","1344","64"],["0","0","0","0","0","0","352","6336","38656","81024","-10560","-119808","-94208","-28800","-3872","-192"],["0","0","0","0","0","144","2512","13856","15424","-73120","-131232","48000","88384","31376","4432","224"],["0","0","0","0","8","144","392","-6080","-39408","-36512","128336","14784","-41752","-17264","-2520","-128"],["0","0","0","-4","-72","-592","-3224","-9204","5296","53696","-44976","-15916","9496","4752","712","36"],["0","0","0","-4","-80","-520","-784","3140","4960","-13424","4960","3140","-784","-520","-80","-4"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","32","800","7808","36992","85440","85440","36992","7808","800","32"],["0","0","0","0","0","0","48","1184","11248","50048","95584","25536","-98208","-66688","-16784","-1888","-80"],["0","0","0","0","0","24","600","5736","24936","39408","-32400","-112944","18384","41592","12984","1608","72"],["0","0","0","0","4","112","1192","5616","7964","-18976","-40272","48736","10876","-10320","-4312","-592","-28"],["0","0","0","0","4","80","520","784","-3140","-4960","13424","-4960","-3140","784","520","80","4"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","0","0","-16","-320","-2368","-7872","-11616","-7872","-2368","-320","-16"],["0","0","0","0","-8","-152","-896","-448","12336","34128","16960","3328","280","8"],["0","0","0","0","-16","-128","960","11136","22560","-18816","-13120","-2432","-144","0"],["0","0","0","-8","-88","64","3168","6608","-10128","-7712","4448","3064","552","32"],["0","0","0","0","32","480","1920","-896","-10560","10560","896","-1920","-480","-32"],["0","0","0","8","112","360","-704","-2416","5280","-2416","-704","360","112","8"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","-16","-272","-1632","-4928","-15200","-44256","-39424","-19520","-5136","-656","-32"],["0","0","0","0","-8","-96","-200","80","-9360","-44032","-20048","28896","32152","10976","1560","80"],["0","0","0","0","8","104","-8","-5224","-22192","-9456","61424","7472","-21464","-9208","-1384","-72"],["0","0","0","-4","-64","-424","-2016","-6428","1792","40272","-31552","-12412","6720","3544","544","28"],["0","0","0","-4","-80","-520","-784","3140","4960","-13424","4960","3140","-784","-520","-80","-4"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","16","384","3504","14592","24224","0","-24224","-14592","-3504","-384","-16"],["0","0","0","0","0","16","384","3472","13856","17952","-22912","-49760","10944","19408","5888","720","32"],["0","0","0","0","4","104","1024","4408","5188","-15472","-26848","35312","7372","-7544","-3104","-424","-20"],["0","0","0","0","4","80","520","784","-3140","-4960","13424","-4960","-3140","784","520","80","4"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["0","0","0","0","0","0","-64","-1152","-7104","-16128","-7104","-1152","-64"],["0","0","0","0","0","-96","-1632","-8928","-13536","13536","8928","1632","96"],["0","0","0","0","-48","-768","-3648","-2304","13536","-2304","-3648","-768","-48"],["0","0","0","-8","-120","-480","224","2640","-2640","-224","480","120","8"]]},"start_base":1}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["0","-1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-1","-1"]]},"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 1) 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 >= 1 (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 >= 1"},"method":"operator_division"},"status":"certified"},"input_first_index":1,"interlacing":{"from_index":3,"justification":"the parent theorem (LiuWangDerivativeLag) proves P_(m-1) strictly interlacing P_m for every m >= 3; 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 >= 3","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 [1, +inf) (exact; Taylor shift: the coefficients of delta(n) at n = 1 + 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":"1","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":1,"input_interlacing":{"interlacing":{"from_index":3,"justification":{"premises":["the parent theorem (LiuWangDerivativeLag) proves P_(m-1) strictly interlacing P_m for every m >= 3; 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 >= 3"],"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":1,"initial_polynomials":[["1"],["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["0","1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":1,"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 >= 1"},"parent_proof":{"route":"liu_wang_derivative_lag","statement":"every parent row P_n, n >= 1, is zero or real-rooted with coefficients of one sign","status":"proved"},"root_transfer":{"input_conclusion":"every Q_n, n >= 1, 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":1,"interlacing":"strict","interlacing_from":3,"root_region":{"upper":{"closed":false,"value":"0"}},"simple_roots":true,"statement":"every P_n, n >= 1, is nonzero and real-rooted with every root in (-inf, 0) (so its coefficients have one sign); for n >= 3, 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 >= 4; the rule is applied from n = 4 on in the induction (start moved 1 row(s) past the supplied seeds; P_1, ..., P_3 enter as seed rows, checked exactly)"},"hypotheses":[{"evidence":"checked exactly","name":"seed_roots_negative","statement":"P_2 and P_3 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_3 = deg P_2 + 1, with leading coefficients of one sign","status":{"kind":"verified"}},{"evidence":"Bezout test, exact","name":"seed_strict_interlacing","statement":"P_2 strictly interlaces P_3 (simple real roots, no common root)","status":{"kind":"verified"}},{"evidence":"checked exactly for P_1, ..., P_1","name":"earlier_seeds","statement":"the seed rows P_1, ..., P_1 are each zero or real-rooted with every root in (-inf, 0)","status":{"kind":"verified"}},{"evidence":"lambda_n = 1 > 0 for every integer n in [4, +inf) (exact; Taylor shift: the coefficients of lambda_n = 1 at n = 4 + u have one sign)","name":"degree_step_positive","sign_decision":{"certificate":{"condition":"positive","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1"]},"numerator":["1"],"range":{"first":"4","last":null}},"decision":"holds"},"statement":"lambda_n = [x^1] A_n + (deg P_(n-1)) [x^2] V_n > 0 for every n >= 4 (deg P_n = deg P_(n-1) + 1 with leading coefficients of one sign)","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 >= 4","status":{"kind":"verified"}},{"evidence":"A_n(0) = 1 > 0 for every integer n in [4, +inf) (exact; Taylor shift: the coefficients of A_n(0) = 1 at n = 4 + 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":"4","last":null}},"decision":"holds"},"statement":"A_n(0) > 0 for every n >= 4","status":{"kind":"verified"}},{"evidence":"V_n = 0","name":"derivative_coefficient_nonpositive","statement":"V_n(x) <= 0 for every x < 0 and every n >= 4","status":{"kind":"verified"}},{"evidence":"W_n(x) = gamma(n) w(x) / f(n) with w(x) = x, which is negative on (-inf, 0) (no root there, exact): gamma(n)/f(n) = 1 >= 0 for every integer n in [4, +inf) (exact; Taylor shift: the coefficients of gamma(n)/f(n) = 1 at n = 4 + 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":"4","last":null}},"decision":"holds"},"statement":"W_n(x) <= 0 for every x < 0 and every n >= 4","status":{"kind":"verified"}},{"evidence":"W_n(x) = gamma(n) w(x) / f(n) with w(x) = x, which is negative on (-inf, 0) (no root there, exact): gamma(n)/f(n) = 1 > 0 for every integer n in [4, +inf) (exact; Taylor shift: the coefficients of gamma(n)/f(n) = 1 at n = 4 + 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":"4","last":null}},"decision":"holds"},"statement":"for every n >= 4 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 >= 4, with A_n(x) = (1) + (1) x, V_n(x) = 0, W_n(x) = (1) x","recurrence":{"first_index":1,"initial_polynomials":[["1"],["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["0","1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":1,"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","start_delay":1,"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":"induction start moved 1 row(s) past the seeds: P_n = A_n(x) P_(n-1) + V_n(x) P'_(n-1) + W_n(x) P_(n-2) for n >= 4, with A_n(x) = (1) + (1) x, V_n(x) = 0, W_n(x) = (1) x: every P_n, n >= 1, is nonzero and real-rooted with every root in (-inf, 0) (so its coefficients have one sign); for n >= 3, 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 >= 4; the rule is applied from n = 4 on in the induction (start moved 1 row(s) past the supplied seeds; P_1, ..., P_3 enter as seed rows, checked exactly)","route":"liu_wang_derivative_lag","success":true,"variant":"liu_wang_derivative_lag"}],"conditional_on":[],"interlacing":{"from_index":3,"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 >= 4, with A_n(x) = (1) + (1) x, V_n(x) = 0, W_n(x) = (1) x","every P_n, n >= 1, is nonzero and real-rooted with every root in (-inf, 0) (so its coefficients have one sign); for n >= 3, 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 >= 4; the rule is applied from n = 4 on in the induction (start moved 1 row(s) past the supplied seeds; P_1, ..., P_3 enter as seed rows, checked exactly)"],"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 >= 1, 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 >= 1, the side conditions hold for every n, and every parent row P_n, n >= 1, is zero or real-rooted with coefficients of one sign; so every Q_n, n >= 1, is zero or real-rooted with roots in (-inf, 0]"},"kind":"preserver_image"}