{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"modulus":2,"parent":{"first_index":0,"initial_polynomials":[["1"],["1","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","0","-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":[["0","0","1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-1","-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":[["0","0","1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","-2"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["1","-2"]]},"deriv_order":0,"shift":2},{"coeff":{"coeffs":[["-2"]]},"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":[["0","0","1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-1","-2"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"shift":2}]},"parent_valid_from_base":0,"quotients":[{"component":1,"differentiations":[{"coeff":{"coeffs":[["0","1"]]},"deriv_order":0}],"shift":0},{"component":0,"differentiations":[{"coeff":{"coeffs":[["2"]]},"deriv_order":0}],"shift":1},{"component":1,"differentiations":[{"coeff":{"coeffs":[["-1"]]},"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 three_term_recurrence)","the parent route proves P_(m-1) << P_m (strictly) for every m >= 1: three_term_recurrence: three-term recurrence Q_n = (a_n y + b_n) Q_(n-1) - c_n Q_(n-2) with a_n != 0 and beta_n = c_n / (a_n a_(n-1)) > 0: simple real roots and strict interlacing of consecutive rows (zero separation for orthogonal polynomials: G. Szeg\u0151, Orthogonal Polynomials, \u00a73.3; Favard, C. R. Acad. Sci. Paris 200 (1935)); root regions by a positive-ratio (chain-sequence) induction","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","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"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) V_(2,1)(P_(n+0)) for every n >= 0"},"parent_proof":{"route":"three_term_recurrence","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: 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":"P_n = (a_n + b_n (x + 0)) P_(n-1) - c_n (x + 0)^2 P_(n-2) for n >= 2, with a_n = 1, b_n = 2, c_n = 1; Q_n(y) = y^(d_n) P_n(1/y + 0), d_n = deg P_0 + n - 0, satisfies Q_n = (a_n y + b_n) Q_(n-1) - c_n Q_(n-2): every P_n, n >= 0, is nonzero and real-rooted, with simple roots from n = 0 on; P_(n-1) strictly interlaces P_n for n >= 1; every root lies in (-inf, 0)","route":"three_term_recurrence","success":true,"variant":"three_term_recurrence"}],"conditional_on":[],"interlacing":{"from_index":1,"justification":{"premises":["every hypothesis of the theorem is verified exactly for every index: P_n = (a_n + b_n (x + 0)) P_(n-1) - c_n (x + 0)^2 P_(n-2) for n >= 2, with a_n = 1, b_n = 2, c_n = 1; Q_n(y) = y^(d_n) P_n(1/y + 0), d_n = deg P_0 + n - 0, satisfies Q_n = (a_n y + b_n) Q_(n-1) - c_n Q_(n-2)","every P_n, n >= 0, is nonzero and real-rooted, with simple roots from n = 0 on; P_(n-1) strictly interlaces P_n for n >= 1; every root lies in (-inf, 0)"],"theorem":"three_term_recurrence: three-term recurrence Q_n = (a_n y + b_n) Q_(n-1) - c_n Q_(n-2) with a_n != 0 and beta_n = c_n / (a_n a_(n-1)) > 0: simple real roots and strict interlacing of consecutive rows (zero separation for orthogonal polynomials: G. Szeg\u0151, Orthogonal Polynomials, \u00a73.3; Favard, C. R. Acad. Sci. Paris 200 (1935)); root regions by a positive-ratio (chain-sequence) induction"},"kind":"strict","orientation":"previous_interlaces_next"},"route":"three_term_recurrence","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"],["1"],["3"],["5","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","0","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-1","2","0"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["0","2","0"]]},"deriv_order":0,"offset":3,"sign":"none"},{"coeff":{"coeffs":[["0","0","-1"]]},"deriv_order":0,"offset":4,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"kind":"veronese_section"}