{"chains":[{"edge":{"id":"e-2264f7a24faf3ec6","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"mobius\",\"a\":\"1\",\"b\":\"0\",\"c\":\"1\",\"e\":\"1\",\"schedule\":{\"first_index\":0,\"first_degree\":0,\"step\":1}}"},"operation_detail":"mobius, shift 0","conclusion_id":"n-716d3d94b0532646","premise_count":1,"theorem":"a real affine substitution x -> a x + b (a != 0), the reversal x^d p(1/x) (d >= deg p) and a real Mobius map (c x + e)^d p((a x + b)/(c x + e)) (a e - b c != 0, d >= deg p) map real roots to real roots: a root r of p gives the root (r - b)/a, 1/r (and 0) or (e r - b)/(a - c r) (and -e/c); for an input row that is a polynomial the degree condition holds automatically","lean_route":"fTransform","lean_declarations":["RealRooted.splits_fPolynomial"],"certificate_hash":"6a2ce3a1f6dd9aafc877c8d46ff139dc3c7034293eb17ba169179c7691d5602a","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":true,"value":"-1"},"upper":{"closed":true,"value":"0"}}}],"premises":[{"position":0,"node_id":"n-55c2b7e431107e43","role":"sequence","name":"basis_map_A013609 of 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-55c2b7e431107e43","role":"sequence","name":"basis_map_A013609 of 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-1a65135df7496975","operation":{"map":"A013609","operation":"basis_map"},"operation_detail":"A013609","conclusion_id":"n-55c2b7e431107e43","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":"76acf7d0467269c62b2fe37c1e72ad524152b1baa774dae5eed7b359b481b92a","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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-44818b0078c36afb","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":"04e11476c20d784b1f2c1ce2ecf0336a62b6f3d40ec865adb3d355db1920605b","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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-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-5cca7f04a77cbd96","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":"032b275d66d13353897f6cbd39936b9077cbca06149f7144bba795422d991217","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"repeat":true,"premises":[]}]}]},{"edge":{"id":"e-6d904904d3e4d8b9","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":"4245567621bee893cb5e5c89e2af0703f9865f4d57ca88b7f9b070c1d0b2c0f6","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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-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-77e35b34a60259fd","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":"71f3b44d9a387cf5a17cc059227e9e9af8cdc34b48c0b3584066f996ca49ab1a","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"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-929f94ef15e51b44","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":"f7a65afe17dd30c12ed3e25d35aa24f3d66f305a53b7e387807fc7b5a7b67593","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"repeat":true,"premises":[]}]}]},{"edge":{"id":"e-9fc5379559392366","operation":{"operation":"theorem_check","theorem":"liu_wang_three_term"},"operation_detail":"liu_wang_three_term","conclusion_id":"n-f5a001953ee28e8f","premise_count":0,"theorem":"L. L. Liu and Y. Wang, Adv. Appl. Math. 38 (2007) 542-560, Theorem 2.1 and Corollary 2.4 (A unified approach to polynomial sequences with only real zeros; the lag row as the interlacer, b_n = 0), weak interlacing of consecutive rows, with nonnegativity of the coefficients replaced, where a root region is certified, by an exact root-location induction","lean_route":"sign","lean_declarations":["RealRooted.threeTerm_interlaces_of_nonnegCoeffs","RealRooted.threeTerm_interlaces","RealRooted.threeTerm_hasNonnegCoeffs"],"certificate_hash":"4aff548277f139d022b3448468dcdb50d2c540f707295eac4e466a414ed55ab2","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"premises":[]},{"edge":{"id":"e-ab6304809ddce2f2","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":"6779c02b746856d12ff837c1cc7b6ac0e9d7453930c76296abd285b9ab43bf48","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"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]"}]},"repeat":true,"premises":[]}]}]},{"edge":{"id":"e-bf9f6d4d21603526","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":"67ef090415a86bece16368e74066288450c4f8f560b4f72fa95b48a3e0ce3e4a","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"repeat":true,"premises":[]}]}]},{"edge":{"id":"e-c0ed4179820a0fae","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":"74a0dc438fa4a9c3430476ff566803a699ab6372317b218c1115b8398a705ec2","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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-c129a9d1cd986a33","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":"e1ab2be877771d49f63161285e28fa31752cb929c4c59a980d5c12d62c7eb79f","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"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]"}]},"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]"}]},"repeat":true,"premises":[]}]}]},{"edge":{"id":"e-e8a9756a3597a938","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":"7375a75a2cbb42a8504d276f4332cefb36c7a1548543bca5d4375610eb43c69f","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"repeat":true,"premises":[]}]}]},{"edge":{"id":"e-e9092500340f951b","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":"f2c3f8d9a1c724d3ed47b93c064b3180ef9111f452ede9997c08395855b4216c","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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":[]}]}]}]}]},{"edge":{"id":"e-ef84c8a758761468","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":"d3d5dc1c90414e28ca0c983afacdb2347a43715195c761475a4b0e76e6f9ca20","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"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]"}]},"repeat":true,"premises":[]}]}]}]}]},{"edge":{"id":"e-6a0666d85481949f","operation":{"map":"A013609","operation":"basis_map"},"operation_detail":"A013609","conclusion_id":"n-55c2b7e431107e43","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":"ced430e47484e5083e4be76dedc9cf3edaeb039a1da20e4c1babec7a7c2958e9","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"repeat":true,"premises":[]},{"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-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]"}]},"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]"}]},"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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-44818b0078c36afb","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":"04e11476c20d784b1f2c1ce2ecf0336a62b6f3d40ec865adb3d355db1920605b","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-5cca7f04a77cbd96","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":"032b275d66d13353897f6cbd39936b9077cbca06149f7144bba795422d991217","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-6d904904d3e4d8b9","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":"4245567621bee893cb5e5c89e2af0703f9865f4d57ca88b7f9b070c1d0b2c0f6","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"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]"}]},"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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-77e35b34a60259fd","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":"71f3b44d9a387cf5a17cc059227e9e9af8cdc34b48c0b3584066f996ca49ab1a","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-929f94ef15e51b44","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":"f7a65afe17dd30c12ed3e25d35aa24f3d66f305a53b7e387807fc7b5a7b67593","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-9fc5379559392366","operation":{"operation":"theorem_check","theorem":"liu_wang_three_term"},"operation_detail":"liu_wang_three_term","conclusion_id":"n-f5a001953ee28e8f","premise_count":0,"theorem":"L. L. Liu and Y. Wang, Adv. Appl. Math. 38 (2007) 542-560, Theorem 2.1 and Corollary 2.4 (A unified approach to polynomial sequences with only real zeros; the lag row as the interlacer, b_n = 0), weak interlacing of consecutive rows, with nonnegativity of the coefficients replaced, where a root region is certified, by an exact root-location induction","lean_route":"sign","lean_declarations":["RealRooted.threeTerm_interlaces_of_nonnegCoeffs","RealRooted.threeTerm_interlaces","RealRooted.threeTerm_hasNonnegCoeffs"],"certificate_hash":"4aff548277f139d022b3448468dcdb50d2c540f707295eac4e466a414ed55ab2","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]},{"edge":{"id":"e-ab6304809ddce2f2","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":"6779c02b746856d12ff837c1cc7b6ac0e9d7453930c76296abd285b9ab43bf48","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-bf9f6d4d21603526","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":"67ef090415a86bece16368e74066288450c4f8f560b4f72fa95b48a3e0ce3e4a","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-c0ed4179820a0fae","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":"74a0dc438fa4a9c3430476ff566803a699ab6372317b218c1115b8398a705ec2","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-c129a9d1cd986a33","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":"e1ab2be877771d49f63161285e28fa31752cb929c4c59a980d5c12d62c7eb79f","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"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]"}]},"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]"}]},"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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-e8a9756a3597a938","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":"7375a75a2cbb42a8504d276f4332cefb36c7a1548543bca5d4375610eb43c69f","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-e9092500340f951b","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":"f2c3f8d9a1c724d3ed47b93c064b3180ef9111f452ede9997c08395855b4216c","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-ef84c8a758761468","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":"d3d5dc1c90414e28ca0c983afacdb2347a43715195c761475a4b0e76e6f9ca20","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"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]"}]},"repeat":true,"premises":[]}]}]},{"edge":{"id":"e-76d46a3bbdce7b63","operation":{"map":"A013609","operation":"basis_map"},"operation_detail":"A013609","conclusion_id":"n-55c2b7e431107e43","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":"ec353014e7b6a621e49b9c0ebf3f1181a5123fc7344ac4ad0e11d39627bc3455","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]"}]},"repeat":true,"premises":[]},{"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-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]"}]},"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]"}]},"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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-44818b0078c36afb","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":"04e11476c20d784b1f2c1ce2ecf0336a62b6f3d40ec865adb3d355db1920605b","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-5cca7f04a77cbd96","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":"032b275d66d13353897f6cbd39936b9077cbca06149f7144bba795422d991217","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-6d904904d3e4d8b9","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":"4245567621bee893cb5e5c89e2af0703f9865f4d57ca88b7f9b070c1d0b2c0f6","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"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]"}]},"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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-77e35b34a60259fd","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":"71f3b44d9a387cf5a17cc059227e9e9af8cdc34b48c0b3584066f996ca49ab1a","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-929f94ef15e51b44","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":"f7a65afe17dd30c12ed3e25d35aa24f3d66f305a53b7e387807fc7b5a7b67593","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-9fc5379559392366","operation":{"operation":"theorem_check","theorem":"liu_wang_three_term"},"operation_detail":"liu_wang_three_term","conclusion_id":"n-f5a001953ee28e8f","premise_count":0,"theorem":"L. L. Liu and Y. Wang, Adv. Appl. Math. 38 (2007) 542-560, Theorem 2.1 and Corollary 2.4 (A unified approach to polynomial sequences with only real zeros; the lag row as the interlacer, b_n = 0), weak interlacing of consecutive rows, with nonnegativity of the coefficients replaced, where a root region is certified, by an exact root-location induction","lean_route":"sign","lean_declarations":["RealRooted.threeTerm_interlaces_of_nonnegCoeffs","RealRooted.threeTerm_interlaces","RealRooted.threeTerm_hasNonnegCoeffs"],"certificate_hash":"4aff548277f139d022b3448468dcdb50d2c540f707295eac4e466a414ed55ab2","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"previous_interlaces_next"}],"premises":[]},"repeat":true,"premises":[]},{"edge":{"id":"e-ab6304809ddce2f2","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":"6779c02b746856d12ff837c1cc7b6ac0e9d7453930c76296abd285b9ab43bf48","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-bf9f6d4d21603526","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":"67ef090415a86bece16368e74066288450c4f8f560b4f72fa95b48a3e0ce3e4a","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-c0ed4179820a0fae","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":"74a0dc438fa4a9c3430476ff566803a699ab6372317b218c1115b8398a705ec2","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-c129a9d1cd986a33","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":"e1ab2be877771d49f63161285e28fa31752cb929c4c59a980d5c12d62c7eb79f","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"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]"}]},"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]"}]},"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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-e8a9756a3597a938","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":"7375a75a2cbb42a8504d276f4332cefb36c7a1548543bca5d4375610eb43c69f","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-e9092500340f951b","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":"f2c3f8d9a1c724d3ed47b93c064b3180ef9111f452ede9997c08395855b4216c","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"repeat":true,"premises":[]},{"edge":{"id":"e-ef84c8a758761468","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":"d3d5dc1c90414e28ca0c983afacdb2347a43715195c761475a4b0e76e6f9ca20","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-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]"}]},"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]"}]},"repeat":true,"premises":[]}]}]}]}]}],"truncated":false,"expanded":43}