{"chains":[{"edge":{"id":"e-84973f039edbd602","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-c6ff1e446479ba16","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":"d5130ca2e7490ad45df8b1070848c6bc98dcbf9c6750adfa1d2740ca7235614e","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-22e887254e1ffff8","role":"sequence","name":"basis_map_A013609 of Triangle T(n,k) giving number of degree-2n permutations which decompose into exactly k cycles of even length, k=0..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-22e887254e1ffff8","role":"sequence","name":"basis_map_A013609 of Triangle T(n,k) giving number of degree-2n permutations which decompose into exactly k cycles of even length, k=0..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-2613ba1fbc2604f1","operation":{"map":"A013609","operation":"basis_map"},"operation_detail":"A013609","conclusion_id":"n-22e887254e1ffff8","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":"5ca2c1fafd081a33d52bc9d5d5e9c82c94513e644eab502d16297f59af4fd6a6","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-1336d058dca9979e","role":"sequence","name":"Triangle T(n,k) giving number of degree-2n permutations which decompose into exactly k cycles of even length, k=0..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-1336d058dca9979e","role":"sequence","name":"Triangle T(n,k) giving number of degree-2n permutations which decompose into exactly k cycles of even length, k=0..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-1e6b41b2748404cf","operation":{"operation":"parent_provers","route":"root_domain"},"operation_detail":"root_domain","conclusion_id":"n-1336d058dca9979e","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":"7c9de2194e6cbeeb08e2d7bf1bcf9b0ff62a1a72989c49596df826fcf261d8e1","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-70cef482b9d83b1c","operation":{"operation":"theorem_check","theorem":"iterated_preserver"},"operation_detail":"iterated_preserver","conclusion_id":"n-1336d058dca9979e","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":"ba17c1ab6d91299d51c179687271f93f49549be695eb3aebb6f70c403e13f799","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-8239b1c6b4764045","operation":{"operation":"parent_provers","route":"root_domain"},"operation_detail":"root_domain","conclusion_id":"n-1336d058dca9979e","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":"75ac45a5ece707a69127081905aac1ec98084fc5c21cdd763f1373cfe6557418","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-e22b6489d413d499","operation":{"map":"A013609","operation":"basis_map"},"operation_detail":"A013609","conclusion_id":"n-22e887254e1ffff8","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":"02025d09eafa681c6fc24c87d46772b4614019ee67894ffab698c29b3b6eb39a","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-1336d058dca9979e","role":"sequence","name":"Triangle T(n,k) giving number of degree-2n permutations which decompose into exactly k cycles of even length, k=0..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-1336d058dca9979e","role":"sequence","name":"Triangle T(n,k) giving number of degree-2n permutations which decompose into exactly k cycles of even length, k=0..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-1e6b41b2748404cf","operation":{"operation":"parent_provers","route":"root_domain"},"operation_detail":"root_domain","conclusion_id":"n-1336d058dca9979e","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":"7c9de2194e6cbeeb08e2d7bf1bcf9b0ff62a1a72989c49596df826fcf261d8e1","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-70cef482b9d83b1c","operation":{"operation":"theorem_check","theorem":"iterated_preserver"},"operation_detail":"iterated_preserver","conclusion_id":"n-1336d058dca9979e","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":"ba17c1ab6d91299d51c179687271f93f49549be695eb3aebb6f70c403e13f799","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-8239b1c6b4764045","operation":{"operation":"parent_provers","route":"root_domain"},"operation_detail":"root_domain","conclusion_id":"n-1336d058dca9979e","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":"75ac45a5ece707a69127081905aac1ec98084fc5c21cdd763f1373cfe6557418","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":6}