{"kind":"theorem_check","report":{"conclusion":{"first_index":1,"interlacing":"weak","interlacing_from":2,"root_region":{"lower":{"closed":false,"value":"-1"},"upper":{"closed":true,"value":"0"}},"simple_roots":false,"statement":"every P_n, n >= 1, is nonzero and real-rooted with every root in (-1, 0]; deg P_n = deg P_(n-1) + 1 and P_(n-1) interlaces P_n (Ma--Wang) for n >= 2"},"hypotheses":[{"evidence":"P_1 has degree 0, the root -1 with multiplicity 0 and the root 0 with multiplicity 0; checked exactly","name":"seed_roots_in_interval","statement":"P_1 is nonzero and real-rooted with every root in [-1, 0]","status":{"kind":"verified"}},{"evidence":"a_n = n - 1 > 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of a_n = n - 1 at n = 2 + u have one sign)","name":"slope_positive","sign_decision":{"certificate":{"condition":"positive","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1","1"]},"numerator":["-1","1"],"range":{"first":"2","last":null}},"decision":"holds"},"statement":"a_n = [x^1] c_0(n, x) / gamma(n) > 0 for every n >= 2 (the coefficient a of the normalized step, so deg P_n = deg P_(n-1) + 1)","status":{"kind":"verified"}},{"evidence":"no hit before n = 2; from n = 2 on (multiplicity 0): e(n) + 0 = 0 >= 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of e(n) + 0 = 0 at n = 2 + u have one sign)","name":"upper_endpoint_threshold","sign_decision":{"certificate":{"condition":"nonnegative","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":[]},"numerator":[],"range":{"first":"2","last":null}},"decision":"holds"},"statement":"E(n) = e(n) + m(n) >= 0 for every n >= 2, with e(n) = 0 at the end U = 0, m(2) = 0 the multiplicity of U = 0 in the last seed, and m raised by one after every n with E(n) = 0","status":{"kind":"verified"}},{"evidence":"no hit before n = 2; from n = 2 on (multiplicity 0): e(n) + 0 = n - 1 >= 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of e(n) + 0 = n - 1 at n = 2 + u have one sign)","name":"lower_endpoint_threshold","sign_decision":{"certificate":{"condition":"nonnegative","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1","1"]},"numerator":["-1","1"],"range":{"first":"2","last":null}},"decision":"holds"},"statement":"E(n) = e(n) + m(n) >= 0 for every n >= 2, with e(n) = n - 1 at the end L = -1, m(2) = 0 the multiplicity of L = -1 in the last seed, and m raised by one after every n with E(n) = 0","status":{"kind":"verified"}}],"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"],"lean_replay":"not_attempted","normal_form":"P_n = (alpha_n x + beta_n) P_(n-1) + kappa_n (x - L)(x - U) P'_(n-1) for n >= 2, with L = -1, U = 0, alpha_n = n - 1, beta_n = 0, kappa_n = 1","recurrence":{"first_index":1,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["0","-1"],["0","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","1","1"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"reference":"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","schema":"polytool.recurrence-real-rootedness-theorem.v1","status":"proved","theorem":"ma_wang_interval"}}