{"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]: for n >= 1 the coefficients U_j (U_j = [x^(j + v(n))] P_n, v(n) = n - 1) satisfy U_j = U_0(n) prod_(t <= j) R(n, t), R(n, j) = (-1) (j - 2) / ((j)), so sum_j U_j y^j is U_0(n) times the image of (1 + y)^(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":"induction on the rule: every term x^e D^d P_(n-r) has e - d - (1) r >= 0, and the rows before the rule start are checked exactly","name":"lower_support","statement":"[x^k] P_n = 0 for k < v(n), the valuation","status":{"kind":"verified"}},{"evidence":"M(n) = 1 >= 0 for every integer n in [1, +inf) (exact; Taylor shift: the coefficients of M(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":["1"]},"numerator":["1"],"range":{"first":"1","last":null}},"decision":"holds"},"statement":"the base factor j - 2 and the factor j give binom(M, j) with M(n) >= 0","status":{"kind":"verified"}},{"evidence":"C_eff(n) = 1 > 0 for every integer n in [1, +inf) (exact; Taylor shift: the coefficients of C_eff(n) = 1 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"]},"numerator":["1"],"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) = 1 > 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of rho(n) = 1 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":["1"]},"numerator":["1"],"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_0, ..., 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 = (-1) (k - n + 1), q = (-1) (k - n - 1); valuation v(n) = n - 1, degree d(n) = n","recurrence":{"first_index":0,"initial_polynomials":[["1"],["1","1"]],"recurrence":{"denominator":{"coeffs":[["-1"],["1"]]},"terms":[{"coeff":{"coeffs":[["0","-1"],["0","1"]]},"deriv_order":0,"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"}}