{"kind":"basis_map_theorem","report":{"basis":{"first_index":1,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["-3","1"],["4","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","1"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"basis_name":"Triangle read by rows, the Bell transform of the quartic factorial numbers A007696(n+1) without column 0.","conclusions":[{"hypotheses":["scalar_affine_nondecreasing","multiplier_slope_positive","kappa_nonnegative","initial_row_roots","ray_source_contains_nonpositive_ray"],"input_interval":{"upper":{"closed":true,"value":{"lower_bound":"0","radicand":"1","rational_part":"0","sqrt_coefficient":"0","text":"0","upper_bound":"0"}}},"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":false,"statement":"(-inf, 0] -> (-inf, 0] through R_s, s = 4, and U_g"}],"hypotheses":[{"evidence":"exact","name":"scalar_affine_nondecreasing","statement":"alpha(k) = 5 + 4k is affine in k with slope >= 0","status":{"kind":"verified"}},{"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"}},{"evidence":"exact","name":"ray_source_contains_nonpositive_ray","statement":"a + b h + kappa m = 5 >= 0 (the source of U_g contains (-inf, 0])","status":{"kind":"verified"}}],"lean_declarations":["RealRooted.basisMap_factorization_of_scalarIndex_recurrence","RealRooted.NewtonParametersAffine.preservesNonposRooted","RealRooted.rayBasisMap_maps_realRootedIn_iff"],"lean_replay":"not_attempted","schema":"polytool.recurrence-basis-map-theorem.v1","shape":{"b":"1","initial_row":["1"],"kappa":"1","kind":"scalar_index","root":"0","scalar":["5","4"]},"status":"proved","theorem":"index-dependent scalar term: P_(k+1) = (L + k s) P_k with L f = (a + b t) f + kappa (t - h) f' gives T = U_g o R_s (RealRooted basisMap_factorization_of_scalarIndex_recurrence), where R_s(u^k) = u (u + s) ... (u + (k-1) s) keeps every root <= 0 for s >= 0 (Su, Yang and Zhang, Australas. J. Combin. 56 (2013), Theorem 4; Brenti, Mem. AMS 413 (1989), Theorem 2.4.3; RealRooted NewtonParametersAffine.preservesNonposRooted) and U_g(u^k) = L^k g sends (-inf, a + b h + kappa m] into (-inf, h] (RealRooted rayBasisMap_maps_realRootedIn_iff)"}}