{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"schedule":{"first_degree":0,"first_index":0,"step":2},"shape":"reversal"},"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":[["-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}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"denominator":{"coeffs":[["-1"],["2"]]},"terms":[{"coeff":{"coeffs":[["-1","-9","5","4"],["2","12","-20","-4"],["0","0","16","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","-1","-4","29","8"],["0","0","-4","-24","-4"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","0","0","2","12","2"]]},"deriv_order":2,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["1/2","1"],"operator":{"schedule":{"first_degree":0,"first_index":0,"step":2},"shape":"reversal"},"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":[["1"],["2"]]},"deriv_order":0}],"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":[],"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":[["2"]]},"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 = x^(d_n) P(1/x), d_n = 0 + 2 (n - 0); 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":"the schedule d_n depends on n","status":"none"},"lean_declarations":["RealRooted.X_pow_mul_reverse_eq_zero_or_splits","RealRooted.reflect_eq_zero_or_splits"],"lean_route":"reversed","lift_summary":{"hypotheses":[{"evidence":"lambda(n) = 1","name":"gauge_finite_nonzero","statement":"lambda(n) is finite and nonzero for every n >= n0","status":{"kind":"verified"}}],"identity":{"method":"forward_division","status":"certified"},"input_first_index":0,"input_interlacing":{"reason":"the schedule d_n depends on n","status":"not_proved"},"lean_replay":"not_attempted","operation":{"description":"x^(d_n) P(1/x), d_n = 0 + 2 (n - 0)","kind":"preserver_image","operator":{"schedule":{"first_degree":0,"first_index":0,"step":2},"shape":"reversal"}},"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 = x^(d_n) P(1/x), d_n = 0 + 2 (n - 0), 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":"a real affine substitution x -> a x + b (a != 0), the reversal x^d p(1/x) (d >= deg p) and a real Mobius map (c x + e)^d p((a x + b)/(c x + e)) (a e - b c != 0, d >= deg p) map real roots to real roots: a root r of p gives the root (r - b)/a, 1/r (and 0) or (e r - b)/(a - c r) (and -e/c); for an input row that is a polynomial the degree condition holds automatically"},"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 = x^(d_n) P(1/x), d_n = 0 + 2 (n - 0) 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"}