{"chains":[{"edge":{"id":"e-95c30c4879aff589","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"euler_polynomial\",\"coefficients\":[{\"numerator\":[\"1\"],\"denominator\":[\"1\"]},{\"numerator\":[\"1\"],\"denominator\":[\"1\"]}]}"},"operation_detail":"euler_polynomial, shift 0","conclusion_id":"n-240137c7d3aa3ef6","premise_count":1,"theorem":"Laguerre's theorem on multiplier sequences: if f is a real polynomial whose roots are all real and <= 0, then (f(k))_(k >= 0) is a multiplier sequence, so x^k -> f(k) x^k maps every real-rooted polynomial to a real-rooted polynomial or zero (Laguerre; see T. Craven and G. Csordas, Multiplier sequences for fields, Illinois J. Math. 21 (1977); Polya--Schur, Theorem 40 of P. Branden, arXiv:1410.6601: sum_k f(k) x^k / k! = f(theta) e^x = C e^x x^m prod (1 + x/a_j), a_j > 0); f(k) has one sign for k >= 0, so coefficients of one sign stay of one sign; applied to f(n, .) for each n","lean_route":null,"lean_declarations":["RealRooted.isMultiplierSequence_eval_of_roots_nonpos","RealRooted.isPFMultiplierSequence_eval_of_roots_nonpos","RealRooted.isMultiplierSequence_iff_preserves"],"certificate_hash":"09cd2983353755f46c446abc5285b110b514f6aead948ab420d22d00667a4c3b","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-47fe395e9f7d5f86","role":"sequence","name":"T(n,k) is the number of partial bijections of height k (height(alpha) = |Im(alpha)|) of an n-element set.","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-47fe395e9f7d5f86","role":"sequence","name":"T(n,k) is the number of partial bijections of height k (height(alpha) = |Im(alpha)|) of an n-element set.","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-4ffbad239f6cd570","operation":{"operation":"theorem_check","theorem":"hypergeometric_row"},"operation_detail":"hypergeometric_row","conclusion_id":"n-47fe395e9f7d5f86","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":"8365b79368eba3a4958f63a42e5f877b7c5285f6c88d84cb4be10e19896cde78","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":false,"value":"0"}}}],"premises":[]},"premises":[]},{"edge":{"id":"e-c98efb5092e3dc49","operation":{"operation":"theorem_check","theorem":"liu_wang"},"operation_detail":"liu_wang","conclusion_id":"n-47fe395e9f7d5f86","premise_count":0,"theorem":"L. L. Liu and Y. Wang, A unified approach to polynomial sequences with only real zeros, Adv. in Appl. Math. 38 (2007) 542-560, Theorem 2.1 with g = f' (as in their Corollary 2.4), with nonnegativity of the coefficients replaced by an exact induction keeping every root in (-inf, 0)","lean_route":null,"lean_declarations":[],"certificate_hash":"9bdc3e17255514f18037338a007600b7db493f3902d6fef1feba9e25c9cb40a3","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":false,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"premises":[]},{"edge":{"id":"e-6c3e82dc47b23e3d","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"reversal\",\"schedule\":{\"first_index\":0,\"first_degree\":0,\"step\":1}}"},"operation_detail":"reversal, shift 0","conclusion_id":"n-47fe395e9f7d5f86","premise_count":1,"theorem":"a real affine substitution x -> a x + b (a != 0), the reversal x^d p(1/x) (d >= deg p) and a real Mobius map (c x + e)^d p((a x + b)/(c x + e)) (a e - b c != 0, d >= deg p) map real roots to real roots: a root r of p gives the root (r - b)/a, 1/r (and 0) or (e r - b)/(a - c r) (and -e/c); for an input row that is a polynomial the degree condition holds automatically","lean_route":"reversed","lean_declarations":["RealRooted.X_pow_mul_reverse_eq_zero_or_splits","RealRooted.reflect_eq_zero_or_splits"],"certificate_hash":"700562a4bb1ca0dbd418871d0b06c1d91d7ddff135fb4302bc27cce15f7d4b9f","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}}],"premises":[{"position":0,"node_id":"n-8ab17db79dad1880","role":"sequence","name":"basis_map_A008277 of Triangle of unsigned Stirling numbers of the first kind (see A048994), read by rows, T(n,k) for 0 <= k <= n.","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-8ab17db79dad1880","role":"sequence","name":"basis_map_A008277 of Triangle of unsigned Stirling numbers of the first kind (see A048994), read by rows, T(n,k) for 0 <= k <= n.","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-07cfebc08bea7e3c","operation":{"map":"A008277","operation":"basis_map"},"operation_detail":"A008277","conclusion_id":"n-8ab17db79dad1880","premise_count":1,"theorem":"ray basis maps: for L f = (a + b t) f + kappa (t - h) f', b > 0, kappa >= 0, and g real-rooted with every root <= h, of multiplicity m at h, T(u^k) = L^k g sends every real polynomial with all roots in S to one with all roots in (-inf, h] if and only if S lies in (-inf, a + b h + kappa m] (RealRooted rayBasisMap_maps_realRootedIn_iff; the step is Ma and Wang, EJC 15 (2008) R17, Theorem 2)","lean_route":null,"lean_declarations":[],"certificate_hash":"999e677ad505bf2794061323bd8891475f40627a33629f943089e8d34c39e30f","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}}],"premises":[{"position":0,"node_id":"n-b9fbfb57d9269e2f","role":"sequence","name":"Triangle of unsigned Stirling numbers of the first kind (see A048994), read by rows, T(n,k) for 0 <= k <= n.","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-b9fbfb57d9269e2f","role":"sequence","name":"Triangle of unsigned Stirling numbers of the first kind (see A048994), read by rows, T(n,k) for 0 <= k <= n.","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-7f9dd568d5b3e61f","operation":{"operation":"parent_provers","route":"root_domain"},"operation_detail":"root_domain","conclusion_id":"n-b9fbfb57d9269e2f","premise_count":0,"theorem":"polytool parent provers, route root_domain: every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign","lean_route":null,"lean_declarations":[],"certificate_hash":"7459521a370fd56c834165b8deac52b69ae7b4616aad32986bdce813b2fc790c","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-c0f6eea676fe915a","operation":{"operation":"theorem_check","theorem":"iterated_preserver"},"operation_detail":"iterated_preserver","conclusion_id":"n-b9fbfb57d9269e2f","premise_count":0,"theorem":"Iterated real-rootedness preservers (induction on n): if P_m is nonzero and real-rooted with every root in a closed region R and, for every n > m, P_n = a_n(x) S_n(P_(n-1)) where S_n maps every polynomial that is zero or real-rooted with every root in R to zero or a real-rooted polynomial with every root in R and a_n is real-rooted with every root in R, then every P_n is real-rooted with every root in R (the roots of a product are the roots of its factors); an exact degree step keeps every row nonzero; here S_n is the identity","lean_route":null,"lean_declarations":[],"certificate_hash":"a82705a256da9a31e79dad90e8bb85c35e6f480677669742e9957b3f2d305b48","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":[]},{"edge":{"id":"e-edbf92ee2e446027","operation":{"operation":"parent_provers","route":"root_domain"},"operation_detail":"root_domain","conclusion_id":"n-b9fbfb57d9269e2f","premise_count":0,"theorem":"polytool parent provers, route root_domain: every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign","lean_route":null,"lean_declarations":[],"certificate_hash":"e6cded2063c0080a1f0908b55722412ab5ecc8b8410962a8b595888547fca67c","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-5e8a129593745142","operation":{"map":"A008277","operation":"basis_map"},"operation_detail":"A008277","conclusion_id":"n-8ab17db79dad1880","premise_count":1,"theorem":"ray basis maps: for L f = (a + b t) f + kappa (t - h) f', b > 0, kappa >= 0, and g real-rooted with every root <= h, of multiplicity m at h, T(u^k) = L^k g sends every real polynomial with all roots in S to one with all roots in (-inf, h] if and only if S lies in (-inf, a + b h + kappa m] (RealRooted rayBasisMap_maps_realRootedIn_iff; the step is Ma and Wang, EJC 15 (2008) R17, Theorem 2)","lean_route":null,"lean_declarations":[],"certificate_hash":"6a4b9bcb999cb25fc02a98aa89bef5accc1f7078776a376992d23ea0caa0b902","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}}],"premises":[{"position":0,"node_id":"n-b9fbfb57d9269e2f","role":"sequence","name":"Triangle of unsigned Stirling numbers of the first kind (see A048994), read by rows, T(n,k) for 0 <= k <= n.","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-b9fbfb57d9269e2f","role":"sequence","name":"Triangle of unsigned Stirling numbers of the first kind (see A048994), read by rows, T(n,k) for 0 <= k <= n.","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-7f9dd568d5b3e61f","operation":{"operation":"parent_provers","route":"root_domain"},"operation_detail":"root_domain","conclusion_id":"n-b9fbfb57d9269e2f","premise_count":0,"theorem":"polytool parent provers, route root_domain: every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign","lean_route":null,"lean_declarations":[],"certificate_hash":"7459521a370fd56c834165b8deac52b69ae7b4616aad32986bdce813b2fc790c","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}}],"premises":[]},"repeat":true,"premises":[]},{"edge":{"id":"e-c0f6eea676fe915a","operation":{"operation":"theorem_check","theorem":"iterated_preserver"},"operation_detail":"iterated_preserver","conclusion_id":"n-b9fbfb57d9269e2f","premise_count":0,"theorem":"Iterated real-rootedness preservers (induction on n): if P_m is nonzero and real-rooted with every root in a closed region R and, for every n > m, P_n = a_n(x) S_n(P_(n-1)) where S_n maps every polynomial that is zero or real-rooted with every root in R to zero or a real-rooted polynomial with every root in R and a_n is real-rooted with every root in R, then every P_n is real-rooted with every root in R (the roots of a product are the roots of its factors); an exact degree step keeps every row nonzero; here S_n is the identity","lean_route":null,"lean_declarations":[],"certificate_hash":"a82705a256da9a31e79dad90e8bb85c35e6f480677669742e9957b3f2d305b48","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":[]},"repeat":true,"premises":[]},{"edge":{"id":"e-edbf92ee2e446027","operation":{"operation":"parent_provers","route":"root_domain"},"operation_detail":"root_domain","conclusion_id":"n-b9fbfb57d9269e2f","premise_count":0,"theorem":"polytool parent provers, route root_domain: every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign","lean_route":null,"lean_declarations":[],"certificate_hash":"e6cded2063c0080a1f0908b55722412ab5ecc8b8410962a8b595888547fca67c","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}}],"premises":[]},"repeat":true,"premises":[]}]}]},{"edge":{"id":"e-98ed2204a3519c03","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"reversal\",\"schedule\":{\"first_index\":0,\"first_degree\":0,\"step\":1}}"},"operation_detail":"reversal, shift 0","conclusion_id":"n-8ab17db79dad1880","premise_count":1,"theorem":"a real affine substitution x -> a x + b (a != 0), the reversal x^d p(1/x) (d >= deg p) and a real Mobius map (c x + e)^d p((a x + b)/(c x + e)) (a e - b c != 0, d >= deg p) map real roots to real roots: a root r of p gives the root (r - b)/a, 1/r (and 0) or (e r - b)/(a - c r) (and -e/c); for an input row that is a polynomial the degree condition holds automatically","lean_route":"reversed","lean_declarations":["RealRooted.X_pow_mul_reverse_eq_zero_or_splits","RealRooted.reflect_eq_zero_or_splits"],"certificate_hash":"97f5493573503bf56ab3bd3935e75017c99d5a7cd43986e71275d58e4ad12a9c","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}}],"premises":[{"position":0,"node_id":"n-47fe395e9f7d5f86","role":"sequence","name":"T(n,k) is the number of partial bijections of height k (height(alpha) = |Im(alpha)|) of an n-element set.","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-47fe395e9f7d5f86","role":"sequence","name":"T(n,k) is the number of partial bijections of height k (height(alpha) = |Im(alpha)|) of an n-element set.","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-4ffbad239f6cd570","operation":{"operation":"theorem_check","theorem":"hypergeometric_row"},"operation_detail":"hypergeometric_row","conclusion_id":"n-47fe395e9f7d5f86","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":"8365b79368eba3a4958f63a42e5f877b7c5285f6c88d84cb4be10e19896cde78","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":false,"value":"0"}}}],"premises":[]},"repeat":true,"premises":[]},{"edge":{"id":"e-c98efb5092e3dc49","operation":{"operation":"theorem_check","theorem":"liu_wang"},"operation_detail":"liu_wang","conclusion_id":"n-47fe395e9f7d5f86","premise_count":0,"theorem":"L. L. Liu and Y. Wang, A unified approach to polynomial sequences with only real zeros, Adv. in Appl. Math. 38 (2007) 542-560, Theorem 2.1 with g = f' (as in their Corollary 2.4), with nonnegativity of the coefficients replaced by an exact induction keeping every root in (-inf, 0)","lean_route":null,"lean_declarations":[],"certificate_hash":"9bdc3e17255514f18037338a007600b7db493f3902d6fef1feba9e25c9cb40a3","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":false,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]},{"edge":{"id":"e-bef9620f9d798d0f","operation":{"operation":"theorem_check","theorem":"iterated_preserver"},"operation_detail":"iterated_preserver","conclusion_id":"n-47fe395e9f7d5f86","premise_count":0,"theorem":"Iterated real-rootedness preservers (induction on n): if P_m is nonzero and real-rooted with every root in a closed region R and, for every n > m, P_n = a_n(x) S_n(P_(n-1)) where S_n maps every polynomial that is zero or real-rooted with every root in R to zero or a real-rooted polynomial with every root in R and a_n is real-rooted with every root in R, then every P_n is real-rooted with every root in R (the roots of a product are the roots of its factors); an exact degree step keeps every row nonzero; S_n = A + B D + C D^2 with A = n + x, B = x, C = 0: Branden's Weyl step: T = A + B D + C D^2 maps every real-rooted polynomial to a real-rooted polynomial when (i) B^2 - 4 A C >= 0 on the real line, (ii) A strictly interlaces B (deg B = deg A + 1) or strictly alternates left of B (deg B = deg A), with leading coefficients of the same sign when deg A >= 1, and (iii) T(x^k) has degree deg A + k with leading coefficients of one sign for every k >= 0 (P. Branden, Linear transformations preserving the Polya frequency property, Trans. Amer. Math. Soc. 358 (2006), Corollary 3.5); (i) is necessary for a real-rootedness preserver (J. Borcea and P. Branden, Proc. London Math. Soc. 101 (2010), Theorem 1.3); with coefficients of one sign T also keeps every root in (-inf, 0]; the induction runs on the rows Q_n = x^(d_n) P_n(1/x) at the nominal degree d_n, with d_(n-L) = n - 1 (an upper bound of deg P_(n-L)) (exact coordinate change of the rule; the rows P_n have every root in (-inf, 0] when the rows Q_n have every root in (-inf, 0])","lean_route":null,"lean_declarations":[],"certificate_hash":"636ba4353f9dca36252959c20440ce0982176027bf83370394c8c906d2cf260e","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-bef9620f9d798d0f","operation":{"operation":"theorem_check","theorem":"iterated_preserver"},"operation_detail":"iterated_preserver","conclusion_id":"n-47fe395e9f7d5f86","premise_count":0,"theorem":"Iterated real-rootedness preservers (induction on n): if P_m is nonzero and real-rooted with every root in a closed region R and, for every n > m, P_n = a_n(x) S_n(P_(n-1)) where S_n maps every polynomial that is zero or real-rooted with every root in R to zero or a real-rooted polynomial with every root in R and a_n is real-rooted with every root in R, then every P_n is real-rooted with every root in R (the roots of a product are the roots of its factors); an exact degree step keeps every row nonzero; S_n = A + B D + C D^2 with A = n + x, B = x, C = 0: Branden's Weyl step: T = A + B D + C D^2 maps every real-rooted polynomial to a real-rooted polynomial when (i) B^2 - 4 A C >= 0 on the real line, (ii) A strictly interlaces B (deg B = deg A + 1) or strictly alternates left of B (deg B = deg A), with leading coefficients of the same sign when deg A >= 1, and (iii) T(x^k) has degree deg A + k with leading coefficients of one sign for every k >= 0 (P. Branden, Linear transformations preserving the Polya frequency property, Trans. Amer. Math. Soc. 358 (2006), Corollary 3.5); (i) is necessary for a real-rootedness preserver (J. Borcea and P. Branden, Proc. London Math. Soc. 101 (2010), Theorem 1.3); with coefficients of one sign T also keeps every root in (-inf, 0]; the induction runs on the rows Q_n = x^(d_n) P_n(1/x) at the nominal degree d_n, with d_(n-L) = n - 1 (an upper bound of deg P_(n-L)) (exact coordinate change of the rule; the rows P_n have every root in (-inf, 0] when the rows Q_n have every root in (-inf, 0])","lean_route":null,"lean_declarations":[],"certificate_hash":"636ba4353f9dca36252959c20440ce0982176027bf83370394c8c906d2cf260e","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}}],"premises":[]},"repeat":true,"premises":[]}]}]}],"truncated":false,"expanded":11}