{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"modulus":2,"parent":{"first_index":0,"initial_polynomials":[["1"],["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","3"]]},"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","-3"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-1"]]},"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","-9"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["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":0,"modulus":2,"multiplier":["1"],"parent_leader_shift":2,"parent_relation":{"terms":[{"coeff":{"coeffs":[["0","-3"]]},"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":[{"component":0,"differentiations":[{"coeff":{"coeffs":[["3"]]},"deriv_order":0}],"shift":0},{"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 paper_theorem)","the parent route proves P_(m-1) << P_m (weakly) for every m >= 1: 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.","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"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","3"]]},"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":"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 = 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":"P_n = P_(n-1) + 3 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 + 3 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-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"],["0"],["3"],["6"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-1","0"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["0","9"]]},"deriv_order":0,"offset":4,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"kind":"veronese_section"}