{"kind":"basis_map_theorem","report":{"basis":{"first_index":0,"initial_polynomials":[["36","18","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["6","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","6"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"basis_name":"Stirling2 triangle with scaled diagonals (powers of 6).","conclusions":[{"hypotheses":["multiplier_slope_positive","kappa_nonnegative","initial_row_roots"],"input_interval":{"upper":{"closed":true,"value":{"lower_bound":"6","radicand":"1","rational_part":"6","sqrt_coefficient":"0","text":"6","upper_bound":"6"}}},"nonnegative_coefficients":true,"output_interval":{"upper":{"closed":true,"value":{"lower_bound":"0","radicand":"1","rational_part":"0","sqrt_coefficient":"0","text":"0","upper_bound":"0"}}},"sharp":true,"statement":"source (-inf, a + b h + kappa m] = (-inf, 6] with m = 0, target (-inf, 0]"}],"hypotheses":[{"evidence":"exact","name":"multiplier_slope_positive","statement":"b > 0","status":{"kind":"verified"}},{"evidence":"exact","name":"kappa_nonnegative","statement":"kappa >= 0","status":{"kind":"verified"}},{"evidence":"exact root isolation","name":"initial_row_roots","statement":"g = P_0 is nonzero and real-rooted with every root <= 0","status":{"kind":"verified"}}],"lean_declarations":["RealRooted.rayBasisMap_maps_realRootedIn_iff"],"lean_replay":"not_attempted","schema":"polytool.recurrence-basis-map-theorem.v1","shape":{"a":"6","b":"1","initial_row":["36","18","1"],"kappa":"6","kind":"ray_differential","root":"0"},"status":"proved","theorem":"ray basis maps: for L f = (a + b t) f + kappa (t - h) f', b > 0, kappa >= 0, and g real-rooted with every root <= h, of multiplicity m at h, T(u^k) = L^k g sends every real polynomial with all roots in S to one with all roots in (-inf, h] if and only if S lies in (-inf, a + b h + kappa m] (RealRooted rayBasisMap_maps_realRootedIn_iff; the step is Ma and Wang, EJC 15 (2008) R17, Theorem 2)"}}