{"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^(d(n) - j)] P_n, d(n) = n) satisfy U_j = U_0(n) prod_(t <= j) R(n, t), R(n, j) = (-1) (j + 2 n) (j - n - 1) / ((j + n) (j)), so sum_j U_j y^j is U_0(n) times the image of (1 + y)^(n) 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":"d(n) = n","name":"upper_support_factor","statement":"q(n, k) has the factor k - d(n) - 1","status":{"kind":"verified"}},{"evidence":"c_p(n) = 1/2 != 0 for every integer n in [0, +inf) (exact; Taylor shift: the coefficients of c_p(n) = 1/2 at n = 0 + u have one sign)","name":"upper_support_scalar","sign_decision":{"certificate":{"condition":"nonzero","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1/2"]},"numerator":["1/2"],"range":{"first":"0","last":null}},"decision":"holds"},"statement":"c_p(n) != 0, the scalar factor of p","status":{"kind":"verified"}},{"evidence":"u(n) + D(n) = -n - 1 < 0 for every integer n in [0, +inf) (exact; Taylor shift: the coefficients of u(n) + D(n) = -n - 1 at n = 0 + u have one sign)","name":"upper_support_root_0","sign_decision":{"certificate":{"condition":"negative","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["-1","-1"]},"numerator":["-1","-1"],"range":{"first":"0","last":null}},"decision":"holds"},"statement":"u(n) + D(n) < 0 for the degree bound D(n) = 2 n of the rule (deg P_n <= D(n) by induction: D(n) >= e - d + D(n - r) for every term x^e D^d P_(n-r), the rows before checked exactly), so the root -u(n) of p lies above every degree and p(n, k) != 0 for d(n) < k <= D(n)","status":{"kind":"verified"}},{"evidence":"u(n) + d(n) + 1 = n + 1 > 0 for every integer n in [0, +inf) (exact; Taylor shift: the coefficients of u(n) + d(n) + 1 = n + 1 at n = 0 + u have one sign)","name":"upper_support_root_1","sign_decision":{"certificate":{"condition":"positive","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1","1"]},"numerator":["1","1"],"range":{"first":"0","last":null}},"decision":"holds"},"statement":"u(n) + d(n) + 1 > 0, so p(n, k) != 0 for every integer k > d(n) and [x^k] P_n = 0 there","status":{"kind":"verified"}},{"evidence":"M(n) = n >= 0 for every integer n in [0, +inf) (exact; Taylor shift: the coefficients of M(n) = n 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":["0","1"]},"numerator":["0","1"],"range":{"first":"0","last":null}},"decision":"holds"},"statement":"the base factor j - n - 1 and the factor j give binom(M, j) with M(n) >= 0","status":{"kind":"verified"}},{"evidence":"d(n) - v - M(n) = 0 >= 0 for every integer n in [0, +inf) (exact; Taylor shift: the coefficients of d(n) - v - M(n) = 0 at n = 0 + u have one sign)","name":"base_within_degree","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":"M(n) <= d(n) - v (reversal at the degree)","status":{"kind":"verified"}},{"evidence":"a(n) - b(n) = n >= 0 for every integer n in [0, +inf) (exact; Taylor shift: the coefficients of a(n) - b(n) = n at n = 0 + u have one sign)","name":"pair_0_0_length","sign_decision":{"certificate":{"condition":"nonnegative","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["0","1"]},"numerator":["0","1"],"range":{"first":"0","last":null}},"decision":"holds"},"statement":"(j + 2 n) / (j + n) pairs to the polynomial (k + b + 1) ... (k + a): a - b is an integer >= 0 (Laguerre)","status":{"kind":"verified"}},{"evidence":"b(n) + 1 = n + 1 > 0 for every integer n in [0, +inf) (exact; Taylor shift: the coefficients of b(n) + 1 = n + 1 at n = 0 + u have one sign)","name":"pair_0_0_roots","sign_decision":{"certificate":{"condition":"positive","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1","1"]},"numerator":["1","1"],"range":{"first":"0","last":null}},"decision":"holds"},"statement":"b(n) + 1 > 0: every root of the paired polynomial is negative","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) = 1, the identity sum_r sigma_r(n) prod_(i < r) 1/rho(n - i) = f(n) holds exactly; rho(n) = (4 n - 2)/(n) > 0 for every integer n in [1, +inf) (exact; Taylor shift: the coefficients of rho(n) = (4 n - 2)/(n) at n = 1 + u have one sign)","name":"first_coefficient","sign_decision":{"certificate":{"condition":"positive","denominator":["0","1"],"method":{"kind":"taylor_shift","shifted_denominator":["1","1"],"shifted_numerator":["2","4"]},"numerator":["-2","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/2) (k - 3 n - 1) (k), q = (1/2) (k - 2 n - 1) (k - n - 1); valuation v(n) = 0, degree d(n) = n","recurrence":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"denominator":{"coeffs":[["0"],["-2"],["4"]]},"terms":[{"coeff":{"coeffs":[["6","6","0"],["-27","-26","-1"],["27","24","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","3","3","0"],["0","-9","-10","-1"]]},"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"}}