{"kind":"basis_map_theorem","report":{"basis":{"first_index":1,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","1","1"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"basis_name":"Triangle of numbers T(n,k) = k!*Stirling2(n,k) read by rows (n >= 1, 1 <= k <= n).","conclusions":[{"hypotheses":["kappa_positive","top_coefficient_positive","initial_row_roots"],"input_interval":{"lower":{"closed":true,"value":{"lower_bound":"-1","radicand":"1","rational_part":"-1","sqrt_coefficient":"0","text":"-1","upper_bound":"-1"}},"upper":{"closed":true,"value":{"lower_bound":"1","radicand":"1","rational_part":"1","sqrt_coefficient":"0","text":"1","upper_bound":"1"}}},"nonnegative_coefficients":true,"output_interval":{"lower":{"closed":true,"value":{"lower_bound":"-1","radicand":"1","rational_part":"-1","sqrt_coefficient":"0","text":"-1","upper_bound":"-1"}},"upper":{"closed":true,"value":{"lower_bound":"0","radicand":"1","rational_part":"0","sqrt_coefficient":"0","text":"0","upper_bound":"0"}}},"sharp":true,"statement":"source [-1, 1], target [-1, 0]"}],"hypotheses":[{"evidence":"exact","name":"kappa_positive","statement":"kappa > 0","status":{"kind":"verified"}},{"evidence":"exact","name":"top_coefficient_positive","statement":"b + kappa deg g = 2 > 0","status":{"kind":"verified"}},{"evidence":"exact root isolation","name":"initial_row_roots","statement":"g = P_0 is nonzero and real-rooted with every root in [-1, 0]","status":{"kind":"verified"}}],"lean_declarations":["RealRooted.intervalBasisMap_maps_realRootedIn_iff"],"lean_replay":"not_attempted","schema":"polytool.recurrence-basis-map-theorem.v1","shape":{"a":"1","b":"2","initial_row":["1"],"kappa":"1","kind":"interval_differential","lower_root":"-1","upper_root":"0"},"status":"proved","theorem":"interval basis maps: for L f = (a + b t) f + kappa (t - l)(t - h) f', l < h, kappa > 0, b + kappa deg g > 0, and g with positive leading coefficient, real-rooted in [l, h] with endpoint multiplicities m_l, m_h, T(u^k) = L^k g sends every real polynomial with all roots in S to one with all roots in [l, h] if and only if S lies in [a + b l - kappa (h - l) m_l, a + b h + kappa (h - l) m_h] (RealRooted intervalBasisMap_maps_realRootedIn_iff; Ma and Wang, EJC 15 (2008) R17, Theorem 2 and Corollary 3); a negative leading coefficient of g only changes the sign of T"}}