{"chains":[{"edge":{"id":"e-85a3ed719eb2b15f","operation":{"map":"A013609","operation":"basis_map"},"operation_detail":"A013609","conclusion_id":"n-e14fba9d75956da0","premise_count":1,"theorem":"geometric family P_k = g(t) (a + d t)^k: T(p) = g(t) p(a + d t), so the roots of T(p) are those of g and the points (r - a)/d for the roots r of p (elementary)","lean_route":null,"lean_declarations":[],"certificate_hash":"5f4f6426f38114262d118f207f1982df2c214dd55bc4a1a8815537422fe5a166","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-8a65e165240c40e0","role":"sequence","name":"Triangular array of generalized Narayana numbers T(n,k) = 2*binomial(n+1,k)* binomial(n-2,k-1)/(n+1) for n >= 1 and 0 <= k <= n-1, read by rows.","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-8a65e165240c40e0","role":"sequence","name":"Triangular array of generalized Narayana numbers T(n,k) = 2*binomial(n+1,k)* binomial(n-2,k-1)/(n+1) for n >= 1 and 0 <= k <= n-1, read by rows.","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 0]"},"chains":[{"edge":{"id":"e-6f94bd2ed3daf65b","operation":{"operation":"theorem_check","theorem":"hypergeometric_row"},"operation_detail":"hypergeometric_row","conclusion_id":"n-8a65e165240c40e0","premise_count":0,"theorem":"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)","lean_route":null,"lean_declarations":["RealRooted.isPFMultiplierSequence_eval_of_roots_nonpos","RealRooted.isPFMultiplierSequence_inv_ascPochhammer","RealRooted.IsPFMultiplierSequence.mul","RealRooted.IsPFMultiplierSequence.diagonalOperator_isPF"],"certificate_hash":"f9cd8cab2644b68250c8ffbe5bc251ac87e0d25d5ed5c71c2aa1126340938e1f","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}}],"premises":[]},"premises":[]},{"edge":{"id":"e-deeee4aa3e096f87","operation":{"operation":"theorem_check","theorem":"liu_wang_three_term"},"operation_detail":"liu_wang_three_term","conclusion_id":"n-8a65e165240c40e0","premise_count":0,"theorem":"L. L. Liu and Y. Wang, Adv. Appl. Math. 38 (2007) 542-560, Theorem 2.1 and Corollary 2.4 (A unified approach to polynomial sequences with only real zeros; the lag row as the interlacer, b_n = 0), weak interlacing of consecutive rows, with nonnegativity of the coefficients replaced, where a root region is certified, by an exact root-location induction; Proposition 3.3 (the case B_n(x) = -(c_n x + d_n)^2)","lean_route":"sign","lean_declarations":["RealRooted.threeTerm_interlaces_of_eval_nonpos","RealRooted.threeTerm_interlaces","RealRooted.eval_nonpos_of_natDegree_le_two"],"certificate_hash":"85545cdd99cfe479591037681844e58bbf75377d2a13e43b5c3af8967209ff35","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"premises":[]}]}]}],"truncated":false,"expanded":3}