{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"modulus":2,"parent":{"first_index":1,"initial_polynomials":[["1"],["0","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"residue":0},"identifying_rows":4,"identity":{"certificate":{"exceptional_bases":[],"gauge":{"kind":"none"},"gauged_parent_relation":{"terms":[{"coeff":{"coeffs":[["0","-1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-1","-1"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"shift":2}]},"identifying_indices":[1,2,3,4],"index_shift":0,"input_leader_shift":4,"input_relation":{"terms":[{"coeff":{"coeffs":[["0","-1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","-2"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["1","-1"]]},"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":1,"modulus":2,"multiplier":["1"],"parent_leader_shift":2,"parent_relation":{"terms":[{"coeff":{"coeffs":[["0","-1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-1","-1"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"shift":2}]},"parent_valid_from_base":1,"quotients":[{"component":1,"differentiations":[{"coeff":{"coeffs":[["0","1"]]},"deriv_order":0}],"shift":0},{"component":0,"differentiations":[{"coeff":{"coeffs":[["-1"]]},"deriv_order":0}],"shift":1},{"component":1,"differentiations":[{"coeff":{"coeffs":[["0","1"]]},"deriv_order":0}],"shift":1},{"component":0,"differentiations":[{"coeff":{"coeffs":[["1"]]},"deriv_order":0}],"shift":2}],"residue":0,"statement":"w(n) e_0^T M = sum_nu H_nu S^nu phi(L~) with remainder zero, so w(n) (M V_(2,0)(P~))_n = 0 for every base n >= 1; with the exceptional bases checked exactly, V_(2,0)(P~) satisfies the input rule at every base n >= 1, and agreement on the 4 identifying rows gives Q_n = lambda(n) V_(2,0)(P_(n+0)) for every n >= 1"},"kind":"forward_division","status":"certified"},"input_first_index":1,"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":1,"input_interlacing":{"interlacing":{"from_index":2,"justification":{"premises":["Q_n = lambda(n) V_(2,0)(P_(n+0)) for every n >= 1 (identity certified)","every parent row P_n, n >= 1, is zero or real-rooted with coefficients of one sign (proved, route liu_wang_derivative_lag)","the parent route proves P_(m-1) << P_m (weakly) for every m >= 2: liu_wang_derivative_lag: L. L. Liu and Y. Wang, A unified approach to polynomial sequences with only real zeros, Adv. in Appl. Math. 38 (2007) 542-560, Theorem 2.1 with the interlacers f' and the lag row (strict form, as in the derivative-lag theorems of the RealRooted library, https://github.com/PerAlexandersson/RealRooted), with nonnegativity of the coefficients replaced by an exact induction keeping every root in (-inf, 0)","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 >= 2"],"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":0},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":1,"initial_polynomials":[["1"],["0","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","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) V_(2,0)(P_(n+0)) for every n >= 1"},"parent_proof":{"route":"liu_wang_derivative_lag","statement":"every parent row P_n, n >= 1, is zero or real-rooted with coefficients of one sign","status":"proved"},"root_transfer":{"input_conclusion":"every Q_n = lambda(n) V_(2,0)(P_(n+0)), n >= 1, 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: more than one weighted lag)","route":"paper_theorem","success":false,"variant":"match_recurrence_theorems"},{"detail":"not applicable: c_2(n, x) = gamma(n) w(x) with w neither constant nor a constant times a square (x + v_0)^2","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":"induction start moved 1 row(s) past the seeds: P_n = x^1 Q_n for n >= 2 (x^1 divides P_2 and P_3, and V_n(0) = 0), with Q_n = A_n(x) Q_(n-1) + V_n(x) Q'_(n-1) + W_n(x) Q_(n-2) for n >= 4, A_n(x) = (1) + (1) x, V_n(x) = 0, W_n(x) = (1) x (A_n = a_n + 1 V_n / x for the rule's a_n(x) = (1) + (1) x): every P_n, n >= 1, is nonzero and real-rooted with every root in (-inf, 0] (so its coefficients have one sign); P_n = x^1 Q_n for n >= 2 with Q_n(0) != 0, and for n >= 3 the Q_n have simple roots, Q_(n-1) strictly interlaces Q_n, and P_(n-1) interlaces P_n (Liu--Wang, common root 0); the rule is applied from n = 4 on in the induction (start moved 1 row(s) past the supplied seeds; P_1, ..., P_3 enter as seed rows, checked exactly); P_(m-1) interlaces P_m checked exactly for m = 2, ..., 2","route":"liu_wang_derivative_lag","success":true,"variant":"liu_wang_derivative_lag"}],"conditional_on":[],"interlacing":{"from_index":2,"justification":{"premises":["every hypothesis of the theorem is verified exactly for every index: P_n = x^1 Q_n for n >= 2 (x^1 divides P_2 and P_3, and V_n(0) = 0), with Q_n = A_n(x) Q_(n-1) + V_n(x) Q'_(n-1) + W_n(x) Q_(n-2) for n >= 4, A_n(x) = (1) + (1) x, V_n(x) = 0, W_n(x) = (1) x (A_n = a_n + 1 V_n / x for the rule's a_n(x) = (1) + (1) x)","every P_n, n >= 1, is nonzero and real-rooted with every root in (-inf, 0] (so its coefficients have one sign); P_n = x^1 Q_n for n >= 2 with Q_n(0) != 0, and for n >= 3 the Q_n have simple roots, Q_(n-1) strictly interlaces Q_n, and P_(n-1) interlaces P_n (Liu--Wang, common root 0); the rule is applied from n = 4 on in the induction (start moved 1 row(s) past the supplied seeds; P_1, ..., P_3 enter as seed rows, checked exactly); P_(m-1) interlaces P_m checked exactly for m = 2, ..., 2"],"theorem":"liu_wang_derivative_lag: L. L. Liu and Y. Wang, A unified approach to polynomial sequences with only real zeros, Adv. in Appl. Math. 38 (2007) 542-560, Theorem 2.1 with the interlacers f' and the lag row (strict form, as in the derivative-lag theorems of the RealRooted library, https://github.com/PerAlexandersson/RealRooted), with nonnegativity of the coefficients replaced by an exact induction keeping every root in (-inf, 0)"},"kind":"weak","orientation":"previous_interlaces_next"},"route":"liu_wang_derivative_lag","rows_checked":10,"statement":"every parent row P_n, n >= 1, 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,0)(P_(n+0)) for every n >= 1 and every parent row P_n, n >= 1, is zero or real-rooted with coefficients of one sign; so every Q_n, n >= 1, is zero or real-rooted with nonpositive roots","verdict":"proved"},"input":{"first_index":1,"initial_polynomials":[["1"],["0"],["0","1"],["0","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-1","1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["0","2"]]},"deriv_order":0,"offset":3,"sign":"none"},{"coeff":{"coeffs":[["0","1"]]},"deriv_order":0,"offset":4,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"kind":"veronese_section"}