{"kind":"theorem_check","report":{"conclusion":{"first_index":0,"interlacing":"weak","interlacing_from":1,"root_region":{"lower":{"closed":false,"value":"-8"},"upper":{"closed":true,"value":"0"}},"simple_roots":false,"statement":"every P_n, n >= 0, is nonzero and real-rooted with every root in (-8, 0]; deg P_n = deg P_(n-1) + 1 and P_(n-1) interlaces P_n (Ma--Wang) for n >= 1"},"hypotheses":[{"evidence":"f(n) = n != 0 for every integer n in [1, +inf) (exact; Taylor shift: the coefficients of f(n) = n at n = 1 + 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":["0","1"],"range":{"first":"1","last":null}},"decision":"holds"},"statement":"the left-hand factor f(n) is nonzero for every n >= 1","status":{"kind":"verified"}},{"evidence":"P_0 has degree 0, the root -8 with multiplicity 0 and the root 0 with multiplicity 0; checked exactly","name":"seed_roots_in_interval","statement":"P_0 is nonzero and real-rooted with every root in [-8, 0]","status":{"kind":"verified"}},{"evidence":"a_n = 1 > 0 for every integer n in [1, +inf) (exact; Taylor shift: the coefficients of a_n = 1 at n = 1 + 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":"1","last":null}},"decision":"holds"},"statement":"a_n = [x^1] c_0(n, x) / gamma(n) > 0 for every n >= 1 (the coefficient a of the normalized step, so deg P_n = deg P_(n-1) + 1)","status":{"kind":"verified"}},{"evidence":"no hit before n = 1; lattice argument from n = 1 (multiplicity 0): e(n) = -1/2 n + 1/2 is affine with slope -1/2 and 1/1/2 = 2 is an integer, and E(1) = 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' >= 1, with a hit every 2 steps","name":"upper_endpoint_threshold","statement":"E(n) = e(n) + m(n) >= 0 for every n >= 1, with e(n) = -1/2 n + 1/2 at the end U = 0, m(1) = 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 = 1; from n = 1 on (multiplicity 0): e(n) + 0 = 1/2 n + 1/2 >= 0 for every integer n in [1, +inf) (exact; Taylor shift: the coefficients of e(n) + 0 = 1/2 n + 1/2 at n = 1 + 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":["1/2","1/2"],"range":{"first":"1","last":null}},"decision":"holds"},"statement":"E(n) = e(n) + m(n) >= 0 for every n >= 1, with e(n) = 1/2 n + 1/2 at the end L = -8, m(1) = 0 the multiplicity of L = -8 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 >= 1, with L = -8, U = 0, alpha_n = (1)/(n), beta_n = (-4 n + 4)/(n), kappa_n = (1)/(n)","recurrence":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"denominator":{"coeffs":[["0"],["1"]]},"terms":[{"coeff":{"coeffs":[["4","1"],["-4","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","8","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"}}