{"kind":"theorem_check","report":{"conclusion":{"first_index":1,"interlacing":"weak","interlacing_from":2,"root_region":{"lower":{"closed":false,"value":"-4"},"upper":{"closed":true,"value":"0"}},"simple_roots":false,"statement":"every P_n, n >= 1, is nonzero and real-rooted with every root in (-4, 0]; deg P_n = deg P_(n-1) + 1 and P_(n-1) interlaces P_n (Ma--Wang) for n >= 2"},"hypotheses":[{"evidence":"f(n) = n - 1 != 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of f(n) = n - 1 at n = 2 + u have one sign)","name":"left_factor_nonzero","sign_decision":{"certificate":{"condition":"nonzero","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1","1"]},"numerator":["-1","1"],"range":{"first":"2","last":null}},"decision":"holds"},"statement":"the left-hand factor f(n) is nonzero for every n >= 2","status":{"kind":"verified"}},{"evidence":"P_1 has degree 0, the root -4 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 [-4, 0]","status":{"kind":"verified"}},{"evidence":"a_n = 1 > 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of a_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"]},"numerator":["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; lattice argument from n = 2 (multiplicity 0): e(n) = -1/2 n + 1 is affine with slope -1/2 and 1/1/2 = 2 is an integer, and E(2) = 0 is a nonnegative multiple of 1/2; E drops by 1/2 per step and returns from 0 to 1/2 after each hit, so E(n') >= 0 for every n' >= 2, with a hit every 2 steps","name":"upper_endpoint_threshold","statement":"E(n) = e(n) + m(n) >= 0 for every n >= 2, with e(n) = -1/2 n + 1 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 = 1/2 n >= 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of e(n) + 0 = 1/2 n 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/2"]},"numerator":["0","1/2"],"range":{"first":"2","last":null}},"decision":"holds"},"statement":"E(n) = e(n) + m(n) >= 0 for every n >= 2, with e(n) = 1/2 n at the end L = -4, m(2) = 0 the multiplicity of L = -4 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 = -4, U = 0, alpha_n = (1)/(n - 1), beta_n = (-2 n + 4)/(n - 1), kappa_n = (1)/(n - 1)","recurrence":{"first_index":1,"initial_polynomials":[["1"]],"recurrence":{"denominator":{"coeffs":[["-1"],["1"]]},"terms":[{"coeff":{"coeffs":[["4","1"],["-2","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","4","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"}}