{"kind":"basis_map_theorem","report":{"basis":{"first_index":0,"initial_polynomials":[["1"],["2","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","2"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"basis_name":"Triangle T(n, k) is coefficient of z^n*w^k in 1/(1 - 2*z - 2*w - 2*z*w) read by rows in order 00, 10, 01, 20, 11, 02, ...","conclusions":[{"hypotheses":["characteristic_parameter_positive","initial_slope_nonnegative"],"input_interval":{"lower":{"closed":true,"value":{"lower_bound":"-5867034435/2147483648","radicand":"3","rational_part":"-1","sqrt_coefficient":"-1","text":"-1 - sqrt(3)","upper_bound":"-11734068869/4294967296"}},"upper":{"closed":true,"value":{"lower_bound":"3144134277/4294967296","radicand":"3","rational_part":"-1","sqrt_coefficient":"1","text":"-1 + sqrt(3)","upper_bound":"1572067139/2147483648"}}},"nonnegative_coefficients":false,"output_interval":{},"sharp":false,"statement":"every real polynomial with all roots in E = [-1 - sqrt(3), -1 + sqrt(3)] has a real-rooted image"},{"hypotheses":["characteristic_parameter_positive","initial_slope_nonnegative","target_interval"],"input_interval":{"lower":{"closed":true,"value":{"lower_bound":"-5867034435/2147483648","radicand":"3","rational_part":"-1","sqrt_coefficient":"-1","text":"-1 - sqrt(3)","upper_bound":"-11734068869/4294967296"}},"upper":{"closed":true,"value":{"lower_bound":"3144134277/4294967296","radicand":"3","rational_part":"-1","sqrt_coefficient":"1","text":"-1 + sqrt(3)","upper_bound":"1572067139/2147483648"}}},"nonnegative_coefficients":false,"output_interval":{"lower":{"closed":true,"value":{"lower_bound":"-8014518083/2147483648","radicand":"3","rational_part":"-2","sqrt_coefficient":"-1","text":"-2 - sqrt(3)","upper_bound":"-16029036165/4294967296"}},"upper":{"closed":true,"value":{"lower_bound":"-1150833019/4294967296","radicand":"3","rational_part":"-2","sqrt_coefficient":"1","text":"-2 + sqrt(3)","upper_bound":"-575416509/2147483648"}}},"sharp":false,"statement":"every real polynomial with all roots in E = [-1 - sqrt(3), -1 + sqrt(3)] has an image with all roots in I = [-2 - sqrt(3), -2 + sqrt(3)]"},{"hypotheses":["characteristic_parameter_positive","initial_slope_nonnegative","target_interval","current_constant_nonnegative","zero_in_source","radius_positive","target_upper_end_nonpositive","initial_constant_nonnegative","constant_terms_nonnegative"],"input_interval":{"lower":{"closed":true,"value":{"lower_bound":"-5867034435/2147483648","radicand":"3","rational_part":"-1","sqrt_coefficient":"-1","text":"-1 - sqrt(3)","upper_bound":"-11734068869/4294967296"}},"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":{"lower":{"closed":true,"value":{"lower_bound":"-8014518083/2147483648","radicand":"3","rational_part":"-2","sqrt_coefficient":"-1","text":"-2 - sqrt(3)","upper_bound":"-16029036165/4294967296"}},"upper":{"closed":true,"value":{"lower_bound":"-1150833019/4294967296","radicand":"3","rational_part":"-2","sqrt_coefficient":"1","text":"-2 + sqrt(3)","upper_bound":"-575416509/2147483648"}}},"sharp":false,"statement":"every PF input with all roots in [-1 - sqrt(3), 0] has a PF image; no larger [-R, 0] works"}],"hypotheses":[{"evidence":"exact","name":"characteristic_parameter_positive","statement":"K = beta^2 + a beta - c = 3 > 0","status":{"kind":"verified"}},{"evidence":"exact","name":"initial_slope_nonnegative","statement":"eta = m/d = 1 >= 0","status":{"kind":"verified"}},{"evidence":"exact","name":"target_interval","statement":"2 eta - 1 = 1 >= 0 and (s - (2 eta - 1) beta)^2 <= (2 eta - 1)^2 K, s = 0","status":{"kind":"verified"}},{"evidence":"exact","name":"current_constant_nonnegative","statement":"a = 2 >= 0","status":{"kind":"verified"}},{"evidence":"exact","name":"zero_in_source","statement":"K >= beta^2 (3 >= 1)","status":{"kind":"verified"}},{"evidence":"exact","name":"radius_positive","statement":"R = beta + sqrt(K) = 1 + sqrt(3) > 0","status":{"kind":"verified"}},{"evidence":"exact","name":"target_upper_end_nonpositive","statement":"a + 2 beta = 4 >= 0 and a^2 + 4c = 4 >= 0","status":{"kind":"verified"}},{"evidence":"exact","name":"initial_constant_nonnegative","statement":"l = 2 >= 0","status":{"kind":"verified"}},{"evidence":"a^2 + 4c = 4 >= 0: true; 2s >= a or c >= s^2 - a s: true","name":"constant_terms_nonnegative","statement":"2l >= a or c >= l^2 - a l (with a^2 + 4c >= 0): every P_k(0) >= 0","status":{"kind":"verified"}}],"lean_declarations":["RealRooted.orderTwoConstants_nonneg_iff"],"lean_replay":"not_attempted","schema":"polytool.recurrence-basis-map-theorem.v1","shape":{"a":"2","b":"2","c":"0","d":"2","initial_constant":"2","initial_slope":"2","kind":"affine_current","normalization":"1"},"status":"proved","theorem":"affine current multiplier with an affine initial row (module documentation, \"The affine-current theorem\"): with beta = b/d, K = beta^2 + a beta - c > 0 and eta = m/d >= 0, every real polynomial with all roots in E = [-beta - sqrt(K), -beta + sqrt(K)] has a real-rooted image, and no interval of positive length outside E works (Theorem 1); for eta > 0 the images lie in I = [(-a - 2 beta - 2 sqrt(K))/d, (-a - 2 beta + 2 sqrt(K))/d] if and only if eta >= 1/2 and (s - (2 eta - 1) beta)^2 <= (2 eta - 1)^2 K, s = l - eta a (Theorem 2); with a >= 0, K >= beta^2, a + 2 beta >= 0, a^2 + 4c >= 0, l >= 0 and the scalar criterion, PF inputs with roots in [-R, 0], R = beta + sqrt(K), have PF images, sharply (the common-interlacer proof; the Chebyshev case is Iserles and Saff, Math. Proc. Cambridge Philos. Soc. 105 (1989), Theorem 1; the scalar criterion is RealRooted orderTwoConstants_nonneg_iff)"}}