{"chains":[{"edge":{"id":"e-bef7d6eb81d01d29","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-1b9a6f7f2a208e06","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":"a6c58860ebb50f454c403706a2d1147549ad0e0a0cc3fe484c50495937589e25","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-0efca9aef0911045","role":"sequence","name":"veronese_section_2_1 of A natural number operator.","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-0efca9aef0911045","role":"sequence","name":"veronese_section_2_1 of A natural number operator.","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-611716aca3d048f2","operation":{"index_shift":0,"modulus":2,"operation":"veronese_section","residue":1},"operation_detail":"r=2, j=1, shift 0","conclusion_id":"n-0efca9aef0911045","premise_count":1,"theorem":"Veronese sections of Polya frequency sequences (Aissen--Schoenberg--Whitney--Edrei): if P is real-rooted with coefficients of one sign, equivalently nonzero with all roots in (-inf, 0], every section V_(r,j)(P) is zero or real-rooted with roots in (-inf, 0]","lean_route":null,"lean_declarations":[],"certificate_hash":"54bbc3870a9bab1480e77df315db981e54b42c8e0e884330603e7b983939b722","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-f4c1dee76f5a68b2","role":"sequence","name":"A natural number operator.","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-f4c1dee76f5a68b2","role":"sequence","name":"A natural number operator.","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-3fa49e62bb44b5e9","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"derivative_polynomial\",\"coefficients\":[{\"numerator\":[\"1\",\"2\"],\"denominator\":[\"1\"]},{\"numerator\":[\"2\"],\"denominator\":[\"1\"]}]}"},"operation_detail":"derivative_polynomial, shift 0","conclusion_id":"n-f4c1dee76f5a68b2","premise_count":1,"theorem":"Laguerre's theorem on differential operators: if phi is a real polynomial with only real roots, then phi(D) maps every real-rooted polynomial to a real-rooted polynomial or zero (write phi(D) = C D^j prod (1 + c_i D); D preserves real-rootedness by Rolle's theorem and p + c p' is real-rooted for every real c by Rolle's theorem applied to e^(x/c) p; Polya--Schur 1914); when the coefficients of phi have one sign, coefficients of one sign stay of one sign; applied to phi(n, .) for each n","lean_route":null,"lean_declarations":["RealRooted.splits_add_C_mul_derivative_all","RealRooted.splits_C_mul_add_derivative","Polynomial.Splits.derivative"],"certificate_hash":"4b4b993bacdbfba3402e6d1e91fbdba1bb2ecb2193958d2cb51bcf416991f067","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-6fea5aff4f44fa54","role":"sequence","name":"a(n) = 1 if n is of the form m(m+3)/2, otherwise 0.","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-6fea5aff4f44fa54","role":"sequence","name":"a(n) = 1 if n is of the form m(m+3)/2, otherwise 0.","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-06e4036009691da2","operation":{"operation":"theorem_check","theorem":"iterated_preserver"},"operation_detail":"iterated_preserver","conclusion_id":"n-6fea5aff4f44fa54","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":"7c912ab923c9452960fd948e2fd8c52d90d69cab55f4c9bc2b8f8cdc969cc005","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-292206ad4ae86d2d","operation":{"index_shift":0,"modulus":2,"operation":"veronese_section","residue":0},"operation_detail":"r=2, j=0, shift 0","conclusion_id":"n-6fea5aff4f44fa54","premise_count":1,"theorem":"Veronese sections of Polya frequency sequences (Aissen--Schoenberg--Whitney--Edrei): if P is real-rooted with coefficients of one sign, equivalently nonzero with all roots in (-inf, 0], every section V_(r,j)(P) is zero or real-rooted with roots in (-inf, 0]","lean_route":null,"lean_declarations":[],"certificate_hash":"c465820f18c46c973a857042716eb1aaf6aa6c14f8138fb65e09d43ac3468670","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-cdb0db4ad473ee28","role":"sequence","name":"basis-map coefficients of Irregular triangle read by rows formed by taking every other row of the Delannoy array (A008288) regarded as a triangle. shifted by x -> -x + 0","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-cdb0db4ad473ee28","role":"sequence","name":"basis-map coefficients of Irregular triangle read by rows formed by taking every other row of the Delannoy array (A008288) regarded as a triangle. shifted by x -> -x + 0","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-1991a148b9538b93","operation":{"operation":"parent_provers","route":"periodic_product"},"operation_detail":"periodic_product","conclusion_id":"n-cdb0db4ad473ee28","premise_count":0,"theorem":"polytool parent provers, route periodic_product: every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign","lean_route":null,"lean_declarations":[],"certificate_hash":"8cf856a836985e96bd407ce4af801578ea18373bd96c64891a6ad18f0bd7c29e","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-51515ec3828e72c6","operation":{"operation":"theorem_check","theorem":"iterated_preserver"},"operation_detail":"iterated_preserver","conclusion_id":"n-cdb0db4ad473ee28","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":"c7e3b02e1174428d487f2e94194926b23d9ebc09b1aa07ae72bbf115162aed16","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-12303ad0e0b9f8eb","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"mobius\",\"a\":\"1\",\"b\":\"0\",\"c\":\"1\",\"e\":\"1\",\"schedule\":{\"first_index\":0,\"first_degree\":0,\"step\":2}}"},"operation_detail":"mobius, shift 0","conclusion_id":"n-cdb0db4ad473ee28","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":"fTransform","lean_declarations":["RealRooted.splits_fPolynomial"],"certificate_hash":"dd20f68543ec96b80fc61a9099ece7e9f6f16d4d392531db688c5b0c3cd77272","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":true,"value":"-1"},"upper":{"closed":true,"value":"0"}}}],"premises":[{"position":0,"node_id":"n-cdb0db4ad473ee28","role":"sequence","name":"basis-map coefficients of Irregular triangle read by rows formed by taking every other row of the Delannoy array (A008288) regarded as a triangle. shifted by x -> -x + 0","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-cdb0db4ad473ee28","role":"sequence","name":"basis-map coefficients of Irregular triangle read by rows formed by taking every other row of the Delannoy array (A008288) regarded as a triangle. shifted by x -> -x + 0","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-1991a148b9538b93","operation":{"operation":"parent_provers","route":"periodic_product"},"operation_detail":"periodic_product","conclusion_id":"n-cdb0db4ad473ee28","premise_count":0,"theorem":"polytool parent provers, route periodic_product: every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign","lean_route":null,"lean_declarations":[],"certificate_hash":"8cf856a836985e96bd407ce4af801578ea18373bd96c64891a6ad18f0bd7c29e","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-51515ec3828e72c6","operation":{"operation":"theorem_check","theorem":"iterated_preserver"},"operation_detail":"iterated_preserver","conclusion_id":"n-cdb0db4ad473ee28","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":"c7e3b02e1174428d487f2e94194926b23d9ebc09b1aa07ae72bbf115162aed16","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-b7eca039219a7f53","operation":{"operation":"parent_provers","route":"periodic_product"},"operation_detail":"periodic_product","conclusion_id":"n-6fea5aff4f44fa54","premise_count":0,"theorem":"polytool parent provers, route periodic_product: every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign","lean_route":null,"lean_declarations":[],"certificate_hash":"28b0677de51356622004bdee49b3e32263cbcbf0992e57af7cdf296451825f68","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-7e44b66e04c497d6","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"mobius\",\"a\":\"1\",\"b\":\"0\",\"c\":\"1\",\"e\":\"1\",\"schedule\":{\"first_index\":0,\"first_degree\":0,\"step\":1}}"},"operation_detail":"mobius, shift 0","conclusion_id":"n-6fea5aff4f44fa54","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":"fTransform","lean_declarations":["RealRooted.splits_fPolynomial"],"certificate_hash":"29fd5ce083ab0ea9777d2838738405a218d7a71aee67f7d82621aeb4d52fb9a1","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":true,"value":"-1"},"upper":{"closed":true,"value":"0"}}}],"premises":[{"position":0,"node_id":"n-6fea5aff4f44fa54","role":"sequence","name":"a(n) = 1 if n is of the form m(m+3)/2, otherwise 0.","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-6fea5aff4f44fa54","role":"sequence","name":"a(n) = 1 if n is of the form m(m+3)/2, otherwise 0.","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-06e4036009691da2","operation":{"operation":"theorem_check","theorem":"iterated_preserver"},"operation_detail":"iterated_preserver","conclusion_id":"n-6fea5aff4f44fa54","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":"7c912ab923c9452960fd948e2fd8c52d90d69cab55f4c9bc2b8f8cdc969cc005","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-292206ad4ae86d2d","operation":{"index_shift":0,"modulus":2,"operation":"veronese_section","residue":0},"operation_detail":"r=2, j=0, shift 0","conclusion_id":"n-6fea5aff4f44fa54","premise_count":1,"theorem":"Veronese sections of Polya frequency sequences (Aissen--Schoenberg--Whitney--Edrei): if P is real-rooted with coefficients of one sign, equivalently nonzero with all roots in (-inf, 0], every section V_(r,j)(P) is zero or real-rooted with roots in (-inf, 0]","lean_route":null,"lean_declarations":[],"certificate_hash":"c465820f18c46c973a857042716eb1aaf6aa6c14f8138fb65e09d43ac3468670","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-cdb0db4ad473ee28","role":"sequence","name":"basis-map coefficients of Irregular triangle read by rows formed by taking every other row of the Delannoy array (A008288) regarded as a triangle. shifted by x -> -x + 0","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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-b7eca039219a7f53","operation":{"operation":"parent_provers","route":"periodic_product"},"operation_detail":"periodic_product","conclusion_id":"n-6fea5aff4f44fa54","premise_count":0,"theorem":"polytool parent provers, route periodic_product: every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign","lean_route":null,"lean_declarations":[],"certificate_hash":"28b0677de51356622004bdee49b3e32263cbcbf0992e57af7cdf296451825f68","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-f4214b1b9dbd784c","operation":{"operation":"theorem_check","theorem":"liu_wang_three_term"},"operation_detail":"liu_wang_three_term","conclusion_id":"n-f4c1dee76f5a68b2","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","lean_route":null,"lean_declarations":["RealRooted.MaWang.strictInterl_of_interlaces_evalCoeff_nonpos"],"certificate_hash":"253f3befb8cf4d8ee832df5b715879d3d85c59775cccd4e5a3da38dad5e2aa68","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-7c3f493b81ba2cb3","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"mobius\",\"a\":\"1\",\"b\":\"0\",\"c\":\"1\",\"e\":\"1\",\"schedule\":{\"first_index\":0,\"first_degree\":0,\"step\":1}}"},"operation_detail":"mobius, shift 0","conclusion_id":"n-f4c1dee76f5a68b2","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":"fTransform","lean_declarations":["RealRooted.splits_fPolynomial"],"certificate_hash":"7765934752f29369985835b4d83b641e4b8fb7457121b8a97a7a6d51bbb31c0a","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":true,"value":"-1"},"upper":{"closed":true,"value":"0"}}}],"premises":[{"position":0,"node_id":"n-66d5ecabca128038","role":"sequence","name":"Triangle read by rows, (n-1) zeros followed by (2n, 1).","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-66d5ecabca128038","role":"sequence","name":"Triangle read by rows, (n-1) zeros followed by (2n, 1).","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-224384a428b81acf","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"derivative_polynomial\",\"coefficients\":[{\"numerator\":[\"1\"],\"denominator\":[\"1\"]},{\"numerator\":[\"2\"],\"denominator\":[\"1\"]}]}"},"operation_detail":"derivative_polynomial, shift 0","conclusion_id":"n-66d5ecabca128038","premise_count":1,"theorem":"Laguerre's theorem on differential operators: if phi is a real polynomial with only real roots, then phi(D) maps every real-rooted polynomial to a real-rooted polynomial or zero (write phi(D) = C D^j prod (1 + c_i D); D preserves real-rootedness by Rolle's theorem and p + c p' is real-rooted for every real c by Rolle's theorem applied to e^(x/c) p; Polya--Schur 1914); when the coefficients of phi have one sign, coefficients of one sign stay of one sign; applied to phi(n, .) for each n","lean_route":null,"lean_declarations":["RealRooted.splits_add_C_mul_derivative_all","RealRooted.splits_C_mul_add_derivative","Polynomial.Splits.derivative"],"certificate_hash":"e63acbae81ab20b250be6a8ad6ed68a4d65f13193c39d67955e8931b3180a4e4","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-6fea5aff4f44fa54","role":"sequence","name":"a(n) = 1 if n is of the form m(m+3)/2, otherwise 0.","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-6fea5aff4f44fa54","role":"sequence","name":"a(n) = 1 if n is of the form m(m+3)/2, otherwise 0.","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-06e4036009691da2","operation":{"operation":"theorem_check","theorem":"iterated_preserver"},"operation_detail":"iterated_preserver","conclusion_id":"n-6fea5aff4f44fa54","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":"7c912ab923c9452960fd948e2fd8c52d90d69cab55f4c9bc2b8f8cdc969cc005","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-292206ad4ae86d2d","operation":{"index_shift":0,"modulus":2,"operation":"veronese_section","residue":0},"operation_detail":"r=2, j=0, shift 0","conclusion_id":"n-6fea5aff4f44fa54","premise_count":1,"theorem":"Veronese sections of Polya frequency sequences (Aissen--Schoenberg--Whitney--Edrei): if P is real-rooted with coefficients of one sign, equivalently nonzero with all roots in (-inf, 0], every section V_(r,j)(P) is zero or real-rooted with roots in (-inf, 0]","lean_route":null,"lean_declarations":[],"certificate_hash":"c465820f18c46c973a857042716eb1aaf6aa6c14f8138fb65e09d43ac3468670","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-cdb0db4ad473ee28","role":"sequence","name":"basis-map coefficients of Irregular triangle read by rows formed by taking every other row of the Delannoy array (A008288) regarded as a triangle. shifted by x -> -x + 0","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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-b7eca039219a7f53","operation":{"operation":"parent_provers","route":"periodic_product"},"operation_detail":"periodic_product","conclusion_id":"n-6fea5aff4f44fa54","premise_count":0,"theorem":"polytool parent provers, route periodic_product: every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign","lean_route":null,"lean_declarations":[],"certificate_hash":"28b0677de51356622004bdee49b3e32263cbcbf0992e57af7cdf296451825f68","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-7e44b66e04c497d6","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"mobius\",\"a\":\"1\",\"b\":\"0\",\"c\":\"1\",\"e\":\"1\",\"schedule\":{\"first_index\":0,\"first_degree\":0,\"step\":1}}"},"operation_detail":"mobius, shift 0","conclusion_id":"n-6fea5aff4f44fa54","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":"fTransform","lean_declarations":["RealRooted.splits_fPolynomial"],"certificate_hash":"29fd5ce083ab0ea9777d2838738405a218d7a71aee67f7d82621aeb4d52fb9a1","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":true,"value":"-1"},"upper":{"closed":true,"value":"0"}}}],"premises":[{"position":0,"node_id":"n-6fea5aff4f44fa54","role":"sequence","name":"a(n) = 1 if n is of the form m(m+3)/2, otherwise 0.","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]"}]},"repeat":true,"premises":[]}]}]},{"edge":{"id":"e-f2b6d972cb6f448e","operation":{"operation":"theorem_check","theorem":"liu_wang_three_term"},"operation_detail":"liu_wang_three_term","conclusion_id":"n-66d5ecabca128038","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","lean_route":null,"lean_declarations":["RealRooted.MaWang.strictInterl_of_interlaces_evalCoeff_nonpos"],"certificate_hash":"143b05acc967dab496e7cfa8a4602883f9404ac12763af8f0483a90c4d86d05b","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-cbd96c681ac3cbdc","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"mobius\",\"a\":\"1\",\"b\":\"0\",\"c\":\"1\",\"e\":\"1\",\"schedule\":{\"first_index\":0,\"first_degree\":0,\"step\":1}}"},"operation_detail":"mobius, shift 0","conclusion_id":"n-f4c1dee76f5a68b2","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":"fTransform","lean_declarations":["RealRooted.splits_fPolynomial"],"certificate_hash":"a4202a8d4eb6e5999d7a509d5e00e66d76b448dea1b5b33fe91436b016a15332","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":true,"value":"-1"},"upper":{"closed":true,"value":"0"}}}],"premises":[{"position":0,"node_id":"n-66d5ecabca128038","role":"sequence","name":"Triangle read by rows, (n-1) zeros followed by (2n, 1).","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-66d5ecabca128038","role":"sequence","name":"Triangle read by rows, (n-1) zeros followed by (2n, 1).","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-224384a428b81acf","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"derivative_polynomial\",\"coefficients\":[{\"numerator\":[\"1\"],\"denominator\":[\"1\"]},{\"numerator\":[\"2\"],\"denominator\":[\"1\"]}]}"},"operation_detail":"derivative_polynomial, shift 0","conclusion_id":"n-66d5ecabca128038","premise_count":1,"theorem":"Laguerre's theorem on differential operators: if phi is a real polynomial with only real roots, then phi(D) maps every real-rooted polynomial to a real-rooted polynomial or zero (write phi(D) = C D^j prod (1 + c_i D); D preserves real-rootedness by Rolle's theorem and p + c p' is real-rooted for every real c by Rolle's theorem applied to e^(x/c) p; Polya--Schur 1914); when the coefficients of phi have one sign, coefficients of one sign stay of one sign; applied to phi(n, .) for each n","lean_route":null,"lean_declarations":["RealRooted.splits_add_C_mul_derivative_all","RealRooted.splits_C_mul_add_derivative","Polynomial.Splits.derivative"],"certificate_hash":"e63acbae81ab20b250be6a8ad6ed68a4d65f13193c39d67955e8931b3180a4e4","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-6fea5aff4f44fa54","role":"sequence","name":"a(n) = 1 if n is of the form m(m+3)/2, otherwise 0.","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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-f2b6d972cb6f448e","operation":{"operation":"theorem_check","theorem":"liu_wang_three_term"},"operation_detail":"liu_wang_three_term","conclusion_id":"n-66d5ecabca128038","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","lean_route":null,"lean_declarations":["RealRooted.MaWang.strictInterl_of_interlaces_evalCoeff_nonpos"],"certificate_hash":"143b05acc967dab496e7cfa8a4602883f9404ac12763af8f0483a90c4d86d05b","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-93737dfd95ce689c","operation":{"index_shift":0,"modulus":2,"operation":"veronese_section","residue":1},"operation_detail":"r=2, j=1, shift 0","conclusion_id":"n-0efca9aef0911045","premise_count":1,"theorem":"Veronese sections of Polya frequency sequences (Aissen--Schoenberg--Whitney--Edrei): if P is real-rooted with coefficients of one sign, equivalently nonzero with all roots in (-inf, 0], every section V_(r,j)(P) is zero or real-rooted with roots in (-inf, 0]","lean_route":null,"lean_declarations":[],"certificate_hash":"3469ae8858ff73425e964a123d4dbedcca66e8b6e0a3e679d691b7fa544017ca","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-f4c1dee76f5a68b2","role":"sequence","name":"A natural number operator.","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-f4c1dee76f5a68b2","role":"sequence","name":"A natural number operator.","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-3fa49e62bb44b5e9","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"derivative_polynomial\",\"coefficients\":[{\"numerator\":[\"1\",\"2\"],\"denominator\":[\"1\"]},{\"numerator\":[\"2\"],\"denominator\":[\"1\"]}]}"},"operation_detail":"derivative_polynomial, shift 0","conclusion_id":"n-f4c1dee76f5a68b2","premise_count":1,"theorem":"Laguerre's theorem on differential operators: if phi is a real polynomial with only real roots, then phi(D) maps every real-rooted polynomial to a real-rooted polynomial or zero (write phi(D) = C D^j prod (1 + c_i D); D preserves real-rootedness by Rolle's theorem and p + c p' is real-rooted for every real c by Rolle's theorem applied to e^(x/c) p; Polya--Schur 1914); when the coefficients of phi have one sign, coefficients of one sign stay of one sign; applied to phi(n, .) for each n","lean_route":null,"lean_declarations":["RealRooted.splits_add_C_mul_derivative_all","RealRooted.splits_C_mul_add_derivative","Polynomial.Splits.derivative"],"certificate_hash":"4b4b993bacdbfba3402e6d1e91fbdba1bb2ecb2193958d2cb51bcf416991f067","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-6fea5aff4f44fa54","role":"sequence","name":"a(n) = 1 if n is of the form m(m+3)/2, otherwise 0.","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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-f4214b1b9dbd784c","operation":{"operation":"theorem_check","theorem":"liu_wang_three_term"},"operation_detail":"liu_wang_three_term","conclusion_id":"n-f4c1dee76f5a68b2","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","lean_route":null,"lean_declarations":["RealRooted.MaWang.strictInterl_of_interlaces_evalCoeff_nonpos"],"certificate_hash":"253f3befb8cf4d8ee832df5b715879d3d85c59775cccd4e5a3da38dad5e2aa68","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-7c3f493b81ba2cb3","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"mobius\",\"a\":\"1\",\"b\":\"0\",\"c\":\"1\",\"e\":\"1\",\"schedule\":{\"first_index\":0,\"first_degree\":0,\"step\":1}}"},"operation_detail":"mobius, shift 0","conclusion_id":"n-f4c1dee76f5a68b2","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":"fTransform","lean_declarations":["RealRooted.splits_fPolynomial"],"certificate_hash":"7765934752f29369985835b4d83b641e4b8fb7457121b8a97a7a6d51bbb31c0a","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":true,"value":"-1"},"upper":{"closed":true,"value":"0"}}}],"premises":[{"position":0,"node_id":"n-66d5ecabca128038","role":"sequence","name":"Triangle read by rows, (n-1) zeros followed by (2n, 1).","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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-cbd96c681ac3cbdc","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"mobius\",\"a\":\"1\",\"b\":\"0\",\"c\":\"1\",\"e\":\"1\",\"schedule\":{\"first_index\":0,\"first_degree\":0,\"step\":1}}"},"operation_detail":"mobius, shift 0","conclusion_id":"n-f4c1dee76f5a68b2","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":"fTransform","lean_declarations":["RealRooted.splits_fPolynomial"],"certificate_hash":"a4202a8d4eb6e5999d7a509d5e00e66d76b448dea1b5b33fe91436b016a15332","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":true,"value":"-1"},"upper":{"closed":true,"value":"0"}}}],"premises":[{"position":0,"node_id":"n-66d5ecabca128038","role":"sequence","name":"Triangle read by rows, (n-1) zeros followed by (2n, 1).","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]"}]},"repeat":true,"premises":[]}]}]}]}]}],"truncated":false,"expanded":16}