{"kind":"theorem_check","report":{"conclusion":{"first_index":0,"root_region":{"upper":{"closed":true,"value":"0"}},"simple_roots":false,"statement":"every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0]; deg P_n = deg P_(n-1) + 1 for n >= 1"},"hypotheses":[{"evidence":"q(n) delta_S(n) sum_d c_d(n, x) D^d = f(n) (g H)(n, x) o S_num holds exactly in the Ore algebra (S_n = kappa (theta + a)(theta + b) + x (u + v theta) with kappa (t + a)(t + b) = 1 + (4) t + (3) t^2 and u + v theta = n + (-1) theta)","name":"operator_identity","statement":"the step operator T_n of the rule equals a_n(x) S_n","status":{"kind":"verified"}},{"evidence":"P_0 has degree 0; checked exactly","name":"start_row_in_region","statement":"P_0 is nonzero and real-rooted with every root in (-inf, 0]","status":{"kind":"verified"}},{"evidence":"delta = 1, deg P_(n-1) = n - 1: Lambda(n, deg P_(n-1)) = 1 != 0 for every integer n in [1, +inf) (exact; Taylor shift: the coefficients of Lambda(n, deg P_(n-1)) = 1 at n = 1 + u have one sign)","name":"degree_step","sign_decision":{"certificate":{"condition":"nonzero","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1"]},"numerator":["1"],"range":{"first":"1","last":null}},"decision":"holds"},"statement":"deg P_n = deg P_(n-1) + delta for every n >= 1: the coefficient Lambda(n, e) of x^(e + delta) in f(n) T_n(x^e) is nonzero at e = deg P_(n-1)","status":{"kind":"verified"}},{"evidence":"c_2(n) > 0 for every integer n in [1, +inf) (exact; Taylor shift: the coefficients of c_2(n) at n = 1 + u have one sign)","name":"euler_step_kappa_positive","sign_decision":{"certificate":{"condition":"positive","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["3"]},"numerator":["3"],"range":{"first":"1","last":null}},"decision":"holds"},"statement":"kappa(n) = c_2(n) > 0 for every n >= n0","status":{"kind":"verified"}},{"evidence":"c_1(n) > 0 for every integer n in [1, +inf) (exact; Taylor shift: the coefficients of c_1(n) at n = 1 + u have one sign)","name":"euler_step_diagonal_sum_positive","sign_decision":{"certificate":{"condition":"positive","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["4"]},"numerator":["4"],"range":{"first":"1","last":null}},"decision":"holds"},"statement":"kappa (a + b) = c_1(n) > 0 for every n >= n0 (with kappa > 0: a + b > 0)","status":{"kind":"verified"}},{"evidence":"c_0(n) > 0 for every integer n in [1, +inf) (exact; Taylor shift: the coefficients of c_0(n) at n = 1 + u have one sign)","name":"euler_step_diagonal_product_positive","sign_decision":{"certificate":{"condition":"positive","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1"]},"numerator":["1"],"range":{"first":"1","last":null}},"decision":"holds"},"statement":"kappa a b = c_0(n) > 0 for every n >= n0 (with kappa > 0: a b > 0)","status":{"kind":"verified"}},{"evidence":"c_1(n)^2 - 4 c_2(n) c_0(n) >= 0 for every integer n in [1, +inf) (exact; Taylor shift: the coefficients of c_1(n)^2 - 4 c_2(n) c_0(n) at n = 1 + u have one sign)","name":"euler_step_diagonal_real","sign_decision":{"certificate":{"condition":"nonnegative","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["4"]},"numerator":["4"],"range":{"first":"1","last":null}},"decision":"holds"},"statement":"c_1(n)^2 - 4 c_2(n) c_0(n) >= 0 for every n >= n0 (a and b real, hence both > 0)","status":{"kind":"verified"}},{"evidence":"u(n) > 0 for every integer n in [1, +inf) (exact; Taylor shift: the coefficients of u(n) at n = 1 + u have one sign)","name":"euler_step_raising_constant_positive","sign_decision":{"certificate":{"condition":"positive","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1","1"]},"numerator":["0","1"],"range":{"first":"1","last":null}},"decision":"holds"},"statement":"u(n) > 0 for every n >= n0","status":{"kind":"verified"}},{"evidence":"B(n) >= 0 for every integer n in [1, +inf) (exact; Taylor shift: the coefficients of B(n) at n = 1 + u have one sign)","name":"euler_step_comparison_defect_negative","sign_decision":{"certificate":{"condition":"nonnegative","denominator":["3"],"method":{"kind":"taylor_shift","shifted_denominator":["3"],"shifted_numerator":["13/2","3"]},"numerator":["7/2","3"],"range":{"first":"1","last":null}},"decision":"holds"},"statement":"the comparison defect kappa (a b - (a + b + 1)^2/4) + B s - v^2 s^2/(4 kappa),                      B = u - (a + b + 1) v/2, is < 0 for every s <= 0 and every n >= n0: its                      value at 0 is < 0, so this holds when B >= 0, and otherwise exactly when                      B^2 < v^2 ((a + b + 1)^2/4 - a b)","status":{"kind":"verified"}},{"evidence":"u(n) + v(n) deg P_(n-1) = 1 > 0 for every integer n in [1, +inf) (exact; Taylor shift: the coefficients of u(n) + v(n) deg P_(n-1) = 1 at n = 1 + u have one sign)","name":"euler_step_raising_positive_up_to_degree","sign_decision":{"certificate":{"condition":"positive","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1"]},"numerator":["1"],"range":{"first":"1","last":null}},"decision":"holds"},"statement":"u(n) + v(n) deg P_(n-1) > 0 for every n >= 1 (with u(n) > 0: u + v k > 0 for 0 <= k <= deg P_(n-1), the degree-local hypothesis)","status":{"kind":"verified"}},{"evidence":"the menu image of (-inf, 0] lies in (-inf, 0]","name":"preserver_keeps_region","statement":"S_n maps every polynomial that is zero or real-rooted with every root in (-inf, 0] to zero or such a polynomial, for every n >= 1","status":{"kind":"verified"}}],"iterated_preserver":{"degree_step":1,"induction_start":0,"multiplier_fixed_factor":["1"],"multiplier_index_factor":[{"denominator":["1"],"numerator":["1"]}],"operator_identity":"f(n) T_n = sum_d c_d(n, x) D^d equals f(n) a_n(x) S_n with a_n(x) = (1) ((1))","preserver":{"diagonal":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["4"]},{"denominator":["1"],"numerator":["3"]}],"raising":[{"denominator":["1"],"numerator":["0","1"]},{"denominator":["1"],"numerator":["-1"]}],"shape":"euler_step"},"region":{"upper":{"closed":true,"value":"0"}},"start_degree":0},"lean_declarations":["RealRooted.IsPFPolynomial.generalStep_of_natDegree_le","RealRooted.EulerBidiagonal.generalStep","RealRooted.EulerBidiagonal.comparisonDefect","RealRooted.EulerBidiagonal.generalRowsDep_spec"],"lean_replay":"not_attempted","normal_form":"P_n = a_n(x) S_n(P_(n-1)) for n >= 1, with a_n(x) = (1) ((1)) and S_n = kappa (theta + a)(theta + b) + x (u + v theta) with kappa (t + a)(t + b) = 1 + (4) t + (3) t^2 and u + v theta = n + (-1) theta","recurrence":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","0"],["0","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","7","-1"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","0","3"]]},"deriv_order":2,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"reference":"Iterated real-rootedness preservers (induction on n): if P_m is nonzero and real-rooted with every root in a closed region R and, for every n > m, P_n = a_n(x) S_n(P_(n-1)) where S_n maps every polynomial that is zero or real-rooted with every root in R to zero or a real-rooted polynomial with every root in R and a_n is real-rooted with every root in R, then every P_n is real-rooted with every root in R (the roots of a product are the roots of its factors); an exact degree step keeps every row nonzero; S_n = kappa (theta + a)(theta + b) + x (u + v theta) with kappa (t + a)(t + b) = 1 + (4) t + (3) t^2 and u + v theta = n + (-1) theta: The degree-local Euler step: T = kappa (theta + a)(theta + b) + x (u + v theta), theta = x D, with kappa, a, b > 0, u + v k > 0 for every k <= d and a negative comparison defect kappa (a b - (a + b + 1)^2/4) + (u - (a + b + 1) v/2) s - v^2 s^2/(4 kappa) < 0 for every s <= 0, maps every polynomial of degree <= d with nonnegative coefficients and only real roots to such a polynomial (RealRooted IsPFPolynomial.generalStep_of_natDegree_le, a half-line theorem: the symbol of T has discriminant -4 kappa s^2 times the comparison defect at s, so its real-rootedness is required for s <= 0 only, and the hypothesis (i) of P. Branden, Linear transformations preserving the Polya frequency property, Trans. Amer. Math. Soc. 358 (2006), Corollary 3.5, for every real s, is not needed); here d = deg P_(n-1), so u(n) + v(n) k > 0 is required for 0 <= k <= deg P_(n-1) only (both ends, the condition being linear in k); by linearity a row with nonpositive coefficients is handled through its negative","schema":"polytool.recurrence-real-rootedness-theorem.v1","status":"proved","theorem":"iterated_preserver"}}