{"chains":[{"edge":{"id":"e-45dbacd2ab49646c","operation":{"index_shift":0,"modulus":2,"operation":"veronese_section","residue":1},"operation_detail":"r=2, j=1, shift 0","conclusion_id":"n-82635508a6f8758c","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":"2b50c243a19fb5ed9c1958e61b2809310479d4915d834cb25f11c72e0f6e8cca","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-016d7724d51f6416","role":"sequence","name":"Riordan array (1, 3+3x).","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-016d7724d51f6416","role":"sequence","name":"Riordan array (1, 3+3x).","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-97db6227df9d6f92","operation":{"map":"A099093","operation":"basis_map"},"operation_detail":"A099093","conclusion_id":"n-016d7724d51f6416","premise_count":1,"theorem":"affine current multiplier with an affine initial row (module documentation, \"The affine-current theorem\"): with beta = b/d, K = beta^2 + a beta - c > 0 and eta = m/d >= 0, every real polynomial with all roots in E = [-beta - sqrt(K), -beta + sqrt(K)] has a real-rooted image, and no interval of positive length outside E works (Theorem 1); for eta > 0 the images lie in I = [(-a - 2 beta - 2 sqrt(K))/d, (-a - 2 beta + 2 sqrt(K))/d] if and only if eta >= 1/2 and (s - (2 eta - 1) beta)^2 <= (2 eta - 1)^2 K, s = l - eta a (Theorem 2); with a >= 0, K >= beta^2, a + 2 beta >= 0, a^2 + 4c >= 0, l >= 0 and the scalar criterion, PF inputs with roots in [-R, 0], R = beta + sqrt(K), have PF images, sharply (the common-interlacer proof; the Chebyshev case is Iserles and Saff, Math. Proc. Cambridge Philos. Soc. 105 (1989), Theorem 1; the scalar criterion is RealRooted orderTwoConstants_nonneg_iff)","lean_route":null,"lean_declarations":[],"certificate_hash":"ae21c3aab0072bcb0b759810d40fcc82ed63fe0f50d34afa198133f91513d59a","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":true,"value":"-4/3"},"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":{"lower":{"closed":true,"value":"0"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in [0, 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":{"lower":{"closed":true,"value":"0"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in [0, 0]"},"chains":[]}]},{"edge":{"id":"e-a3711e6f8037cbc8","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-016d7724d51f6416","premise_count":0,"theorem":"S.-M. Ma and Y. Wang, q-Eulerian polynomials and polynomials with only real zeros, Electron. J. Combin. 15 (2008) R17, Theorem 2 and Corollary 3 (arXiv:math/0611826), in the closed two-endpoint form of the RealRooted library (https://github.com/PerAlexandersson/RealRooted, RealRooted.affineEndpointStep_closed), after the change of variable x = U + (U - L) y, with the endpoint multiplicities tracked exactly through the induction","lean_route":null,"lean_declarations":["RealRooted.affineEndpointStep_closed","RealRooted.affineEndpointStep_roots_mem_Icc_iff","RealRooted.affineEndpointStep_rootMultiplicity_zero","RealRooted.affineEndpointStep_rootMultiplicity_neg_one","RealRooted.MaWang.endpointStep","RealRooted.MaWang.affineEndpointSequence","RealRooted.normalizedAffineEndpointSequence_roots_mem_Icc_iff"],"certificate_hash":"ed99275eeb269a7692b27d618c30778d69f4602b9e0bab63d3f711b571a775fd","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"premises":[]},{"edge":{"id":"e-04516916870a85c6","operation":{"map":"A027466","operation":"basis_map"},"operation_detail":"A027466","conclusion_id":"n-016d7724d51f6416","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":"ba4f03b6207308a01675821b2b2a6671c5b9f6d0ce37d2c930a59dcb177419af","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-b481f693dcd8357c","role":"sequence","name":"basis-map coefficients of Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"7"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 7]"}]},"premises":[{"premise":{"position":0,"node_id":"n-b481f693dcd8357c","role":"sequence","name":"basis-map coefficients of Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"7"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 7]"},"chains":[{"edge":{"id":"e-bc143c20b95292bc","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-7\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-b481f693dcd8357c","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":null,"lean_declarations":["Polynomial.Splits.comp_of_degree_le_one"],"certificate_hash":"9fca20b3c6833998975bdad3822ae25ce6bfad0b6f20e409634367b26871252b","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"17/3"},"upper":{"closed":true,"value":"7"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-016d7724d51f6416","role":"sequence","name":"Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4/3, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-016d7724d51f6416","role":"sequence","name":"Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4/3, 0]"},"chains":[{"edge":{"id":"e-a3711e6f8037cbc8","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-016d7724d51f6416","premise_count":0,"theorem":"S.-M. Ma and Y. Wang, q-Eulerian polynomials and polynomials with only real zeros, Electron. J. Combin. 15 (2008) R17, Theorem 2 and Corollary 3 (arXiv:math/0611826), in the closed two-endpoint form of the RealRooted library (https://github.com/PerAlexandersson/RealRooted, RealRooted.affineEndpointStep_closed), after the change of variable x = U + (U - L) y, with the endpoint multiplicities tracked exactly through the induction","lean_route":null,"lean_declarations":["RealRooted.affineEndpointStep_closed","RealRooted.affineEndpointStep_roots_mem_Icc_iff","RealRooted.affineEndpointStep_rootMultiplicity_zero","RealRooted.affineEndpointStep_rootMultiplicity_neg_one","RealRooted.MaWang.endpointStep","RealRooted.MaWang.affineEndpointSequence","RealRooted.normalizedAffineEndpointSequence_roots_mem_Icc_iff"],"certificate_hash":"ed99275eeb269a7692b27d618c30778d69f4602b9e0bab63d3f711b571a775fd","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-089b35b0d9fc7c83","operation":{"map":"A038243","operation":"basis_map"},"operation_detail":"A038243","conclusion_id":"n-016d7724d51f6416","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":"5b7bf863668dee68c26f0f9eea2d0920697e3725d6597584cba31882b9dee7c5","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-ce49db683d596495","role":"sequence","name":"basis-map coefficients of Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"5"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 5]"}]},"premises":[{"premise":{"position":0,"node_id":"n-ce49db683d596495","role":"sequence","name":"basis-map coefficients of Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"5"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 5]"},"chains":[{"edge":{"id":"e-ae28d4484158822f","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-5\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-ce49db683d596495","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":null,"lean_declarations":["Polynomial.Splits.comp_of_degree_le_one"],"certificate_hash":"f5e490405f81862db4e7ccf123d12eb2fa30d30f6755482f1fc32122df3b6e9b","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"11/3"},"upper":{"closed":true,"value":"5"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-016d7724d51f6416","role":"sequence","name":"Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4/3, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-016d7724d51f6416","role":"sequence","name":"Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4/3, 0]"},"chains":[{"edge":{"id":"e-a3711e6f8037cbc8","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-016d7724d51f6416","premise_count":0,"theorem":"S.-M. Ma and Y. Wang, q-Eulerian polynomials and polynomials with only real zeros, Electron. J. Combin. 15 (2008) R17, Theorem 2 and Corollary 3 (arXiv:math/0611826), in the closed two-endpoint form of the RealRooted library (https://github.com/PerAlexandersson/RealRooted, RealRooted.affineEndpointStep_closed), after the change of variable x = U + (U - L) y, with the endpoint multiplicities tracked exactly through the induction","lean_route":null,"lean_declarations":["RealRooted.affineEndpointStep_closed","RealRooted.affineEndpointStep_roots_mem_Icc_iff","RealRooted.affineEndpointStep_rootMultiplicity_zero","RealRooted.affineEndpointStep_rootMultiplicity_neg_one","RealRooted.MaWang.endpointStep","RealRooted.MaWang.affineEndpointSequence","RealRooted.normalizedAffineEndpointSequence_roots_mem_Icc_iff"],"certificate_hash":"ed99275eeb269a7692b27d618c30778d69f4602b9e0bab63d3f711b571a775fd","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-344ac1c74a22d15f","operation":{"map":"A007318","operation":"basis_map"},"operation_detail":"A007318","conclusion_id":"n-016d7724d51f6416","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":"34032b4d96c71c84359213ef1052fa8a6077f15a2325b5a843646312051032a8","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-c7f2f3338041a8d8","role":"sequence","name":"basis-map coefficients of Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"1"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 1]"}]},"premises":[{"premise":{"position":0,"node_id":"n-c7f2f3338041a8d8","role":"sequence","name":"basis-map coefficients of Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"1"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 1]"},"chains":[{"edge":{"id":"e-9ac4433d08f91ae9","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-1\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-c7f2f3338041a8d8","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":null,"lean_declarations":["Polynomial.Splits.comp_of_degree_le_one"],"certificate_hash":"a8f6f97fd63391368077d2b31938a4192f2d2f2e5bc7f46b1805f82fde00c07d","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-1/3"},"upper":{"closed":true,"value":"1"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-016d7724d51f6416","role":"sequence","name":"Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4/3, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-016d7724d51f6416","role":"sequence","name":"Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4/3, 0]"},"chains":[{"edge":{"id":"e-a3711e6f8037cbc8","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-016d7724d51f6416","premise_count":0,"theorem":"S.-M. Ma and Y. Wang, q-Eulerian polynomials and polynomials with only real zeros, Electron. J. Combin. 15 (2008) R17, Theorem 2 and Corollary 3 (arXiv:math/0611826), in the closed two-endpoint form of the RealRooted library (https://github.com/PerAlexandersson/RealRooted, RealRooted.affineEndpointStep_closed), after the change of variable x = U + (U - L) y, with the endpoint multiplicities tracked exactly through the induction","lean_route":null,"lean_declarations":["RealRooted.affineEndpointStep_closed","RealRooted.affineEndpointStep_roots_mem_Icc_iff","RealRooted.affineEndpointStep_rootMultiplicity_zero","RealRooted.affineEndpointStep_rootMultiplicity_neg_one","RealRooted.MaWang.endpointStep","RealRooted.MaWang.affineEndpointSequence","RealRooted.normalizedAffineEndpointSequence_roots_mem_Icc_iff"],"certificate_hash":"ed99275eeb269a7692b27d618c30778d69f4602b9e0bab63d3f711b571a775fd","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-3547903a43c489fd","operation":{"map":"A038231","operation":"basis_map"},"operation_detail":"A038231","conclusion_id":"n-016d7724d51f6416","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":"87833a4e7d126ebc4259aef239b779e79ffd02b6c9551b92d92bab6bd7ceb3e8","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-e58e3554d9394f92","role":"sequence","name":"basis-map coefficients of Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"4"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 4]"}]},"premises":[{"premise":{"position":0,"node_id":"n-e58e3554d9394f92","role":"sequence","name":"basis-map coefficients of Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"4"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 4]"},"chains":[{"edge":{"id":"e-4e1348328210bdec","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-4\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-e58e3554d9394f92","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":null,"lean_declarations":["Polynomial.Splits.comp_of_degree_le_one"],"certificate_hash":"c5b9ec4cd28e72067da5b47bc7905dde27025b94805d323a0b638796464a7b34","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"8/3"},"upper":{"closed":true,"value":"4"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-016d7724d51f6416","role":"sequence","name":"Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4/3, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-016d7724d51f6416","role":"sequence","name":"Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4/3, 0]"},"chains":[{"edge":{"id":"e-a3711e6f8037cbc8","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-016d7724d51f6416","premise_count":0,"theorem":"S.-M. Ma and Y. Wang, q-Eulerian polynomials and polynomials with only real zeros, Electron. J. Combin. 15 (2008) R17, Theorem 2 and Corollary 3 (arXiv:math/0611826), in the closed two-endpoint form of the RealRooted library (https://github.com/PerAlexandersson/RealRooted, RealRooted.affineEndpointStep_closed), after the change of variable x = U + (U - L) y, with the endpoint multiplicities tracked exactly through the induction","lean_route":null,"lean_declarations":["RealRooted.affineEndpointStep_closed","RealRooted.affineEndpointStep_roots_mem_Icc_iff","RealRooted.affineEndpointStep_rootMultiplicity_zero","RealRooted.affineEndpointStep_rootMultiplicity_neg_one","RealRooted.MaWang.endpointStep","RealRooted.MaWang.affineEndpointSequence","RealRooted.normalizedAffineEndpointSequence_roots_mem_Icc_iff"],"certificate_hash":"ed99275eeb269a7692b27d618c30778d69f4602b9e0bab63d3f711b571a775fd","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-35fdacf74fcfdf8c","operation":{"map":"A027467","operation":"basis_map"},"operation_detail":"A027467","conclusion_id":"n-016d7724d51f6416","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":"69eaa80605e71abac13d462bc457d8a2215bc9fcbd93311b7073c7b5c623c339","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-8910fc24d8983662","role":"sequence","name":"basis-map coefficients of Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"15"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 15]"}]},"premises":[{"premise":{"position":0,"node_id":"n-8910fc24d8983662","role":"sequence","name":"basis-map coefficients of Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"15"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 15]"},"chains":[{"edge":{"id":"e-b320272c2500474a","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-15\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-8910fc24d8983662","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":null,"lean_declarations":["Polynomial.Splits.comp_of_degree_le_one"],"certificate_hash":"ee76d124510616a9b77df9e17a4a91569a7b0954a26df9ed9de3972dec30b006","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"41/3"},"upper":{"closed":true,"value":"15"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-016d7724d51f6416","role":"sequence","name":"Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4/3, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-016d7724d51f6416","role":"sequence","name":"Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4/3, 0]"},"chains":[{"edge":{"id":"e-a3711e6f8037cbc8","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-016d7724d51f6416","premise_count":0,"theorem":"S.-M. Ma and Y. Wang, q-Eulerian polynomials and polynomials with only real zeros, Electron. J. Combin. 15 (2008) R17, Theorem 2 and Corollary 3 (arXiv:math/0611826), in the closed two-endpoint form of the RealRooted library (https://github.com/PerAlexandersson/RealRooted, RealRooted.affineEndpointStep_closed), after the change of variable x = U + (U - L) y, with the endpoint multiplicities tracked exactly through the induction","lean_route":null,"lean_declarations":["RealRooted.affineEndpointStep_closed","RealRooted.affineEndpointStep_roots_mem_Icc_iff","RealRooted.affineEndpointStep_rootMultiplicity_zero","RealRooted.affineEndpointStep_rootMultiplicity_neg_one","RealRooted.MaWang.endpointStep","RealRooted.MaWang.affineEndpointSequence","RealRooted.normalizedAffineEndpointSequence_roots_mem_Icc_iff"],"certificate_hash":"ed99275eeb269a7692b27d618c30778d69f4602b9e0bab63d3f711b571a775fd","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-69bbc7837aabb73c","operation":{"map":"A027465","operation":"basis_map"},"operation_detail":"A027465","conclusion_id":"n-016d7724d51f6416","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":"387cb5866eeaacc7e24f97997a3d4816cd483c66fe00c9a8590563ecfd6f2aa0","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-4ec583084451043e","role":"sequence","name":"basis-map coefficients of Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"3"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 3]"}]},"premises":[{"premise":{"position":0,"node_id":"n-4ec583084451043e","role":"sequence","name":"basis-map coefficients of Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"3"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 3]"},"chains":[{"edge":{"id":"e-7438d71d24adbb8f","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-3\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-4ec583084451043e","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":null,"lean_declarations":["Polynomial.Splits.comp_of_degree_le_one"],"certificate_hash":"61273dc4961e5fbe0344fd700be9c9e3b152a7b61776c36e6409c1761bac1603","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"5/3"},"upper":{"closed":true,"value":"3"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-016d7724d51f6416","role":"sequence","name":"Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4/3, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-016d7724d51f6416","role":"sequence","name":"Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4/3, 0]"},"chains":[{"edge":{"id":"e-a3711e6f8037cbc8","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-016d7724d51f6416","premise_count":0,"theorem":"S.-M. Ma and Y. Wang, q-Eulerian polynomials and polynomials with only real zeros, Electron. J. Combin. 15 (2008) R17, Theorem 2 and Corollary 3 (arXiv:math/0611826), in the closed two-endpoint form of the RealRooted library (https://github.com/PerAlexandersson/RealRooted, RealRooted.affineEndpointStep_closed), after the change of variable x = U + (U - L) y, with the endpoint multiplicities tracked exactly through the induction","lean_route":null,"lean_declarations":["RealRooted.affineEndpointStep_closed","RealRooted.affineEndpointStep_roots_mem_Icc_iff","RealRooted.affineEndpointStep_rootMultiplicity_zero","RealRooted.affineEndpointStep_rootMultiplicity_neg_one","RealRooted.MaWang.endpointStep","RealRooted.MaWang.affineEndpointSequence","RealRooted.normalizedAffineEndpointSequence_roots_mem_Icc_iff"],"certificate_hash":"ed99275eeb269a7692b27d618c30778d69f4602b9e0bab63d3f711b571a775fd","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-70271c52b20af48c","operation":{"map":"A038291","operation":"basis_map"},"operation_detail":"A038291","conclusion_id":"n-016d7724d51f6416","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":"4fbba89c60794520b0a8c1c1f02cc2c33be2d01859e2b19cbaf9cc86f45a0984","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-767aa1cf87a969b2","role":"sequence","name":"basis-map coefficients of Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"9"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 9]"}]},"premises":[{"premise":{"position":0,"node_id":"n-767aa1cf87a969b2","role":"sequence","name":"basis-map coefficients of Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"9"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 9]"},"chains":[{"edge":{"id":"e-7d49a73cf4bf68ad","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-9\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-767aa1cf87a969b2","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":null,"lean_declarations":["Polynomial.Splits.comp_of_degree_le_one"],"certificate_hash":"9e77cf0d1034804a523614fc1794bb9df89ae8914513e6ab023dd82e6113bb21","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"23/3"},"upper":{"closed":true,"value":"9"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-016d7724d51f6416","role":"sequence","name":"Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4/3, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-016d7724d51f6416","role":"sequence","name":"Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4/3, 0]"},"chains":[{"edge":{"id":"e-a3711e6f8037cbc8","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-016d7724d51f6416","premise_count":0,"theorem":"S.-M. Ma and Y. Wang, q-Eulerian polynomials and polynomials with only real zeros, Electron. J. Combin. 15 (2008) R17, Theorem 2 and Corollary 3 (arXiv:math/0611826), in the closed two-endpoint form of the RealRooted library (https://github.com/PerAlexandersson/RealRooted, RealRooted.affineEndpointStep_closed), after the change of variable x = U + (U - L) y, with the endpoint multiplicities tracked exactly through the induction","lean_route":null,"lean_declarations":["RealRooted.affineEndpointStep_closed","RealRooted.affineEndpointStep_roots_mem_Icc_iff","RealRooted.affineEndpointStep_rootMultiplicity_zero","RealRooted.affineEndpointStep_rootMultiplicity_neg_one","RealRooted.MaWang.endpointStep","RealRooted.MaWang.affineEndpointSequence","RealRooted.normalizedAffineEndpointSequence_roots_mem_Icc_iff"],"certificate_hash":"ed99275eeb269a7692b27d618c30778d69f4602b9e0bab63d3f711b571a775fd","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-726dbe4e92e67f96","operation":{"map":"A038207","operation":"basis_map"},"operation_detail":"A038207","conclusion_id":"n-016d7724d51f6416","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":"4073dfa7460f237549b4b8310029e336c62be8fb68978d91a21586ce29bc3769","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-ffce392acf4abae7","role":"sequence","name":"basis-map coefficients of Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"2"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 2]"}]},"premises":[{"premise":{"position":0,"node_id":"n-ffce392acf4abae7","role":"sequence","name":"basis-map coefficients of Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"2"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 2]"},"chains":[{"edge":{"id":"e-8e25fd3c0a02e03b","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-2\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-ffce392acf4abae7","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":null,"lean_declarations":["Polynomial.Splits.comp_of_degree_le_one"],"certificate_hash":"63a47263f2464491899e02f7222eaf92dac7e02e4a88578a7110c69ec0f1d0a0","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"2/3"},"upper":{"closed":true,"value":"2"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-016d7724d51f6416","role":"sequence","name":"Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4/3, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-016d7724d51f6416","role":"sequence","name":"Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4/3, 0]"},"chains":[{"edge":{"id":"e-a3711e6f8037cbc8","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-016d7724d51f6416","premise_count":0,"theorem":"S.-M. Ma and Y. Wang, q-Eulerian polynomials and polynomials with only real zeros, Electron. J. Combin. 15 (2008) R17, Theorem 2 and Corollary 3 (arXiv:math/0611826), in the closed two-endpoint form of the RealRooted library (https://github.com/PerAlexandersson/RealRooted, RealRooted.affineEndpointStep_closed), after the change of variable x = U + (U - L) y, with the endpoint multiplicities tracked exactly through the induction","lean_route":null,"lean_declarations":["RealRooted.affineEndpointStep_closed","RealRooted.affineEndpointStep_roots_mem_Icc_iff","RealRooted.affineEndpointStep_rootMultiplicity_zero","RealRooted.affineEndpointStep_rootMultiplicity_neg_one","RealRooted.MaWang.endpointStep","RealRooted.MaWang.affineEndpointSequence","RealRooted.normalizedAffineEndpointSequence_roots_mem_Icc_iff"],"certificate_hash":"ed99275eeb269a7692b27d618c30778d69f4602b9e0bab63d3f711b571a775fd","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-78bb889c5d4c7dc1","operation":{"map":"A038279","operation":"basis_map"},"operation_detail":"A038279","conclusion_id":"n-016d7724d51f6416","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":"31324d8574901d692117e58927baaab60f00f6391f5b391beb0c1fb522adc7dd","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-b2ac077f0522ccfd","role":"sequence","name":"basis-map coefficients of Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"8"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 8]"}]},"premises":[{"premise":{"position":0,"node_id":"n-b2ac077f0522ccfd","role":"sequence","name":"basis-map coefficients of Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"8"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 8]"},"chains":[{"edge":{"id":"e-b4aa148b93b9dcb2","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-8\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-b2ac077f0522ccfd","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":null,"lean_declarations":["Polynomial.Splits.comp_of_degree_le_one"],"certificate_hash":"a0536bbb0269b95a5e704c3ce904a62e4116b0f16d3374ab9999111a550e92e6","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"20/3"},"upper":{"closed":true,"value":"8"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-016d7724d51f6416","role":"sequence","name":"Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4/3, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-016d7724d51f6416","role":"sequence","name":"Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4/3, 0]"},"chains":[{"edge":{"id":"e-a3711e6f8037cbc8","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-016d7724d51f6416","premise_count":0,"theorem":"S.-M. Ma and Y. Wang, q-Eulerian polynomials and polynomials with only real zeros, Electron. J. Combin. 15 (2008) R17, Theorem 2 and Corollary 3 (arXiv:math/0611826), in the closed two-endpoint form of the RealRooted library (https://github.com/PerAlexandersson/RealRooted, RealRooted.affineEndpointStep_closed), after the change of variable x = U + (U - L) y, with the endpoint multiplicities tracked exactly through the induction","lean_route":null,"lean_declarations":["RealRooted.affineEndpointStep_closed","RealRooted.affineEndpointStep_roots_mem_Icc_iff","RealRooted.affineEndpointStep_rootMultiplicity_zero","RealRooted.affineEndpointStep_rootMultiplicity_neg_one","RealRooted.MaWang.endpointStep","RealRooted.MaWang.affineEndpointSequence","RealRooted.normalizedAffineEndpointSequence_roots_mem_Icc_iff"],"certificate_hash":"ed99275eeb269a7692b27d618c30778d69f4602b9e0bab63d3f711b571a775fd","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-a4925a412f743bbb","operation":{"map":"A038303","operation":"basis_map"},"operation_detail":"A038303","conclusion_id":"n-016d7724d51f6416","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":"4662f3866d09af58dafe7eedade567ce2e22c836502f6dd6cc61f9183f7197a3","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-e2dcd39fb6d71722","role":"sequence","name":"basis-map coefficients of Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"10"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 10]"}]},"premises":[{"premise":{"position":0,"node_id":"n-e2dcd39fb6d71722","role":"sequence","name":"basis-map coefficients of Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"10"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 10]"},"chains":[{"edge":{"id":"e-d18687645e4e9661","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-10\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-e2dcd39fb6d71722","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":null,"lean_declarations":["Polynomial.Splits.comp_of_degree_le_one"],"certificate_hash":"48a6b59c9ea0eb58d5436b5871ef5a41e2d9b8b0e939964e6aaf68b4bdcc4641","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"26/3"},"upper":{"closed":true,"value":"10"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-016d7724d51f6416","role":"sequence","name":"Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4/3, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-016d7724d51f6416","role":"sequence","name":"Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4/3, 0]"},"chains":[{"edge":{"id":"e-a3711e6f8037cbc8","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-016d7724d51f6416","premise_count":0,"theorem":"S.-M. Ma and Y. Wang, q-Eulerian polynomials and polynomials with only real zeros, Electron. J. Combin. 15 (2008) R17, Theorem 2 and Corollary 3 (arXiv:math/0611826), in the closed two-endpoint form of the RealRooted library (https://github.com/PerAlexandersson/RealRooted, RealRooted.affineEndpointStep_closed), after the change of variable x = U + (U - L) y, with the endpoint multiplicities tracked exactly through the induction","lean_route":null,"lean_declarations":["RealRooted.affineEndpointStep_closed","RealRooted.affineEndpointStep_roots_mem_Icc_iff","RealRooted.affineEndpointStep_rootMultiplicity_zero","RealRooted.affineEndpointStep_rootMultiplicity_neg_one","RealRooted.MaWang.endpointStep","RealRooted.MaWang.affineEndpointSequence","RealRooted.normalizedAffineEndpointSequence_roots_mem_Icc_iff"],"certificate_hash":"ed99275eeb269a7692b27d618c30778d69f4602b9e0bab63d3f711b571a775fd","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-e0b7b31567b585e1","operation":{"map":"A038327","operation":"basis_map"},"operation_detail":"A038327","conclusion_id":"n-016d7724d51f6416","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":"36a03f3d6de2c8dc8c4979a07ea34bc93a3af6d20404ca2072b1cec4576c4dcf","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-2ed842deeffb5058","role":"sequence","name":"basis-map coefficients of Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"12"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 12]"}]},"premises":[{"premise":{"position":0,"node_id":"n-2ed842deeffb5058","role":"sequence","name":"basis-map coefficients of Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"12"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 12]"},"chains":[{"edge":{"id":"e-2a73ae63953e9ff6","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-12\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-2ed842deeffb5058","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":null,"lean_declarations":["Polynomial.Splits.comp_of_degree_le_one"],"certificate_hash":"9fd9bb86eb314ef28d7bde0de0533395262ebe23113857af2f64153434bcf6d5","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"32/3"},"upper":{"closed":true,"value":"12"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-016d7724d51f6416","role":"sequence","name":"Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4/3, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-016d7724d51f6416","role":"sequence","name":"Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4/3, 0]"},"chains":[{"edge":{"id":"e-a3711e6f8037cbc8","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-016d7724d51f6416","premise_count":0,"theorem":"S.-M. Ma and Y. Wang, q-Eulerian polynomials and polynomials with only real zeros, Electron. J. Combin. 15 (2008) R17, Theorem 2 and Corollary 3 (arXiv:math/0611826), in the closed two-endpoint form of the RealRooted library (https://github.com/PerAlexandersson/RealRooted, RealRooted.affineEndpointStep_closed), after the change of variable x = U + (U - L) y, with the endpoint multiplicities tracked exactly through the induction","lean_route":null,"lean_declarations":["RealRooted.affineEndpointStep_closed","RealRooted.affineEndpointStep_roots_mem_Icc_iff","RealRooted.affineEndpointStep_rootMultiplicity_zero","RealRooted.affineEndpointStep_rootMultiplicity_neg_one","RealRooted.MaWang.endpointStep","RealRooted.MaWang.affineEndpointSequence","RealRooted.normalizedAffineEndpointSequence_roots_mem_Icc_iff"],"certificate_hash":"ed99275eeb269a7692b27d618c30778d69f4602b9e0bab63d3f711b571a775fd","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-e9cb24f9617f2dae","operation":{"map":"A038255","operation":"basis_map"},"operation_detail":"A038255","conclusion_id":"n-016d7724d51f6416","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":"129e54740897c8489a50aec75abe68a409dd820368f7ba06367c249b120732de","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-4c459b8c0c09c21c","role":"sequence","name":"basis-map coefficients of Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"6"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 6]"}]},"premises":[{"premise":{"position":0,"node_id":"n-4c459b8c0c09c21c","role":"sequence","name":"basis-map coefficients of Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"6"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 6]"},"chains":[{"edge":{"id":"e-6c0da882dbe0cffe","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-6\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-4c459b8c0c09c21c","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":null,"lean_declarations":["Polynomial.Splits.comp_of_degree_le_one"],"certificate_hash":"8b74cd658ad30f89f736988959366380a9aead344c4c81a85ae4155915314877","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"14/3"},"upper":{"closed":true,"value":"6"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-016d7724d51f6416","role":"sequence","name":"Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4/3, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-016d7724d51f6416","role":"sequence","name":"Riordan array (1, 3+3x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4/3, 0]"},"chains":[{"edge":{"id":"e-a3711e6f8037cbc8","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-016d7724d51f6416","premise_count":0,"theorem":"S.-M. Ma and Y. Wang, q-Eulerian polynomials and polynomials with only real zeros, Electron. J. Combin. 15 (2008) R17, Theorem 2 and Corollary 3 (arXiv:math/0611826), in the closed two-endpoint form of the RealRooted library (https://github.com/PerAlexandersson/RealRooted, RealRooted.affineEndpointStep_closed), after the change of variable x = U + (U - L) y, with the endpoint multiplicities tracked exactly through the induction","lean_route":null,"lean_declarations":["RealRooted.affineEndpointStep_closed","RealRooted.affineEndpointStep_roots_mem_Icc_iff","RealRooted.affineEndpointStep_rootMultiplicity_zero","RealRooted.affineEndpointStep_rootMultiplicity_neg_one","RealRooted.MaWang.endpointStep","RealRooted.MaWang.affineEndpointSequence","RealRooted.normalizedAffineEndpointSequence_roots_mem_Icc_iff"],"certificate_hash":"ed99275eeb269a7692b27d618c30778d69f4602b9e0bab63d3f711b571a775fd","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4/3"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]}]}]}],"truncated":false,"expanded":27}