{"kind":"theorem_check","report":{"conclusion":{"first_index":1,"root_region":{"upper":{"closed":false,"value":"0"}},"simple_roots":false,"statement":"every P_n, n >= 1, is nonzero and real-rooted with every root in (-inf, 0): for n >= 1 the coefficients U_j (U_j = [x^(j + v(n))] P_n, v(n) = 0) satisfy U_j = U_0(n) prod_(t <= j) R(n, t), R(n, j) = (-1/4) (j - n) / ((j - 1/2) (j)), so sum_j U_j y^j is U_0(n) times the image of (1 + y)^(n - 1) under a nonnegative multiplier sequence, and U_0(n) != 0 for n >= 1 by its scalar recurrence"},"hypotheses":[{"evidence":"invariant system with 1 generator(s) from base 1 (restart bases []), mu H = sum_l Z_l A^(l), H P_m = 0 checked exactly at the zeros [] of mu","name":"row_relation","statement":"H(n) P_n = 0 for every n >= the first base, H = p(n, theta) + x q(n, theta + 1): an invariant row-annihilator system of the rule contains H","status":{"kind":"verified"}},{"evidence":"M(n) = n - 1 >= 0 for every integer n in [1, +inf) (exact; Taylor shift: the coefficients of M(n) = n - 1 at n = 1 + u have one sign)","name":"base_size","sign_decision":{"certificate":{"condition":"nonnegative","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["0","1"]},"numerator":["-1","1"],"range":{"first":"1","last":null}},"decision":"holds"},"statement":"the base factor j - n and the factor j give binom(M, j) with M(n) >= 0","status":{"kind":"verified"}},{"evidence":"b(n) + 1 = 1/2 > 0 for every integer n in [1, +inf) (exact; Taylor shift: the coefficients of b(n) + 1 = 1/2 at n = 1 + u have one sign)","name":"reciprocal_0","sign_decision":{"certificate":{"condition":"positive","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1/2"]},"numerator":["1/2"],"range":{"first":"1","last":null}},"decision":"holds"},"statement":"the factor j - 1/2 gives k -> 1/(b + 1)_k with b(n) + 1 > 0","status":{"kind":"verified"}},{"evidence":"C_eff(n) = 1/4 > 0 for every integer n in [1, +inf) (exact; Taylor shift: the coefficients of C_eff(n) = 1/4 at n = 1 + u have one sign)","name":"scale_positive","sign_decision":{"certificate":{"condition":"positive","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1/4"]},"numerator":["1/4"],"range":{"first":"1","last":null}},"decision":"holds"},"statement":"C_eff(n) = C(n) (-1)^(complements) > 0 (the scaling x -> C_eff x)","status":{"kind":"verified"}},{"evidence":"U_0(n) = rho(n) U_0(n - 1) from U_0(1) = 1, the identity sum_r sigma_r(n) prod_(i < r) 1/rho(n - i) = f(n) holds exactly; rho(n) = 4 n - 6 > 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of rho(n) = 4 n - 6 at n = 2 + u have one sign)","name":"first_coefficient","sign_decision":{"certificate":{"condition":"positive","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["2","4"]},"numerator":["-6","4"],"range":{"first":"2","last":null}},"decision":"holds"},"statement":"the first coefficient U_0(n) is nonzero with one sign for every n from the induction seeds on (a hypergeometric solution U_0(n) = rho(n) U_0(n - 1) of its scalar recurrence with rho(n) > 0)","status":{"kind":"verified"}},{"evidence":"checked exactly","name":"earlier_rows","statement":"the rows P_1, ..., P_1 before the induction start are nonzero and real-rooted with every root in (-inf, 0)","status":{"kind":"verified"}}],"lean_declarations":["RealRooted.isPFMultiplierSequence_eval_of_roots_nonpos","RealRooted.isPFMultiplierSequence_inv_ascPochhammer","RealRooted.IsPFMultiplierSequence.mul","RealRooted.IsPFMultiplierSequence.diagonalOperator_isPF"],"lean_replay":"not_attempted","normal_form":"row relation p(n, k) [x^k] P_n + q(n, k) [x^(k-1)] P_n = 0, n >= 1, with p = (-4) (k - 1/2) (k), q = (-1) (k - n); valuation v(n) = 0, degree d(n) = n - 1","recurrence":{"first_index":1,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["8","8"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","16"]]},"deriv_order":2,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"reference":"Row-hypergeometric rows: an exact row relation p(n, k) [x^k] P_n + q(n, k) [x^(k-1)] P_n = 0, proved for every n by an invariant row-annihilator system of the rule, writes every row as U_0(n) x^v (or its reversal) times the image of (1 + x)^M(n) under a product of nonnegative multiplier sequences: C^k (C > 0); k -> M'!/(M' - k)!, whose exponential generating function is (1 + x)^M' (Polya--Schur, Theorem 7.1 (3) => (1) of P. Branden, Unimodality, log-concavity, real-rootedness and beyond, arXiv:1410.6601: a sequence is a multiplier sequence when G(x) = sum_k lambda_k x^k / k! or G(-x) can be written C x^m e^(a x) prod_k (1 + alpha_k x) with a >= 0, alpha_k >= 0); k -> phi(k) for a polynomial phi with only real roots, all <= 0 (Laguerre's theorem, RealRooted isPFMultiplierSequence_eval_of_roots_nonpos); k -> 1/(alpha)_k for alpha > 0 (RealRooted isPFMultiplierSequence_inv_ascPochhammer, via the generalized Laguerre polynomials); products of PF multiplier sequences are PF multiplier sequences (RealRooted IsPFMultiplierSequence.mul) and map real-rooted polynomials with nonnegative coefficients to such polynomials (IsPFMultiplierSequence.diagonalOperator_isPF)","schema":"polytool.recurrence-real-rootedness-theorem.v1","status":"proved","theorem":"hypergeometric_row"}}