{"kind":"theorem_check","report":{"conclusion":{"first_index":0,"root_region":{"upper":{"closed":false,"value":"0"}},"simple_roots":false,"statement":"every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0): for n >= 0 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) (j - n - 3) (j - n - 3) / ((j) (j + n + 2)), so sum_j U_j y^j is U_0(n) times the image of (1 + y)^(n + 2) under a nonnegative multiplier sequence, and U_0(n) != 0 for n >= 0 by its scalar recurrence"},"hypotheses":[{"evidence":"invariant system with 1 generator(s) from base 0 (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 + 2 >= 0 for every integer n in [0, +inf) (exact; Taylor shift: the coefficients of M(n) = n + 2 at n = 0 + u have one sign)","name":"base_size","sign_decision":{"certificate":{"condition":"nonnegative","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["2","1"]},"numerator":["2","1"],"range":{"first":"0","last":null}},"decision":"holds"},"statement":"the base factor j - n - 3 and the factor j give binom(M, j) with M(n) >= 0","status":{"kind":"verified"}},{"evidence":"M'(n) - M(n) = 0 >= 0 for every integer n in [0, +inf) (exact; Taylor shift: the coefficients of M'(n) - M(n) = 0 at n = 0 + u have one sign)","name":"complement_1","sign_decision":{"certificate":{"condition":"nonnegative","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":[]},"numerator":[],"range":{"first":"0","last":null}},"decision":"holds"},"statement":"the factor j - n - 3 gives k -> M'!/(M' - k)! with M'(n) >= M(n) (Polya--Schur)","status":{"kind":"verified"}},{"evidence":"b(n) + 1 = n + 3 > 0 for every integer n in [0, +inf) (exact; Taylor shift: the coefficients of b(n) + 1 = n + 3 at n = 0 + u have one sign)","name":"reciprocal_1","sign_decision":{"certificate":{"condition":"positive","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["3","1"]},"numerator":["3","1"],"range":{"first":"0","last":null}},"decision":"holds"},"statement":"the factor j + n + 2 gives k -> 1/(b + 1)_k with b(n) + 1 > 0","status":{"kind":"verified"}},{"evidence":"C_eff(n) = 1 > 0 for every integer n in [0, +inf) (exact; Taylor shift: the coefficients of C_eff(n) = 1 at n = 0 + 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":"0","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(0) = 6, the identity sum_r sigma_r(n) prod_(i < r) 1/rho(n - i) = f(n) holds exactly; rho(n) = (4 n + 6)/(n + 2) > 0 for every integer n in [1, +inf) (exact; Taylor shift: the coefficients of rho(n) = (4 n + 6)/(n + 2) at n = 1 + u have one sign)","name":"first_coefficient","sign_decision":{"certificate":{"condition":"positive","denominator":["2","1"],"method":{"kind":"taylor_shift","shifted_denominator":["3","1"],"shifted_numerator":["10","4"]},"numerator":["6","4"],"range":{"first":"1","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_0 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 >= 0, with p = (-1) (k) (k + n + 2), q = (1) (k - n - 3) (k - n - 3); valuation v(n) = 0, degree d(n) = n + 2","recurrence":{"first_index":0,"initial_polynomials":[["6","8","1"]],"recurrence":{"denominator":{"coeffs":[["12"],["14"],["4"]]},"terms":[{"coeff":{"coeffs":[["35","25"],["46","35"],["15","12"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["2","11","-13"],["1","7","-8"]]},"deriv_order":1,"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"}}