{"kind":"basis_map_theorem","report":{"basis":{"first_index":0,"initial_polynomials":[["1"],["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"basis_name":"Irregular triangle read by rows: T(n,k) = binomial(n-k, k), n >= 0, 0 <= k <= floor(n/2); or, coefficients of (one version of) Fibonacci polynomials.","conclusions":[{"hypotheses":["current_nonnegative","initial_constant_nonnegative","lag_slope_positive"],"input_interval":{"upper":{"closed":true,"value":{"lower_bound":"0","radicand":"1","rational_part":"0","sqrt_coefficient":"0","text":"0","upper_bound":"0"}}},"nonnegative_coefficients":false,"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":"every PF input has a real-rooted image with every root <= -c/b = 0"},{"hypotheses":["current_nonnegative","initial_constant_nonnegative","lag_slope_positive","constant_terms_nonnegative"],"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":true,"statement":"every PF input has a PF image (zero allowed)"}],"hypotheses":[{"evidence":"exact","name":"current_nonnegative","statement":"a >= 0","status":{"kind":"verified"}},{"evidence":"exact","name":"initial_constant_nonnegative","statement":"s >= 0","status":{"kind":"verified"}},{"evidence":"exact","name":"lag_slope_positive","statement":"b > 0","status":{"kind":"verified"}},{"evidence":"a^2 + 4c = 1 >= 0: true; 2s >= a or c >= s^2 - a s: true","name":"constant_terms_nonnegative","statement":"a^2 + 4c >= 0 and (2s >= a or c >= s^2 - a s), equivalently every P_k(0) >= 0","status":{"kind":"verified"}}],"lean_declarations":["RealRooted.basisTransform_orderTwoBasis_eq_comp","RealRooted.orderTwoZeroTransform_isPFPolynomial","RealRooted.orderTwoBasis_pf_equivalences","RealRooted.basisTransform_orderTwoBasis_preserves_bounded_pf_iff"],"lean_replay":"not_attempted","schema":"polytool.recurrence-basis-map-theorem.v1","shape":{"a":"1","b":"1","c":"0","initial_constant":"1","kind":"constant_current","normalization":"1"},"status":"proved","theorem":"constant current multiplier: P_0 = 1, P_1 = s, P_(k+2) = a P_(k+1) + (b t + c) P_k with a, s >= 0, b > 0.  P_k(t) = Q_k(b t + c) for the rows Q_k with b = 1, c = 0, whose map sends PF inputs to PF outputs (an interlacing-preserving 2 x 2 matrix, Branden, arXiv:1410.6601, Theorem 8.5), so every PF input has a real-rooted image with roots <= -c/b; PF inputs (also those with roots in any [-R, 0]) have PF images if and only if every P_k(0) >= 0, if and only if a^2 + 4c >= 0 and (2s >= a or c >= s^2 - a s) (RealRooted orderTwoBasis_pf_equivalences, basisTransform_orderTwoBasis_preserves_bounded_pf_iff)"}}