{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"modulus":2,"parent":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","0"],["0","1"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"residue":0},"identifying_rows":3,"identity":{"certificate":{"exceptional_bases":[],"gauge":{"kind":"none"},"gauged_parent_relation":{"terms":[{"coeff":{"coeffs":[["-1","-1"],["0","-1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"shift":1}]},"identifying_indices":[0,1,2],"index_shift":0,"input_leader_shift":3,"input_relation":{"terms":[{"coeff":{"coeffs":[["-1","1"],["0","2"],["0","1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["3","-6"],["0","-5"],["0","-1"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["-3"]]},"deriv_order":0,"shift":2},{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"shift":3}]},"input_valid_from_base":0,"modulus":2,"multiplier":["1"],"parent_leader_shift":1,"parent_relation":{"terms":[{"coeff":{"coeffs":[["-1","-1"],["0","-1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"shift":1}]},"parent_valid_from_base":0,"quotients":[{"component":0,"differentiations":[{"coeff":{"coeffs":[["1"]]},"deriv_order":0}],"shift":0},{"component":1,"differentiations":[{"coeff":{"coeffs":[["0","-1"],["0","-1"]]},"deriv_order":0}],"shift":0},{"component":0,"differentiations":[{"coeff":{"coeffs":[["-2"]]},"deriv_order":0}],"shift":1},{"component":1,"differentiations":[{"coeff":{"coeffs":[["0","3"],["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 >= 0; with the exceptional bases checked exactly, V_(2,0)(P~) satisfies the input rule at every base n >= 0, and agreement on the 3 identifying rows gives Q_n = lambda(n) V_(2,0)(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,0)(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: fixed_delay_predecessor_window (paper_proof_not_lean_checked; https://github.com/PerAlexandersson/RealRooted/issues/2037): For every n >= 1: Q_n has nonnegative coefficients and constant term 1, is real-rooted, and Q_i << Q_n (oriented weak interlacing) for p(n) <= i <= n. Hence Q_A << Q_B whenever 0 <= A <= B and B - A <= 1.","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":0},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","0"],["0","1"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"relation":"Q_n = lambda(n) V_(2,0)(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,0)(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":"Q_0 = 1, Q_n = Q_(n-1) + w(n) t Q_(max(0, n-1)), w(n) = n (paper_proof_not_lean_checked): For every n >= 1: Q_n has nonnegative coefficients and constant term 1, is real-rooted, and Q_i << Q_n (oriented weak interlacing) for p(n) <= i <= n. Hence Q_A << Q_B whenever 0 <= A <= B and B - A <= 1.; the identifying seeds equal the canonical rows (Canonical), so every parent row is a canonical row","route":"paper_theorem","success":true,"variant":"fixed_delay_predecessor_window"}],"conditional_on":[],"interlacing":{"from_index":1,"justification":{"premises":["p(n) = max(0, n-1) with 1 >= 1 is nondecreasing and 0 <= p(n) < n for n >= 1 (exact_structural)","w(n) >= 0 for every integer n >= 1: w(1+m) has nonnegative coefficients [1, 1] in m (exact_symbolic_certificate)","window: Q_A << Q_B for 0 <= A <= B with B - A <= 1 (B - A <= 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":"fixed_delay_predecessor_window (paper_proof_not_lean_checked; https://github.com/PerAlexandersson/RealRooted/issues/2037): For every n >= 1: Q_n has nonnegative coefficients and constant term 1, is real-rooted, and Q_i << Q_n (oriented weak interlacing) for p(n) <= i <= n. Hence Q_A << Q_B whenever 0 <= A <= B and B - A <= 1."},"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,0)(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":[["1"],["1"],["1","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["3","0"],["0","0"],["0","0"],["0","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-3","0"],["0","-1"],["0","1"],["0","0"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["1","-4"],["0","4"],["0","-1"],["0","0"]]},"deriv_order":0,"offset":3,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"kind":"veronese_section"}