{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"modulus":2,"parent":{"first_index":0,"initial_polynomials":[["1"],["1","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-1","-2","-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"residue":1},"identifying_rows":4,"identity":{"certificate":{"exceptional_bases":[],"gauge":{"kind":"none"},"gauged_parent_relation":{"terms":[{"coeff":{"coeffs":[["1","2","1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-2","-2"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"shift":2}]},"identifying_indices":[0,1,2,3],"index_shift":0,"input_leader_shift":4,"input_relation":{"terms":[{"coeff":{"coeffs":[["1","-2","1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-4","4"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["6","-2"]]},"deriv_order":0,"shift":2},{"coeff":{"coeffs":[["-4"]]},"deriv_order":0,"shift":3},{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"shift":4}]},"input_valid_from_base":0,"modulus":2,"multiplier":["1"],"parent_leader_shift":2,"parent_relation":{"terms":[{"coeff":{"coeffs":[["1","2","1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-2","-2"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"shift":2}]},"parent_valid_from_base":0,"quotients":[{"component":0,"differentiations":[{"coeff":{"coeffs":[["-2"]]},"deriv_order":0}],"shift":0},{"component":1,"differentiations":[{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0}],"shift":0},{"component":0,"differentiations":[{"coeff":{"coeffs":[["2"]]},"deriv_order":0}],"shift":1},{"component":1,"differentiations":[{"coeff":{"coeffs":[["-2"]]},"deriv_order":0}],"shift":1},{"component":1,"differentiations":[{"coeff":{"coeffs":[["1"]]},"deriv_order":0}],"shift":2}],"residue":1,"statement":"w(n) e_1^T M = sum_nu H_nu S^nu phi(L~) with remainder zero, so w(n) (M V_(2,1)(P~))_n = 0 for every base n >= 0; with the exceptional bases checked exactly, V_(2,1)(P~) satisfies the input rule at every base n >= 0, and agreement on the 4 identifying rows gives Q_n = lambda(n) V_(2,1)(P_(n+0)) for every n >= 0"},"kind":"forward_division","status":"certified"},"input_first_index":0,"lean_replay":"not_attempted","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":{"interlacing":{"from_index":1,"justification":{"premises":["Q_n = lambda(n) V_(2,1)(P_(n+0)) for every n >= 0 (identity certified)","every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign (proved, route liu_wang_three_term)","the parent route proves P_(m-1) << P_m (weakly) for every m >= 1: liu_wang_three_term: L. L. Liu and Y. Wang, Adv. Appl. Math. 38 (2007) 542-560, Theorem 2.1 and Corollary 2.4 (A unified approach to polynomial sequences with only real zeros; the lag row as the interlacer, b_n = 0), weak interlacing of consecutive rows, with nonnegativity of the coefficients replaced, where a root region is certified, by an exact root-location induction; Proposition 3.3 (the case B_n(x) = -(c_n x + d_n)^2)","lambda(n) is finite and nonzero for every n >= n0 (verified: lambda(n) = 1)","each parent row is zero or real-rooted with coefficients of one sign; its negative, where needed, has nonnegative coefficients and the same zeros, and the section commutes with the sign change, so Corollary 5.6(b) applies to consecutive parent rows","the degrees of consecutive parent rows differ by at most one, hence so do those of their nonzero sections (a real-rooted polynomial with nonnegative coefficients has no internal zero coefficient, so deg V_(r,j)(P) = floor((deg P - j) / r))","a nonzero gauge lambda(n) moves no zero","hence Q_(n-1) << Q_n (weakly) for every n >= 1"],"theorem":"C. A. Athanasiadis and D. G. Wagner, Veronese sections and interlacing matrices of formal power series (arXiv:2404.12989), Corollary 5.6(b): if P and Q are real-rooted with nonnegative coefficients and the zeros of P interlace those of Q from the left (P << Q, Q carries the largest zero; the zero polynomial interlaces every such polynomial), then the k-th r-section of P interlaces that of Q in the same sense, for all 0 <= k < r"},"kind":"weak","orientation":"previous_interlaces_next"},"status":"proved"},"lean_replay":"not_attempted","operation":{"kind":"veronese_section","modulus":2,"residue":1},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["1","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-1","-2","-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"relation":"Q_n = lambda(n) V_(2,1)(P_(n+0)) for every n >= 0"},"parent_proof":{"route":"liu_wang_three_term","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 = lambda(n) V_(2,1)(P_(n+0)), 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":"Veronese sections of Polya frequency sequences (Aissen--Schoenberg--Whitney--Edrei): if P is real-rooted with coefficients of one sign, equivalently nonzero with all roots in (-inf, 0], every section V_(r,j)(P) is zero or real-rooted with roots in (-inf, 0]"},"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":"no theorem matched (weighted_renewal_window: coefficient of P_(n-1) must be 1 after normalization; fixed_delay_predecessor_window: coefficient of P_(n-1) must be 1 (+ w(n) t) after normalization)","route":"paper_theorem","success":false,"variant":"match_recurrence_theorems"},{"detail":"HypothesisFailed: P_n = (a_n + b_n (x + 1)) P_(n-1) - c_n (x + 1)^2 P_(n-2) for n >= 2, with a_n = 0, b_n = 2, c_n = 1; Q_n(y) = y^(d_n) P_n(1/y - 1), d_n = deg P_0 + n - 0, satisfies Q_n = (a_n y + b_n) Q_(n-1) - c_n Q_(n-2); open hypotheses: leading_coefficient_nonzero: fails at n = 2: f(n) a_n = 0 = 0 there (exact); first_coefficient_positive: a_2 or c_2 is undefined or a_2 = 0; recurrence_coefficient_positive: fails at n = 3: the denominator of beta_n = 1 vanishes there; root_region: the region contains the pole x = -1 of the coordinate change y = 1/(x + 1)","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":"HypothesisFailed: P_n = A_n(x) P_(n-1) + V_n(x) P'_(n-1) + W_n(x) P_(n-2) for n >= 2, with A_n(x) = (2) + (2) x, V_n(x) = 0, W_n(x) = (-1) + (-2) x + (-1) x^2; open hypotheses: lag_degree_step_nonnegative: fails at n = 2: mu_n = -1 = -1 there (exact); multipliers_vanish_at_zero: [x^0] c_2(n, x) = -1 is not the zero polynomial; lag_coefficient_nonpositive: W_n is not separable with a factor of one sign on (-inf, 0), and the sufficient monomial test (-1)^k [x^k] W_n <= 0 fails for k = 1 (not a disproof): fails at n = 2: [x^1] W_n = -2 there (exact); derivative_or_lag_coefficient_negative: W_n is not separable with a factor of one sign on (-inf, 0), and the sufficient monomial test (-1)^k [x^k] W_n <= 0 fails for k = 1 (not a disproof): fails at n = 2: [x^1] W_n = -2 there (exact)","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":"P_n = A_n(x) P_(n-1) + B_n(x) P_(n-2) for n >= 2, with A_n(x) = (2) + (2) x, B_n(x) = (-1) + (-2) x + (-1) x^2: every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0) (so its coefficients have one sign); for n >= 1, P_(n-1) interlaces P_n (weakly, in the sense of Liu and Wang), and deg P_n - deg P_(n-1) is 0 or 1 for n >= 2","route":"liu_wang_three_term","success":true,"variant":"liu_wang_three_term"}],"conditional_on":[],"interlacing":{"from_index":1,"justification":{"premises":["every hypothesis of the theorem is verified exactly for every index: P_n = A_n(x) P_(n-1) + B_n(x) P_(n-2) for n >= 2, with A_n(x) = (2) + (2) x, B_n(x) = (-1) + (-2) x + (-1) x^2","every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0) (so its coefficients have one sign); for n >= 1, P_(n-1) interlaces P_n (weakly, in the sense of Liu and Wang), and deg P_n - deg P_(n-1) is 0 or 1 for n >= 2"],"theorem":"liu_wang_three_term: L. L. Liu and Y. Wang, Adv. Appl. Math. 38 (2007) 542-560, Theorem 2.1 and Corollary 2.4 (A unified approach to polynomial sequences with only real zeros; the lag row as the interlacer, b_n = 0), weak interlacing of consecutive rows, with nonnegativity of the coefficients replaced, where a root region is certified, by an exact root-location induction; Proposition 3.3 (the case B_n(x) = -(c_n x + d_n)^2)"},"kind":"weak","orientation":"previous_interlaces_next"},"route":"liu_wang_three_term","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-veronese-certificate.v1","statement":"proved: Q_n = lambda(n) V_(2,1)(P_(n+0)) for every n >= 0 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 nonpositive roots","verdict":"proved"},"input":{"first_index":0,"initial_polynomials":[["0"],["2"],["4"],["6","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["4","0","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-6","2","0"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["4","-4","0"]]},"deriv_order":0,"offset":3,"sign":"none"},{"coeff":{"coeffs":[["-1","2","-1"]]},"deriv_order":0,"offset":4,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"kind":"veronese_section"}