{"chains":[{"edge":{"id":"e-ba56344dd1f68fd7","operation":{"map":"A013609","operation":"basis_map"},"operation_detail":"A013609","conclusion_id":"n-30551c14ec291558","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":"c4e4c3c7a68f2ead4a91bab8aa47044c00e73e8dc2c16b208378f52cb30faf13","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-c27b11147fce8bfa","role":"sequence","name":"Riordan array (1+2x,x(1+x)).","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-c27b11147fce8bfa","role":"sequence","name":"Riordan array (1+2x,x(1+x)).","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-7b745496cf172799","operation":{"map":"A111125","operation":"basis_map"},"operation_detail":"A111125","conclusion_id":"n-c27b11147fce8bfa","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":"4008d52c2220f13fe6acd5bbb218195fe367bfff0a8cdbd4f62c2ca957466c1f","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":true,"value":"-4"},"upper":{"closed":true,"value":"0"}}}],"premises":[{"position":0,"node_id":"n-50902364601606aa","role":"sequence","name":"basis-map coefficients of Triangle of Stirling numbers of 2nd kind, S(n,k), n >= 0, 0 <= k <= n.","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":true,"value":"0"},"upper":{"closed":true,"value":"1"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in [0, 1]"}]},"premises":[{"premise":{"position":0,"node_id":"n-50902364601606aa","role":"sequence","name":"basis-map coefficients of Triangle of Stirling numbers of 2nd kind, S(n,k), n >= 0, 0 <= k <= n.","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":true,"value":"0"},"upper":{"closed":true,"value":"1"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in [0, 1]"},"chains":[]}]},{"edge":{"id":"e-5a8f629e61d609b9","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-c27b11147fce8bfa","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":"0d4c38a70084d94a19cc54e1a0f36299b04467cfbaccf70316626f03dfd26f61","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"premises":[]},{"edge":{"id":"e-0902c3fe08444c8c","operation":{"map":"A038303","operation":"basis_map"},"operation_detail":"A038303","conclusion_id":"n-c27b11147fce8bfa","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":"7d52982ad198d583f94f81e4a75b80b5450ae697f05000c2d2960601cd31ad8c","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-0e6280284de0b3d7","role":"sequence","name":"basis-map coefficients of Riordan array (1+2x,x(1+x)).","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-0e6280284de0b3d7","role":"sequence","name":"basis-map coefficients of Riordan array (1+2x,x(1+x)).","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-e470a688ac88b1cf","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-10\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-0e6280284de0b3d7","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":"00da04cac5cccbb978111d2ca761d00421900d50a7acfa6bbeeb14e7a67d1621","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"6"},"upper":{"closed":true,"value":"10"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-c27b11147fce8bfa","role":"sequence","name":"Riordan array (1+2x,x(1+x)).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-c27b11147fce8bfa","role":"sequence","name":"Riordan array (1+2x,x(1+x)).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4, 0]"},"chains":[{"edge":{"id":"e-5a8f629e61d609b9","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-c27b11147fce8bfa","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":"0d4c38a70084d94a19cc54e1a0f36299b04467cfbaccf70316626f03dfd26f61","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-2011332c4965ce14","operation":{"map":"A038255","operation":"basis_map"},"operation_detail":"A038255","conclusion_id":"n-c27b11147fce8bfa","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":"af608326453176182dceecd13cf3d3c1548bd0c4cf0c48a0b0c5c734eee132d1","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-22896c6867f82de3","role":"sequence","name":"basis-map coefficients of Riordan array (1+2x,x(1+x)).","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-22896c6867f82de3","role":"sequence","name":"basis-map coefficients of Riordan array (1+2x,x(1+x)).","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-defa6799aaae8d2a","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-6\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-22896c6867f82de3","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":"4adb047fcac98ecc4ecacb6276b518d7975e1b37cd7d23944508b5b9cefa032b","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"2"},"upper":{"closed":true,"value":"6"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-c27b11147fce8bfa","role":"sequence","name":"Riordan array (1+2x,x(1+x)).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-c27b11147fce8bfa","role":"sequence","name":"Riordan array (1+2x,x(1+x)).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4, 0]"},"chains":[{"edge":{"id":"e-5a8f629e61d609b9","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-c27b11147fce8bfa","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":"0d4c38a70084d94a19cc54e1a0f36299b04467cfbaccf70316626f03dfd26f61","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-253047f151171d84","operation":{"map":"A038327","operation":"basis_map"},"operation_detail":"A038327","conclusion_id":"n-c27b11147fce8bfa","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":"5f20ae927ecf9ef83e756ad8fc875b5bdc7a94a2afd9e24a68358b1bf4b91f11","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-d1b895351f517faa","role":"sequence","name":"basis-map coefficients of Riordan array (1+2x,x(1+x)).","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-d1b895351f517faa","role":"sequence","name":"basis-map coefficients of Riordan array (1+2x,x(1+x)).","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-f8dba443f4d27d49","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-12\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-d1b895351f517faa","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":"7ba7be6587d4fa6c1015a37249de484d75051ef3ae7de12b32b697cc7e2e9888","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"8"},"upper":{"closed":true,"value":"12"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-c27b11147fce8bfa","role":"sequence","name":"Riordan array (1+2x,x(1+x)).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-c27b11147fce8bfa","role":"sequence","name":"Riordan array (1+2x,x(1+x)).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4, 0]"},"chains":[{"edge":{"id":"e-5a8f629e61d609b9","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-c27b11147fce8bfa","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":"0d4c38a70084d94a19cc54e1a0f36299b04467cfbaccf70316626f03dfd26f61","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-4738d2d3e61fb87a","operation":{"map":"A038279","operation":"basis_map"},"operation_detail":"A038279","conclusion_id":"n-c27b11147fce8bfa","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":"4b244726d9121dc4ca03b357f6e4402ca799039ef00dbacf4fbe461c025e0f32","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-e58c4cf54cd7c009","role":"sequence","name":"basis-map coefficients of Riordan array (1+2x,x(1+x)).","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-e58c4cf54cd7c009","role":"sequence","name":"basis-map coefficients of Riordan array (1+2x,x(1+x)).","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-fbfad365d270ad64","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-8\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-e58c4cf54cd7c009","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":"5a716c22bd66537ae05e6736086756b7730568bdc5aedcadd9c1737a165de25e","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"4"},"upper":{"closed":true,"value":"8"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-c27b11147fce8bfa","role":"sequence","name":"Riordan array (1+2x,x(1+x)).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-c27b11147fce8bfa","role":"sequence","name":"Riordan array (1+2x,x(1+x)).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4, 0]"},"chains":[{"edge":{"id":"e-5a8f629e61d609b9","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-c27b11147fce8bfa","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":"0d4c38a70084d94a19cc54e1a0f36299b04467cfbaccf70316626f03dfd26f61","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-71209083fd4bb877","operation":{"map":"A027467","operation":"basis_map"},"operation_detail":"A027467","conclusion_id":"n-c27b11147fce8bfa","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":"529c9d4d56aaae9416db163513c25291470618ee3250e5f11ad154fd1de48a63","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-8be1ba22f08cce79","role":"sequence","name":"basis-map coefficients of Riordan array (1+2x,x(1+x)).","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-8be1ba22f08cce79","role":"sequence","name":"basis-map coefficients of Riordan array (1+2x,x(1+x)).","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-1b92f65567f189e7","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-15\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-8be1ba22f08cce79","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":"17ac3e0d21d24e09e124cec4bab7d682dc16aae5c7e18354488d674aa394acf0","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"11"},"upper":{"closed":true,"value":"15"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-c27b11147fce8bfa","role":"sequence","name":"Riordan array (1+2x,x(1+x)).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-c27b11147fce8bfa","role":"sequence","name":"Riordan array (1+2x,x(1+x)).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4, 0]"},"chains":[{"edge":{"id":"e-5a8f629e61d609b9","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-c27b11147fce8bfa","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":"0d4c38a70084d94a19cc54e1a0f36299b04467cfbaccf70316626f03dfd26f61","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-719615516772b132","operation":{"map":"A007318","operation":"basis_map"},"operation_detail":"A007318","conclusion_id":"n-c27b11147fce8bfa","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":"0c60623b0d674a8c81ca0bd6dddf8ce7cca19e9af9509ad4715d42b020833e52","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-d2980b44b9e1faf3","role":"sequence","name":"basis-map coefficients of Riordan array (1+2x,x(1+x)).","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-d2980b44b9e1faf3","role":"sequence","name":"basis-map coefficients of Riordan array (1+2x,x(1+x)).","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-fa99d43ba99a1c05","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-1\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-d2980b44b9e1faf3","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":"c832a8b30b5725025e24d2152edada5569b212fa1fce10d996bb6be27cabe554","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-3"},"upper":{"closed":true,"value":"1"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-c27b11147fce8bfa","role":"sequence","name":"Riordan array (1+2x,x(1+x)).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-c27b11147fce8bfa","role":"sequence","name":"Riordan array (1+2x,x(1+x)).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4, 0]"},"chains":[{"edge":{"id":"e-5a8f629e61d609b9","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-c27b11147fce8bfa","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":"0d4c38a70084d94a19cc54e1a0f36299b04467cfbaccf70316626f03dfd26f61","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-94eaee4d49f2668d","operation":{"map":"A038243","operation":"basis_map"},"operation_detail":"A038243","conclusion_id":"n-c27b11147fce8bfa","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":"deafdfdd53b608d3e362d117fd32650b5cd6eb4167ebb561ebad718c32f4122b","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-3f406ce82de8647a","role":"sequence","name":"basis-map coefficients of Riordan array (1+2x,x(1+x)).","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-3f406ce82de8647a","role":"sequence","name":"basis-map coefficients of Riordan array (1+2x,x(1+x)).","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-32ad399df63f844d","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-5\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-3f406ce82de8647a","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":"706ea019b2eae3550a15e234d8eed422715d15d42aab3df24ba82233fb501807","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"1"},"upper":{"closed":true,"value":"5"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-c27b11147fce8bfa","role":"sequence","name":"Riordan array (1+2x,x(1+x)).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-c27b11147fce8bfa","role":"sequence","name":"Riordan array (1+2x,x(1+x)).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4, 0]"},"chains":[{"edge":{"id":"e-5a8f629e61d609b9","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-c27b11147fce8bfa","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":"0d4c38a70084d94a19cc54e1a0f36299b04467cfbaccf70316626f03dfd26f61","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-9b73612a2d328481","operation":{"map":"A027466","operation":"basis_map"},"operation_detail":"A027466","conclusion_id":"n-c27b11147fce8bfa","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":"47587bf7755993d167168c3bf31b3157433472e4f060c243401d63f4405497fd","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-2ae85de8aa2f7a20","role":"sequence","name":"basis-map coefficients of Riordan array (1+2x,x(1+x)).","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-2ae85de8aa2f7a20","role":"sequence","name":"basis-map coefficients of Riordan array (1+2x,x(1+x)).","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-921246387fcf3a1f","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-7\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-2ae85de8aa2f7a20","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":"5eb9a2d5947cb2f0c3f5208eeda4d3d945815394c7dffe4d6bec79ee9e8ba630","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"3"},"upper":{"closed":true,"value":"7"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-c27b11147fce8bfa","role":"sequence","name":"Riordan array (1+2x,x(1+x)).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-c27b11147fce8bfa","role":"sequence","name":"Riordan array (1+2x,x(1+x)).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4, 0]"},"chains":[{"edge":{"id":"e-5a8f629e61d609b9","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-c27b11147fce8bfa","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":"0d4c38a70084d94a19cc54e1a0f36299b04467cfbaccf70316626f03dfd26f61","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-a363e9242012bc21","operation":{"map":"A038231","operation":"basis_map"},"operation_detail":"A038231","conclusion_id":"n-c27b11147fce8bfa","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":"a54e62821c183a4e2df9d4eafafb239f0fd5c8ecc7392a28272276223cd21c9b","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-4f2b32a71818a295","role":"sequence","name":"basis-map coefficients of Riordan array (1+2x,x(1+x)).","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-4f2b32a71818a295","role":"sequence","name":"basis-map coefficients of Riordan array (1+2x,x(1+x)).","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-85e6814e89c84b8b","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-4\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-4f2b32a71818a295","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":"daee7b34b21759229482467ea3b09dc62f973b35807e532e87d8483a9d6f681e","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"0"},"upper":{"closed":true,"value":"4"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-c27b11147fce8bfa","role":"sequence","name":"Riordan array (1+2x,x(1+x)).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-c27b11147fce8bfa","role":"sequence","name":"Riordan array (1+2x,x(1+x)).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4, 0]"},"chains":[{"edge":{"id":"e-5a8f629e61d609b9","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-c27b11147fce8bfa","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":"0d4c38a70084d94a19cc54e1a0f36299b04467cfbaccf70316626f03dfd26f61","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-e5bdc121bd99907c","operation":{"map":"A038207","operation":"basis_map"},"operation_detail":"A038207","conclusion_id":"n-c27b11147fce8bfa","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":"cc80542b462f30fbefdab4e28b4d796b1edae5a61bb474f976d234c7c6dd73dd","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-317422c875f06510","role":"sequence","name":"basis-map coefficients of Riordan array (1+2x,x(1+x)).","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-317422c875f06510","role":"sequence","name":"basis-map coefficients of Riordan array (1+2x,x(1+x)).","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-e475554f8902db13","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-2\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-317422c875f06510","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":"54193afd8789490ff7ee15da0e2014e8e50bba7233ee9c0b25a748a99b6cdcd4","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"2"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-c27b11147fce8bfa","role":"sequence","name":"Riordan array (1+2x,x(1+x)).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-c27b11147fce8bfa","role":"sequence","name":"Riordan array (1+2x,x(1+x)).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4, 0]"},"chains":[{"edge":{"id":"e-5a8f629e61d609b9","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-c27b11147fce8bfa","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":"0d4c38a70084d94a19cc54e1a0f36299b04467cfbaccf70316626f03dfd26f61","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-e67dd89b1bcbf6c7","operation":{"map":"A038291","operation":"basis_map"},"operation_detail":"A038291","conclusion_id":"n-c27b11147fce8bfa","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":"c7105b1630ce849bea520d386b37d31ec928ebd05eb2cd82e87988a67e3ee293","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-0e47b6d43ddfe6ee","role":"sequence","name":"basis-map coefficients of Riordan array (1+2x,x(1+x)).","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-0e47b6d43ddfe6ee","role":"sequence","name":"basis-map coefficients of Riordan array (1+2x,x(1+x)).","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-77c8319978ad9839","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-9\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-0e47b6d43ddfe6ee","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":"9acb98e52bcc7baf544bbc1571f802ad0910ee57b9e2d7b3dc68b9b1901b1d76","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"5"},"upper":{"closed":true,"value":"9"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-c27b11147fce8bfa","role":"sequence","name":"Riordan array (1+2x,x(1+x)).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-c27b11147fce8bfa","role":"sequence","name":"Riordan array (1+2x,x(1+x)).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4, 0]"},"chains":[{"edge":{"id":"e-5a8f629e61d609b9","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-c27b11147fce8bfa","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":"0d4c38a70084d94a19cc54e1a0f36299b04467cfbaccf70316626f03dfd26f61","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-f9e5e2bc826d3dc0","operation":{"map":"A027465","operation":"basis_map"},"operation_detail":"A027465","conclusion_id":"n-c27b11147fce8bfa","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":"03d65c3b36ef224ccbffc98231f7410c4d8529acc804fef86c5653a689f11bfa","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-87e7c3f73bb81aac","role":"sequence","name":"basis-map coefficients of Riordan array (1+2x,x(1+x)).","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-87e7c3f73bb81aac","role":"sequence","name":"basis-map coefficients of Riordan array (1+2x,x(1+x)).","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-f73e26dac50fbf3d","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-3\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-87e7c3f73bb81aac","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":"20f81b317223a2aab5566929da949684cb75ed7ceb965832896e2915f1367f46","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-1"},"upper":{"closed":true,"value":"3"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-c27b11147fce8bfa","role":"sequence","name":"Riordan array (1+2x,x(1+x)).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-c27b11147fce8bfa","role":"sequence","name":"Riordan array (1+2x,x(1+x)).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-4, 0]"},"chains":[{"edge":{"id":"e-5a8f629e61d609b9","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-c27b11147fce8bfa","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":"0d4c38a70084d94a19cc54e1a0f36299b04467cfbaccf70316626f03dfd26f61","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]}]}]}],"truncated":false,"expanded":27}