{"chains":[{"edge":{"id":"e-3006d34f722f9e52","operation":{"index_shift":0,"modulus":2,"operation":"veronese_section","residue":1},"operation_detail":"r=2, j=1, shift 0","conclusion_id":"n-b8a5d3147cb58db8","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":"a435da14a37941a8e9e82051f08564d4eb69d32fe580d1d185a541aec7175f6f","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-f5a001953ee28e8f","role":"sequence","name":"Riordan array (1, 2+2x).","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-f5a001953ee28e8f","role":"sequence","name":"Riordan array (1, 2+2x).","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-52040eb0dce100d3","operation":{"map":"A099040","operation":"basis_map"},"operation_detail":"A099040","conclusion_id":"n-f5a001953ee28e8f","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":"6004cbc07b40660b83e46fa01e6bbefc3348ab216adb17c05c3375c177f8c3f0","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":true,"value":"-2"},"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-17786677d2ed021b","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-f5a001953ee28e8f","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":"a944ec45bd0de2697d038c466e0b705b9faabf23f4168cf1985db37880561566","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"premises":[]},{"edge":{"id":"e-0a457ba83443136e","operation":{"map":"A027467","operation":"basis_map"},"operation_detail":"A027467","conclusion_id":"n-f5a001953ee28e8f","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":"1fee33094386ee0179ffb93630544802bc014e29366128b82c968311866f455f","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-22b2bd96c59e3f63","role":"sequence","name":"basis-map coefficients of Riordan array (1, 2+2x).","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-22b2bd96c59e3f63","role":"sequence","name":"basis-map coefficients of Riordan array (1, 2+2x).","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-48e4dfa7d694f880","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-15\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-22b2bd96c59e3f63","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":"342a8638c7f83146823bfaabaf47f0f1fda200e4929646b2d27b7e8812a904a6","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"13"},"upper":{"closed":true,"value":"15"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-f5a001953ee28e8f","role":"sequence","name":"Riordan array (1, 2+2x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-2, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-f5a001953ee28e8f","role":"sequence","name":"Riordan array (1, 2+2x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-2, 0]"},"chains":[{"edge":{"id":"e-17786677d2ed021b","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-f5a001953ee28e8f","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":"a944ec45bd0de2697d038c466e0b705b9faabf23f4168cf1985db37880561566","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-162624a94908f408","operation":{"map":"A038255","operation":"basis_map"},"operation_detail":"A038255","conclusion_id":"n-f5a001953ee28e8f","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":"9f2345717bb21545ac2d14132063a504f7589104d2dba6b9a19d77c5f3c64a50","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-7ab73c0941700e0f","role":"sequence","name":"basis-map coefficients of Riordan array (1, 2+2x).","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-7ab73c0941700e0f","role":"sequence","name":"basis-map coefficients of Riordan array (1, 2+2x).","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-79e1a4a5e521405c","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-6\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-7ab73c0941700e0f","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":"0fcd48ba290bafbfbc9a6ae682cd1a15802dacf030a79889cdd2b2ed779b6319","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"4"},"upper":{"closed":true,"value":"6"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-f5a001953ee28e8f","role":"sequence","name":"Riordan array (1, 2+2x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-2, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-f5a001953ee28e8f","role":"sequence","name":"Riordan array (1, 2+2x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-2, 0]"},"chains":[{"edge":{"id":"e-17786677d2ed021b","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-f5a001953ee28e8f","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":"a944ec45bd0de2697d038c466e0b705b9faabf23f4168cf1985db37880561566","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-3f03a2606d2e6662","operation":{"map":"A027466","operation":"basis_map"},"operation_detail":"A027466","conclusion_id":"n-f5a001953ee28e8f","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":"3df4567aa9c3e5b24cda202e83d840606920db95130c022d251dc0a5384edae7","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-fd1f27ef1d8123fd","role":"sequence","name":"basis-map coefficients of Riordan array (1, 2+2x).","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-fd1f27ef1d8123fd","role":"sequence","name":"basis-map coefficients of Riordan array (1, 2+2x).","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-5e00209341210844","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-7\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-fd1f27ef1d8123fd","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":"3c805243d2abd1d08f2cfb5fa614aacaa53f18120fba8c0af7eaca24bc2f5121","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"5"},"upper":{"closed":true,"value":"7"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-f5a001953ee28e8f","role":"sequence","name":"Riordan array (1, 2+2x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-2, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-f5a001953ee28e8f","role":"sequence","name":"Riordan array (1, 2+2x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-2, 0]"},"chains":[{"edge":{"id":"e-17786677d2ed021b","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-f5a001953ee28e8f","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":"a944ec45bd0de2697d038c466e0b705b9faabf23f4168cf1985db37880561566","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-532ccda39f04a0f0","operation":{"map":"A038303","operation":"basis_map"},"operation_detail":"A038303","conclusion_id":"n-f5a001953ee28e8f","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":"f6ff3b8d6ab0d4da0a06173c07812c30d8dfd364a51763d811734ab2025c5d74","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-dd0db9eabdf2db44","role":"sequence","name":"basis-map coefficients of Riordan array (1, 2+2x).","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-dd0db9eabdf2db44","role":"sequence","name":"basis-map coefficients of Riordan array (1, 2+2x).","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-c2f106499058af8f","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-10\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-dd0db9eabdf2db44","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":"5dfc9d69c940dfa25d99e26c565815f2f80ceeb8c25d84f8b656fe0687016506","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"8"},"upper":{"closed":true,"value":"10"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-f5a001953ee28e8f","role":"sequence","name":"Riordan array (1, 2+2x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-2, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-f5a001953ee28e8f","role":"sequence","name":"Riordan array (1, 2+2x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-2, 0]"},"chains":[{"edge":{"id":"e-17786677d2ed021b","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-f5a001953ee28e8f","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":"a944ec45bd0de2697d038c466e0b705b9faabf23f4168cf1985db37880561566","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-72107609b2d5e6bc","operation":{"map":"A038207","operation":"basis_map"},"operation_detail":"A038207","conclusion_id":"n-f5a001953ee28e8f","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":"fc45acfd161ab415233e62a87bbb5f21876171bd42bfefc50386875f77249299","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-40f758b5452c976a","role":"sequence","name":"basis-map coefficients of Riordan array (1, 2+2x).","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-40f758b5452c976a","role":"sequence","name":"basis-map coefficients of Riordan array (1, 2+2x).","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-8c4e4f825f4ab306","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-2\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-40f758b5452c976a","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":"546e1143a4113313e04f31883d8b281e113d1ae71c272a9b4bfcc8395d1a2ba0","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"0"},"upper":{"closed":true,"value":"2"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-f5a001953ee28e8f","role":"sequence","name":"Riordan array (1, 2+2x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-2, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-f5a001953ee28e8f","role":"sequence","name":"Riordan array (1, 2+2x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-2, 0]"},"chains":[{"edge":{"id":"e-17786677d2ed021b","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-f5a001953ee28e8f","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":"a944ec45bd0de2697d038c466e0b705b9faabf23f4168cf1985db37880561566","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-763de8a298cf812d","operation":{"map":"A038243","operation":"basis_map"},"operation_detail":"A038243","conclusion_id":"n-f5a001953ee28e8f","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":"0358c294c80649627e60f3f71130e9a3feb0676f1c7065059217239dc00e8085","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-af83e10a056d6f29","role":"sequence","name":"basis-map coefficients of Riordan array (1, 2+2x).","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-af83e10a056d6f29","role":"sequence","name":"basis-map coefficients of Riordan array (1, 2+2x).","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-bdc3e5aca0457f81","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-5\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-af83e10a056d6f29","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":"a021cd6c7e87784e813188cb76cb8b4712f804cc9b64de14efe871fc41b40ef3","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"3"},"upper":{"closed":true,"value":"5"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-f5a001953ee28e8f","role":"sequence","name":"Riordan array (1, 2+2x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-2, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-f5a001953ee28e8f","role":"sequence","name":"Riordan array (1, 2+2x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-2, 0]"},"chains":[{"edge":{"id":"e-17786677d2ed021b","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-f5a001953ee28e8f","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":"a944ec45bd0de2697d038c466e0b705b9faabf23f4168cf1985db37880561566","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-8232f658d776d13c","operation":{"map":"A038279","operation":"basis_map"},"operation_detail":"A038279","conclusion_id":"n-f5a001953ee28e8f","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":"363bc819b734c9c230aa6a40a3ad4d485d8b3e1ac0213c871d1c2d5b58fab0cc","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-e10282c2431b31a3","role":"sequence","name":"basis-map coefficients of Riordan array (1, 2+2x).","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-e10282c2431b31a3","role":"sequence","name":"basis-map coefficients of Riordan array (1, 2+2x).","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-4478346993b2c814","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-8\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-e10282c2431b31a3","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":"4d8fba28eabe75d2584e3e405496ac6e305957f661391d34a09ffb6fd6cedeb6","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"6"},"upper":{"closed":true,"value":"8"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-f5a001953ee28e8f","role":"sequence","name":"Riordan array (1, 2+2x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-2, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-f5a001953ee28e8f","role":"sequence","name":"Riordan array (1, 2+2x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-2, 0]"},"chains":[{"edge":{"id":"e-17786677d2ed021b","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-f5a001953ee28e8f","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":"a944ec45bd0de2697d038c466e0b705b9faabf23f4168cf1985db37880561566","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-af79ef336fd9f8da","operation":{"map":"A027465","operation":"basis_map"},"operation_detail":"A027465","conclusion_id":"n-f5a001953ee28e8f","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":"cd653b202d69c8f546dce01fa0ddbc7ce54fa71c4c8ac29cedb290ba505b9b27","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-b59b1769d0dc40fc","role":"sequence","name":"basis-map coefficients of Riordan array (1, 2+2x).","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-b59b1769d0dc40fc","role":"sequence","name":"basis-map coefficients of Riordan array (1, 2+2x).","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-319b2a76ea6c1ab0","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-3\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-b59b1769d0dc40fc","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":"645609b74b314a982fdd6e74564ef145804c84f619b0afd737007dfe914e36ab","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-f5a001953ee28e8f","role":"sequence","name":"Riordan array (1, 2+2x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-2, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-f5a001953ee28e8f","role":"sequence","name":"Riordan array (1, 2+2x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-2, 0]"},"chains":[{"edge":{"id":"e-17786677d2ed021b","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-f5a001953ee28e8f","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":"a944ec45bd0de2697d038c466e0b705b9faabf23f4168cf1985db37880561566","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-c3d762863d6658d7","operation":{"map":"A038291","operation":"basis_map"},"operation_detail":"A038291","conclusion_id":"n-f5a001953ee28e8f","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":"f17276cddb4c6bc56e350c2892fc5af62b11ea0070a16f20e0ca6218e1e70f29","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-192a0153bc9ffe91","role":"sequence","name":"basis-map coefficients of Riordan array (1, 2+2x).","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-192a0153bc9ffe91","role":"sequence","name":"basis-map coefficients of Riordan array (1, 2+2x).","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-b9371054cfe1d371","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-9\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-192a0153bc9ffe91","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":"19a84d8f33423ebc1b1a94e7c2e83ad60c2aa873240d6a7d2322e9b0e5cfefcb","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"7"},"upper":{"closed":true,"value":"9"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-f5a001953ee28e8f","role":"sequence","name":"Riordan array (1, 2+2x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-2, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-f5a001953ee28e8f","role":"sequence","name":"Riordan array (1, 2+2x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-2, 0]"},"chains":[{"edge":{"id":"e-17786677d2ed021b","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-f5a001953ee28e8f","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":"a944ec45bd0de2697d038c466e0b705b9faabf23f4168cf1985db37880561566","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-e158703ce212fb71","operation":{"map":"A007318","operation":"basis_map"},"operation_detail":"A007318","conclusion_id":"n-f5a001953ee28e8f","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":"5b9b7a7849bb3e46f06566abe8df51cb2a2dc92e2d108c8d2e3c4f6e3799525d","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-5b8743d4a9a28750","role":"sequence","name":"basis-map coefficients of Riordan array (1, 2+2x).","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-5b8743d4a9a28750","role":"sequence","name":"basis-map coefficients of Riordan array (1, 2+2x).","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-dc7a132d665751c2","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-1\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-5b8743d4a9a28750","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":"10b93866a9bbf9cd0743348a01e9f29115635c06cc9d4ec6057747441f845ea1","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-1"},"upper":{"closed":true,"value":"1"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-f5a001953ee28e8f","role":"sequence","name":"Riordan array (1, 2+2x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-2, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-f5a001953ee28e8f","role":"sequence","name":"Riordan array (1, 2+2x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-2, 0]"},"chains":[{"edge":{"id":"e-17786677d2ed021b","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-f5a001953ee28e8f","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":"a944ec45bd0de2697d038c466e0b705b9faabf23f4168cf1985db37880561566","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-e36b44dfb8fba667","operation":{"map":"A038231","operation":"basis_map"},"operation_detail":"A038231","conclusion_id":"n-f5a001953ee28e8f","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":"8d40b2ce811109dec755c350f6512120223006a98c1a0c8635e26ec39ca3132c","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-7ca53e27e17e7a26","role":"sequence","name":"basis-map coefficients of Riordan array (1, 2+2x).","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-7ca53e27e17e7a26","role":"sequence","name":"basis-map coefficients of Riordan array (1, 2+2x).","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-23d8b9b067cbe12f","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-4\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-7ca53e27e17e7a26","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":"18397caa7ee82fe43d996c46fcba03f0d09f568442796e5e9f9e5a7feebc0879","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"2"},"upper":{"closed":true,"value":"4"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-f5a001953ee28e8f","role":"sequence","name":"Riordan array (1, 2+2x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-2, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-f5a001953ee28e8f","role":"sequence","name":"Riordan array (1, 2+2x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-2, 0]"},"chains":[{"edge":{"id":"e-17786677d2ed021b","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-f5a001953ee28e8f","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":"a944ec45bd0de2697d038c466e0b705b9faabf23f4168cf1985db37880561566","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-ffeb0648278e3cee","operation":{"map":"A038327","operation":"basis_map"},"operation_detail":"A038327","conclusion_id":"n-f5a001953ee28e8f","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":"5458c0ee6091d4982444f5e45c1c5218565eee4f67ba4fbb1d069137258a030c","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-6d02eb83391908c0","role":"sequence","name":"basis-map coefficients of Riordan array (1, 2+2x).","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-6d02eb83391908c0","role":"sequence","name":"basis-map coefficients of Riordan array (1, 2+2x).","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-1000187f132dd1ea","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"-12\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-6d02eb83391908c0","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":"3dfdbfd55dcb0841976a9c8bac6d1d14053d6eff1a904f7da3796ed6c25821f0","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"10"},"upper":{"closed":true,"value":"12"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-f5a001953ee28e8f","role":"sequence","name":"Riordan array (1, 2+2x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-2, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-f5a001953ee28e8f","role":"sequence","name":"Riordan array (1, 2+2x).","uses":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-2, 0]"},"chains":[{"edge":{"id":"e-17786677d2ed021b","operation":{"operation":"theorem_check","theorem":"ma_wang_interval"},"operation_detail":"ma_wang_interval","conclusion_id":"n-f5a001953ee28e8f","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":"a944ec45bd0de2697d038c466e0b705b9faabf23f4168cf1985db37880561566","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":false,"value":"-2"},"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]}]}]}]}]}]}]}],"truncated":false,"expanded":27}