{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"factor":{"terms":[{"coefficient_offset":0,"index_offset":0,"kind":"binomial"}]},"shape":"hadamard_multiplier"},"parent":{"first_index":0,"initial_polynomials":[["1"],["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"n-75ccd0453a9b6cec"},"identifying_rows":2,"identity":{"certificate":{"certificate":{"factor":{"terms":[{"coefficient_offset":0,"index_offset":0,"kind":"binomial"}]},"hadamard":{"conjugated_input_relation":{"terms":[{"coeff":{"coeffs":[["2","-4"],["5","-8"],["4","-4"],["1","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","-2","4"],["0","-4","0"],["0","-2","-4"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0","1","4"],["0","0","1","4"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["-6"],["-13"],["-9"],["-2"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","3"],["0","5"],["0","2"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["4"],["8"],["5"],["1"]]},"deriv_order":0,"shift":2}]},"conjugation_x_shift":0,"exceptional_bases":[],"factor":{"terms":[{"coefficient_offset":0,"index_offset":0,"kind":"binomial"}]},"gauge":{"kind":"none"},"identifying_indices":[0,1],"input_leader_shift":2,"input_relation":{"terms":[{"coeff":{"coeffs":[["1","-4"],["1","-4"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-3"],["-2"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["2"],["1"]]},"deriv_order":0,"shift":2}]},"input_valid_from_base":0,"multiplier":["1","2","1"],"parent":{"first_index":0,"initial_polynomials":[["1"],["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_leader_shift":2,"parent_relation":{"terms":[{"coeff":{"coeffs":[["0","-1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-1"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"shift":2}]},"parent_valid_from_base":0,"quotients":[{"differentiations":[{"coeff":{"coeffs":[["0","4","16"],["0","16","64"],["0","25","100"],["0","19","76"],["0","7","28"],["0","1","4"]]},"deriv_order":0}],"shift":0}],"row_annihilator_system":{"generators":[{"annihilator":{"terms":[{"coeff":{"coeffs":[["-1","0"],["-1","-2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","1","4"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["1"],["1"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","-2","-8"],["0","-7","-28"],["0","-9","-36"],["0","-5","-20"],["0","-1","-4"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","3","12"],["0","0","8","32"],["0","0","7","28"],["0","0","2","8"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["0","1","4"],["0","2","8"],["0","1","4"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","-2","-8"],["0","0","-4","-16"],["0","0","-2","-8"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","1","8","16"],["0","0","1","8","16"]]},"deriv_order":1}],[{"coeff":{"coeffs":[["0","0","-1","-8","-16"],["0","0","-1","-8","-16"]]},"deriv_order":0}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0"],["-1"],["1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","6"],["-1","-4"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","1","4"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","0","-2","-8"],["0","0","-5","-20"],["0","0","-4","-16"],["0","0","-1","-4"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["0","0","1","8","16"],["0","0","3","24","48"],["0","0","3","24","48"],["0","0","1","8","16"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","0","0"],["0","0","1","8","16"],["0","0","3","24","48"],["0","0","3","24","48"],["0","0","1","8","16"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","-1","-6","0","32"],["0","0","-3","-24","-48","0"],["0","0","-3","-30","-96","-96"],["0","0","-1","-12","-48","-64"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","1","12","48","64"],["0","0","0","2","24","96","128"],["0","0","0","1","12","48","64"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","1","4","-16","-64"],["0","0","3","18","0","-96"],["0","0","3","24","48","0"],["0","0","1","10","32","32"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-1","-12","-48","-64"],["0","0","0","-2","-24","-96","-128"],["0","0","0","-1","-12","-48","-64"]]},"deriv_order":1}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["0","1","4"]]},"start_base":0},"row_multiplier":["1"],"statement":"mu(x) w(n) M'' = sum_nu H_nu S^nu L + sum_l Z_l A_l (an invariant row-annihilator system of the parent) with M'' the input relation conjugated by lambda(n) binom(n, k); 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) sum_k u(n,k) [x^k]P_n x^k for every n >= 0"},"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["1"],["1"]],"recurrence":{"denominator":{"coeffs":[["0"],["1"]]},"terms":[{"coeff":{"coeffs":[["-1"],["2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["1","-4"],["-1","4"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent":{"first_index":0,"initial_polynomials":[["1"],["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"}},"method":"hadamard_conjugation"},"status":"certified"},"input_first_index":0,"interlacing":{"reason":"the factor depends on n","status":"none"},"lift_summary":{"hypotheses":[{"evidence":"binom(n, k) is defined for every n >= 0","name":"factor_defined","statement":"the factor u(n, k) is defined on the index domain","status":{"kind":"verified"}},{"evidence":"binom(n, k): sum_k u(n,k) x^k / k! = L_(A-0)^(0)(-x) with A = n + a (zero when A < 0), a Laguerre polynomial with parameter 0 > -1, whose zeros are real and positive (Szego, Orthogonal Polynomials, Theorem 3.3.1); third condition of Theorem 40","name":"factor_multiplier_sequence","statement":"k -> u(n, k) is a nonnegative multiplier sequence 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"}}],"identity":{"method":"hadamard_conjugation","status":"certified"},"input_first_index":0,"input_interlacing":{"reason":"the factor depends on n","status":"not_proved"},"lean_replay":"not_attempted","operation":{"description":"x^k -> binom(n, k) x^k","kind":"preserver_image","operator":{"factor":{"terms":[{"coefficient_offset":0,"index_offset":0,"kind":"binomial"}]},"shape":"hadamard_multiplier"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["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^k -> binom(n, k) x^k, for every n >= 0"},"parent_proof":{"route":"paper_theorem","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":"Polya--Schur characterization of multiplier sequences (G. Polya and I. Schur, J. Reine Angew. Math. 144 (1914) 89--113; stated as Theorem 40 of P. Branden, Unimodality, log-concavity, real-rootedness and beyond, arXiv:1410.6601): a real sequence (lambda_k) is a multiplier sequence (x^k -> lambda_k x^k maps real-rooted polynomials to real-rooted polynomials or zero) iff sum_k binom(m,k) lambda_k x^k is real-rooted with zeros of one sign for every m, iff sum_k lambda_k x^k / k! (or its reflection) is C x^m e^(a x) prod (1 + alpha_j x) with a, alpha_j >= 0; a product of multiplier sequences is one (composition), and a nonzero factor lambda(n) of the row changes nothing"},"verdict":"proved"},"notes":[],"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":"P_n = P_(n-1) + t P_(n-2); P_0 = 1, P_m = 0 for m < 0; generating function 1/(1 - x R(t x^1)) (paper_proof_not_lean_checked): For all n, s >= 0 with 1*s <= 1*1+1: P_n << P_(n+s) (oriented weak interlacing; shared and repeated zeros allowed). Every P_n has nonnegative coefficients and constant term 1 and is real-rooted.; the identifying seeds equal the canonical rows (Canonical), so every parent row is a canonical row","route":"paper_theorem","success":true,"variant":"weighted_renewal_window"},{"detail":"the parent rows are not the canonical boundary rows (Mismatch)","route":"paper_theorem","success":false,"variant":"fixed_delay_predecessor_window"}],"conditional_on":[],"interlacing":{"from_index":1,"justification":{"premises":["homogeneous, index-independent, no derivatives or sign factors; every t^j term has lag 1 + 1*j with ell = 1 >= 1 (exact_structural)","R(z) = 1 + 1 z has R(0) = 1 and nonnegative coefficients (exact_rational)","R(z) has only real zeros (exact_root_count)","window: P_n << P_(n+s) for every n >= 0 and 0 <= s <= 2 (1*s <= 1*1+1 (d*s <= d*ell+1))","the identifying parent seeds equal the canonical rows (Canonical), so every parent row is a canonical row and consecutive parent rows are consecutive canonical rows"],"theorem":"weighted_renewal_window (paper_proof_not_lean_checked; https://github.com/PerAlexandersson/RealRooted/issues/2037): For all n, s >= 0 with 1*s <= 1*1+1: P_n << P_(n+s) (oriented weak interlacing; shared and repeated zeros allowed). Every P_n has nonnegative coefficients and constant term 1 and is real-rooted."},"kind":"weak","orientation":"previous_interlaces_next"},"route":"paper_theorem","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 = x^k -> binom(n, k) x^k 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"}