{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"intercept":"1","shape":"affine","slope":"1"},"parent":{"first_index":0,"initial_polynomials":[["1"],["2"],["3","3"]],"recurrence":{"denominator":{"coeffs":[["2"],["1"]]},"terms":[{"coeff":{"coeffs":[["3","0"],["3","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","4"],["-3","4"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["-1","4"],["1","-4"]]},"deriv_order":0,"offset":3,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"gamma_polynomial of Triangle read by rows, n>=1, 1<=k<=n, T(n,k) = k*binomial(n,k)^2/(n-k+1)."},"identifying_rows":2,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["6","-24"],["5","-20"],["1","-4"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-15"],["-11"],["-2"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["8"],["6"],["1"]]},"deriv_order":0,"shift":2}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0,1],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["1"],["2"]],"recurrence":{"denominator":{"coeffs":[["0"],["2"],["1"]]},"terms":[{"coeff":{"coeffs":[["0","0"],["3","4"],["3","4"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["1"],["3"],["2"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["12","19","8","1"],"operator":{"intercept":"1","shape":"affine","slope":"1"},"parent":{"first_index":0,"initial_polynomials":[["1"],["2"],["3","3"]],"recurrence":{"denominator":{"coeffs":[["2"],["1"]]},"terms":[{"coeff":{"coeffs":[["3","0"],["3","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","4"],["-3","4"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["-1","4"],["1","-4"]]},"deriv_order":0,"offset":3,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_leader_shift":3,"parent_valid_from_base":0,"quotients":[],"row_annihilation":{"kind":"system","system":{"generators":[{"annihilator":{"terms":[{"coeff":{"coeffs":[["6","-12"],["2","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","2","-8"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-9"],["-3"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["4"],["1"]]},"deriv_order":0,"shift":2}]},"quotient":[{"coeff":{"coeffs":[["24"],["50"],["35"],["10"],["1"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["0","-9","36"],["0","-24","96"],["0","-22","88"],["0","-8","32"],["0","-1","4"]]},"step_quotients":[[],[{"coeff":{"coeffs":[["0","15","-120","240"],["0","38","-304","608"],["0","32","-256","512"],["0","10","-80","160"],["0","1","-8","16"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","-30","240","-480"],["0","0","-46","368","-736"],["0","0","-18","144","-288"],["0","0","-2","16","-32"]]},"deriv_order":1}],[{"coeff":{"coeffs":[["0","0","120","-960","1920"],["0","0","244","-1952","3904"],["0","0","164","-1312","2624"],["0","0","44","-352","704"],["0","0","4","-32","64"]]},"deriv_order":0}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["-6","0"],["-5","-8"],["-1","-4"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","-4","16"],["0","-2","8"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["3"],["4"],["1"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["12"],["19"],["8"],["1"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["0","-36","144"],["0","-105","420"],["0","-112","448"],["0","-54","216"],["0","-12","48"],["0","-1","4"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","-360","1440"],["0","-1302","5208"],["0","-1891","7564"],["0","-1429","5716"],["0","-610","2440"],["0","-148","592"],["0","-19","76"],["0","-1","4"]]},"deriv_order":0}],[{"coeff":{"coeffs":[["0","-360","2160","-2880"],["0","-1122","6732","-8976"],["0","-1330","7980","-10640"],["0","-764","4584","-6112"],["0","-228","1368","-1824"],["0","-34","204","-272"],["0","-2","12","-16"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","360","-2880","5760"],["0","0","762","-6096","12192"],["0","0","568","-4544","9088"],["0","0","196","-1568","3136"],["0","0","32","-256","512"],["0","0","2","-16","32"]]},"deriv_order":1}],[{"coeff":{"coeffs":[["0","0","-1440","11520","-23040"],["0","0","-3768","30144","-60288"],["0","0","-3796","30368","-60736"],["0","0","-1920","15360","-30720"],["0","0","-520","4160","-8320"],["0","0","-72","576","-1152"],["0","0","-4","32","-64"]]},"deriv_order":0}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0"],["-1"],["1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-2","6"],["0","-4"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-1","4"]]},"deriv_order":2,"shift":0}]},"quotient":[],"step_multiplier":{"coeffs":[["0","0","27","-216","432"],["0","0","108","-864","1728"],["0","0","171","-1368","2736"],["0","0","136","-1088","2176"],["0","0","57","-456","912"],["0","0","12","-96","192"],["0","0","1","-8","16"]]},"step_quotients":[[],[{"coeff":{"coeffs":[["0","0","0","0","0"],["0","0","45","-360","720"],["0","0","174","-1392","2784"],["0","0","263","-2104","4208"],["0","0","196","-1568","3136"],["0","0","75","-600","1200"],["0","0","14","-112","224"],["0","0","1","-8","16"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","-90","810","-2160","1440"],["0","0","-258","2142","-4752","1248"],["0","0","-268","1896","-2304","-3968"],["0","0","-124","580","1312","-6592"],["0","0","-26","-14","1360","-3552"],["0","0","-2","-34","368","-800"],["0","0","0","-4","32","-64"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","-45","540","-2160","2880"],["0","0","0","-129","1548","-6192","8256"],["0","0","0","-134","1608","-6432","8576"],["0","0","0","-62","744","-2976","3968"],["0","0","0","-13","156","-624","832"],["0","0","0","-1","12","-48","64"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","450","-4320","12960","-11520"],["0","0","1605","-14904","42192","-33024"],["0","0","2288","-20268","52320","-31424"],["0","0","1687","-13972","30800","-7616"],["0","0","698","-5256","8544","5248"],["0","0","163","-1072","752","3712"],["0","0","20","-108","-96","832"],["0","0","1","-4","-16","64"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","180","-2160","8640","-11520"],["0","0","0","606","-7272","29088","-38784"],["0","0","0","794","-9528","38112","-50816"],["0","0","0","516","-6192","24768","-33024"],["0","0","0","176","-2112","8448","-11264"],["0","0","0","30","-360","1440","-1920"],["0","0","0","2","-24","96","-128"]]},"deriv_order":1}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["1"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-2","8"],["-1","4"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["9","-16"],["3","-4"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["-12"],["-3"]]},"deriv_order":0,"shift":2},{"coeff":{"coeffs":[["5"],["1"]]},"deriv_order":0,"shift":3}]},"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 = P((1) x + (1)); 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":{"reason":"no parent theorem report with an interlacing conclusion","status":"none"},"lean_declarations":["Polynomial.Splits.comp_of_degree_le_one"],"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":"no parent theorem report with an interlacing conclusion","status":"not_proved"},"lean_replay":"not_attempted","operation":{"description":"P((1) x + (1))","kind":"preserver_image","operator":{"intercept":"1","shape":"affine","slope":"1"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["2"],["3","3"]],"recurrence":{"denominator":{"coeffs":[["2"],["1"]]},"terms":[{"coeff":{"coeffs":[["3","0"],["3","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","4"],["-3","4"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["-1","4"],["1","-4"]]},"deriv_order":0,"offset":3,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"relation":"Q_n = lambda(n) T_n(P_(n+0)) with T = P((1) x + (1)), 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, -1]","input_root_region":{"upper":{"closed":true,"value":"-1"}},"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 leader is not a nonzero constant","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: LHS must be a nonzero constant; fixed_delay_predecessor_window: LHS must be a nonzero constant)","route":"paper_theorem","success":false,"variant":"match_recurrence_theorems"},{"detail":"not applicable: the rule is not f(n) P_n = c_1(n, x) P_(n-1) + c_2(n, x) P_(n-2) with both terms nonzero","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: the rule is not f(n) P_n = c_0(n, x) P_(n-1) + c_1(n, x) P'_(n-1) + c_2(n, x) P_(n-2) with a derivative or a lag term","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: the rule is not f(n) P_n = c_1(n, x) P_(n-1) + c_d(n, x) P'_(n-1) + c_2(n, x) P_(n-2) with a nonzero lag term and a nonzero P_(n-1) or P'_(n-1) term","route":"liu_wang_three_term","success":false,"variant":"liu_wang_three_term"},{"detail":"Unresolved: row relation p(n, k) [x^k] P_n + q(n, k) [x^(k-1)] P_n = 0, n >= 0, with p = (-1) (k) (k + 1), q = (4) (k - 1/2 n - 1) (k - 1/2 n - 1/2); valuation v(n) = 0; open hypotheses: multiplier_matching: no matching of the ratio factors (identity: R(n, j) = -q(n, j + v(n)) / p(n, j + v(n))) with a base binom(M, j), complements, pairs and reciprocal rising factorials holds for every n >= 0 + delay, delay <= 4","route":"hypergeometric_row","success":false,"variant":"hypergeometric_row"}],"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 = P((1) x + (1)) 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"}