{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"euler_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["1","3","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","4","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","0","-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"Irregular triangle read by rows formed by taking every other row of the Delannoy array (A008288) regarded as a triangle."},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["2","12","-4","-60","-30"],["6","68","134","-44","-44"],["4","72","228","48","-16"],["0","16","80","32","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","-2","-42","-218","-270","-60"],["0","2","-4","-202","-356","-88"],["0","4","56","116","-64","-32"],["0","0","16","80","32","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0","-2","-27","-107","-105","-15"],["0","0","-2","-36","-168","-156","-22"],["0","0","0","-8","-56","-56","-8"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["-2","0","10"],["-6","-8","38"],["-4","-24","44"],["0","-16","16"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-2","0","10"],["0","-6","-8","38"],["0","-4","-24","44"],["0","0","-16","16"]]},"deriv_order":1,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"denominator":{"coeffs":[["0","0","0"],["2","-8","-2"],["-4","24","-4"],["0","-16","16"]]},"terms":[{"coeff":{"coeffs":[["0","0","-10","0","2"],["2","28","82","44","12"],["-4","-24","12","48","16"],["0","-16","-80","-32","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","0","-1","-5","5","1"],["0","2","20","56","44","6"],["0","0","8","56","56","8"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["1/4","1","1"],"operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"euler_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["1","3","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","4","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","0","-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_leader_shift":2,"parent_valid_from_base":0,"quotients":[],"row_annihilation":{"kind":"system","system":{"generators":[{"annihilator":{"terms":[{"coeff":{"coeffs":[["-1","-3","-1"],["2","8","0"],["-16","0","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","-19","-12","-1"],["4","24","4","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-2","-12","-2"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["1"],["2"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","-2","-20","-20","204","120","-540","148","100","10"],["0","0","-10","-108","-172","980","1136","-3236","780","572","58"],["0","0","-16","-200","-520","1432","3640","-7000","1384","1160","120"],["0","0","-8","-144","-656","496","4768","-6448","912","976","104"],["0","0","0","-32","-288","-160","2144","-2144","160","288","32"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-2","-20","-20","204","120","-540","148","100","10"],["0","0","0","-10","-108","-172","980","1136","-3236","780","572","58"],["0","0","0","-16","-200","-520","1432","3640","-7000","1384","1160","120"],["0","0","0","-8","-144","-656","496","4768","-6448","912","976","104"],["0","0","0","0","-32","-288","-160","2144","-2144","160","288","32"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["0","0","0","-1","-15","-60","28","330","-330","-28","60","15","1"],["0","0","0","-6","-90","-360","168","1980","-1980","-168","360","90","6"],["0","0","0","-12","-180","-720","336","3960","-3960","-336","720","180","12"],["0","0","0","-8","-120","-480","224","2640","-2640","-224","480","120","8"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","12","163","463","-1386","-3604","9626","-4614","-1856","784","363","47","2"],["0","0","0","76","1056","3290","-7318","-23328","53080","-22292","-10212","3620","1784","234","10"],["0","0","0","176","2508","8564","-13088","-55344","102088","-33352","-19536","4832","2764","372","16"],["0","0","0","176","2576","9592","-8888","-56768","79424","-13552","-14992","976","1264","184","8"],["0","0","0","64","960","3840","-1792","-21120","21120","1792","-3840","-960","-64","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-4","-65","-307","-67","1955","166","-4430","2410","914","-373","-175","-23","-1"],["0","0","0","-20","-344","-1832","-1656","9572","7376","-24432","7888","5044","-888","-616","-88","-4"],["0","0","0","-32","-596","-3644","-5820","14828","27512","-44568","2632","9208","924","-364","-76","-4"],["0","0","0","-16","-336","-2416","-5552","7008","26848","-26848","-7008","5552","2416","336","16","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","2","42","302","694","-876","-3356","3356","876","-694","-302","-42","-2"],["0","0","0","0","8","168","1208","2776","-3504","-13424","13424","3504","-2776","-1208","-168","-8"],["0","0","0","0","8","168","1208","2776","-3504","-13424","13424","3504","-2776","-1208","-168","-8"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","-20","-277","-822","2483","8720","-11194","-68","1454","-108","-145","-22","-1"],["0","0","0","-132","-1876","-6180","12908","55896","-60616","-6792","7064","300","-484","-84","-4"],["0","0","0","-320","-4692","-17288","20300","127968","-109672","-28784","10296","2464","-196","-72","-4"],["0","0","0","-336","-5120","-21296","5760","120160","-69504","-35808","2944","2800","384","16","0"],["0","0","0","-128","-2048","-9728","-6144","36096","-6144","-9728","-2048","-128","0","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","8","132","616","-244","-6928","-6712","11888","3384","-1400","-652","-88","-4"],["0","0","0","40","704","3848","3184","-27056","-39616","48208","17696","-4216","-2432","-344","-16"],["0","0","0","64","1232","8000","15664","-25088","-77920","50176","30176","-64","-1904","-320","-16"],["0","0","0","32","704","5536","16640","2624","-51072","2624","16640","5536","704","32","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","-4","-88","-692","-2080","-328","6384","-328","-2080","-692","-88","-4"],["0","0","0","0","-16","-352","-2768","-8320","-1312","25536","-1312","-8320","-2768","-352","-16"],["0","0","0","0","-16","-352","-2768","-8320","-1312","25536","-1312","-8320","-2768","-352","-16"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["2","8","-2"],["-8","8","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","-10","0","2"],["2","10","-10","-2"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-1","-5","5","1"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","0","4","48","143","-50","-223","212","-79","-50","-5"],["0","0","20","256","892","176","-1516","832","-396","-240","-24"],["0","0","32","464","2028","1720","-3804","608","-652","-360","-36"],["0","0","16","320","1984","3168","-4160","-768","-384","-160","-16"],["0","0","0","64","704","1664","-1664","-704","-64","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","4","44","84","-324","-564","516","220","20"],["0","0","0","20","236","580","-1380","-3652","2820","1260","116"],["0","0","0","32","432","1472","-1392","-8672","5328","2560","240"],["0","0","0","16","304","1616","624","-8912","3984","2160","208"],["0","0","0","0","64","640","960","-3328","960","640","64"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["0","0","0","-1","-15","-60","28","330","-330","-28","60","15","1"],["0","0","0","-6","-90","-360","168","1980","-1980","-168","360","90","6"],["0","0","0","-12","-180","-720","336","3960","-3960","-336","720","180","12"],["0","0","0","-8","-120","-480","224","2640","-2640","-224","480","120","8"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","6","74","122","-1098","-1412","7204","-5772","-148","926","114","-14","-2"],["0","0","0","38","482","970","-6194","-9476","41300","-31276","-1444","4990","682","-62","-10"],["0","0","0","88","1152","2776","-12304","-23376","84032","-58256","-4704","9208","1472","-72","-16"],["0","0","0","88","1192","3368","-10024","-24976","71056","-42416","-6224","6584","1352","8","-8"],["0","0","0","32","448","1440","-2816","-9664","21120","-9664","-2816","1440","448","32","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-2","-30","-110","206","1260","-940","-3356","3420","310","-598","-150","-10","0"],["0","0","0","-10","-160","-700","432","6610","-1280","-20136","16160","2810","-2784","-860","-80","-2"],["0","0","0","-16","-280","-1480","-744","11320","6160","-40272","23600","7520","-3960","-1640","-200","-8"],["0","0","0","-8","-160","-1040","-1568","6280","9920","-26848","9920","6280","-1568","-1040","-160","-8"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","1","20","130","196","-785","-1240","3356","-1240","-785","196","130","20","1"],["0","0","0","0","4","80","520","784","-3140","-4960","13424","-4960","-3140","784","520","80","4"],["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","-10","-126","-225","1961","3784","-10424","3458","1710","-102","-34","7","1"],["0","0","0","-66","-858","-1888","11244","25140","-60620","15960","10944","254","-138","24","4"],["0","0","0","-160","-2160","-5812","21892","60432","-122672","21896","24216","2480","-128","12","4"],["0","0","0","-168","-2376","-7792","15392","61136","-96816","6720","20256","3608","56","-16","0"],["0","0","0","-64","-960","-3840","1792","21120","-21120","-1792","3840","960","64","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","4","61","219","-625","-4035","-494","10814","-2738","-2994","-319","87","19","1"],["0","0","0","20","328","1480","-1112","-17892","-8688","49968","-9200","-13364","-1880","264","72","4"],["0","0","0","32","580","3292","3052","-23148","-28824","70104","-3944","-17528","-3692","12","60","4"],["0","0","0","16","336","2416","5552","-7008","-26848","26848","7008","-5552","-2416","-336","-16","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","-2","-42","-302","-694","876","3356","-3356","-876","694","302","42","2"],["0","0","0","0","-8","-168","-1208","-2776","3504","13424","-13424","-3504","2776","1208","168","8"],["0","0","0","0","-8","-168","-1208","-2776","3504","13424","-13424","-3504","2776","1208","168","8"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["0","0","4","40","60","-208","60","40","4"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["0","0","1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-1","-4","-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 0) and E the input rule gauged by lambda(n)/delta(n) and composed with (or conjugated through) T = f(n, theta) = 1 + (1) theta; so the candidate rows satisfy the input rule at every base n >= 0 (the exceptional bases checked exactly), and agreement on the 1 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":{"reason":"no parent theorem report with an interlacing conclusion","status":"none"},"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, 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":{"reason":"no parent theorem report with an interlacing conclusion","status":"not_proved"},"lean_replay":"not_attempted","operation":{"description":"f(n, theta) = 1 + (1) theta","kind":"preserver_image","operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"euler_polynomial"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["1","3","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","4","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","0","-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 + (1) theta, for every n >= 0"},"parent_proof":{"statement":"open: no route proved that every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign; the first 10 parent rows pass the exact check (evidence only)","status":"open"},"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":"open"},"notes":["the division remainder is removed by row annihilators of the shifted parent"],"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: only P_(n-1) and one term w(n) t P_(n-L) are supported)","route":"paper_theorem","success":false,"variant":"match_recurrence_theorems"},{"detail":"not applicable: c_1(n, x) has degree > 1 in x","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":"not applicable: deg_x c_0 > 1, deg_x c_1 > 2 or deg_x c_2 > 2: the degree may grow by more than one","route":"liu_wang_derivative_lag","success":false,"variant":"liu_wang_derivative_lag"},{"detail":"not applicable: the rule is not f(n) P_n = c_0(n, x) P_(n-1) + gamma(n) (x - L)(x - U) P'_(n-1)","route":"ma_wang_interval","success":false,"variant":"ma_wang_interval"},{"detail":"not applicable: deg_x c_1 > 1, deg_x c_d > 2 or deg_x c_2 > 2: the degree may grow by more than one","route":"liu_wang_three_term","success":false,"variant":"liu_wang_three_term"},{"detail":"the parent equals the flagged entry, but the flag gives real-rootedness only and one-signed coefficients are not shown: the weight of the coefficient of x^s of P_(n-2) in the coefficient of x^(s+2) is not shown to be >= 0 for n >= 2","route":"attestation","success":false,"variant":"oeis_catalog:A297191:lean_proved"},{"detail":"no lean_proved catalog entry equals the parent; 1 with the same first index and seeds differ in the rule or in later initial rows (oeis_catalog:A394446:lean_proved)","route":"attestation","success":false,"variant":"oeis_catalog"}],"conditional_on":[],"rows_checked":10,"statement":"open: no route proved that every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign; the first 10 parent rows pass the exact check (evidence only)","status":"not_proved"},"rows_compared":16,"schema":"polytool.recurrence-preserver-image.v1","statement":"Q_n = lambda(n) T_n(P_(n+0)) with T = f(n, theta) = 1 + (1) theta for every n >= 0 is certified; the lift is Open (open: no route proved that every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign; the first 10 parent rows pass the exact check (evidence only))"},"kind":"preserver_image"}