{"certification":{"candidate":{"basis":{"family":{"first_index":0,"initial_polynomials":[["1"],["1","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"name":"A008288"},"coefficient_family":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["0","0"],["2","4"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"}},"coefficient_roots":{"lower_bound":{"attempts":[{"detail":"the rule is not P_(n+k) = c(x) P_n with c free of n","route":"periodic_product","success":false,"variant":"P_(n+k) = c(x) P_n"},{"detail":"B(n) P_n(x) = A(n,x) P_(n-1)(x), n >= 1: every P_n, n >= 0, is nonzero and real-rooted by product induction in the 1 residue classes","route":"product_recurrence","success":true,"variant":"product_recurrence"},{"detail":"not applicable: the theorem needs at least two seed rows","route":"three_term_recurrence","success":false,"variant":"three_term_recurrence"},{"detail":"HypothesisFailed: P_n = a_n(x) P_(n-1) + b_n(x) P'_(n-1) for n >= 1, with a_n(x) = (-2 n) + (-4 n) x and b_n(x) = (0) + (0) x + (0) x^2; open hypotheses: degree_step_positive: fails at n = 1: lambda_n = -4 n = -4 there (exact); constant_term_positive: fails at n = 1: a_n(0) = -2 n = -2 there (exact)","route":"liu_wang","success":false,"variant":"liu_wang"},{"detail":"not applicable: the theorem needs two seed rows","route":"liu_wang_derivative_lag","success":false,"variant":"liu_wang_derivative_lag"},{"detail":"not applicable: the rule is not f(n) P_n = c_0(n, x) P_(n-1) + gamma(n) (x - L)(x - U) P'_(n-1)","route":"ma_wang_interval","success":false,"variant":"ma_wang_interval"},{"detail":"not applicable: the theorem needs two seed rows","route":"liu_wang_three_term","success":false,"variant":"liu_wang_three_term"},{"detail":"P_n = a_n(x) S_n(P_(n-1)) for n >= 1, with a_n(x) = (x + 1/2) ((-4 n)) and S_n = the identity: every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0]; deg P_n = deg P_(n-1) + 1 for n >= 1; P_(n-1) interlaces P_n (weakly: P_n = a_n P_(n-1) with a_n linear adds one real root) for n >= 1","route":"iterated_preserver","success":true,"variant":"iterated_preserver"}],"conditional_on":[],"interlacing":{"from_index":1,"justification":{"premises":["every hypothesis of the theorem is verified exactly for every index: P_n = a_n(x) S_n(P_(n-1)) for n >= 1, with a_n(x) = (x + 1/2) ((-4 n)) and S_n = the identity","every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0]; deg P_n = deg P_(n-1) + 1 for n >= 1; P_(n-1) interlaces P_n (weakly: P_n = a_n P_(n-1) with a_n linear adds one real root) for n >= 1"],"theorem":"iterated_preserver: Iterated real-rootedness preservers (induction on n): if P_m is nonzero and real-rooted with every root in a closed region R and, for every n > m, P_n = a_n(x) S_n(P_(n-1)) where S_n maps every polynomial that is zero or real-rooted with every root in R to zero or a real-rooted polynomial with every root in R and a_n is real-rooted with every root in R, then every P_n is real-rooted with every root in R (the roots of a product are the roots of its factors); an exact degree step keeps every row nonzero; here S_n is the identity"},"kind":"weak","orientation":"previous_interlaces_next"},"route":"iterated_preserver","rows_checked":10,"statement":"every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign","status":"proved"},"parent_proof":{"route":"basis_map_coefficient_roots(liu_wang, iterated_preserver)","statement":"every coefficient row R_n, n >= 0, is zero or real-rooted with every root in [-1, 0]","status":"proved"},"source_interval":{"lower":{"closed":true,"value":{"lower_bound":"-1296121037/536870912","radicand":"2","rational_part":"-1","sqrt_coefficient":"-1","text":"-1 - sqrt(2)","upper_bound":"-10368968295/4294967296"}},"upper":{"closed":true,"value":{"lower_bound":"0","radicand":"1","rational_part":"0","sqrt_coefficient":"0","text":"0","upper_bound":"0"}}},"target_interval":{"lower":{"closed":true,"value":"-1"},"upper":{"closed":true,"value":"0"}},"upper_bound":{"attempts":[{"detail":"the rule is not P_(n+k) = c(x) P_n with c free of n","route":"periodic_product","success":false,"variant":"P_(n+k) = c(x) P_n"},{"detail":"B(n) P_n(x) = A(n,x) P_(n-1)(x), n >= 1: every P_n, n >= 0, is nonzero and real-rooted by product induction in the 1 residue classes","route":"product_recurrence","success":true,"variant":"product_recurrence"},{"detail":"not applicable: the theorem needs at least two seed rows","route":"three_term_recurrence","success":false,"variant":"three_term_recurrence"},{"detail":"P_n = a_n(x) P_(n-1) + b_n(x) P'_(n-1) for n >= 1, with a_n(x) = (2 n) + (4 n) x and b_n(x) = (0) + (0) x + (0) x^2: every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0) (so its coefficients have one sign); deg P_n = deg P_(n-1) + 1 and P_(n-1) interlaces P_n (Liu--Wang) for n >= 1","route":"liu_wang","success":true,"variant":"liu_wang"}],"conditional_on":[],"interlacing":{"from_index":1,"justification":{"premises":["every hypothesis of the theorem is verified exactly for every index: P_n = a_n(x) P_(n-1) + b_n(x) P'_(n-1) for n >= 1, with a_n(x) = (2 n) + (4 n) x and b_n(x) = (0) + (0) x + (0) x^2","every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0) (so its coefficients have one sign); deg P_n = deg P_(n-1) + 1 and P_(n-1) interlaces P_n (Liu--Wang) for n >= 1"],"theorem":"liu_wang: L. L. Liu and Y. Wang, A unified approach to polynomial sequences with only real zeros, Adv. in Appl. Math. 38 (2007) 542-560, Theorem 2.1 with g = f' (as in their Corollary 2.4), with nonnegativity of the coefficients replaced by an exact induction keeping every root in (-inf, 0)"},"kind":"weak","orientation":"previous_interlaces_next"},"route":"liu_wang","rows_checked":10,"statement":"every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign","status":"proved"}},"conclusion":{"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":"-1296121037/536870912","radicand":"2","rational_part":"-1","sqrt_coefficient":"-1","text":"-1 - sqrt(2)","upper_bound":"-10368968295/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":"-1564556493/268435456","radicand":"2","rational_part":"-3","sqrt_coefficient":"-2","text":"-3 - 2 sqrt(2)","upper_bound":"-12516451943/2147483648"}},"upper":{"closed":true,"value":{"lower_bound":"-368449945/2147483648","radicand":"2","rational_part":"-3","sqrt_coefficient":"2","text":"-3 + 2 sqrt(2)","upper_bound":"-46056243/268435456"}}},"sharp":false,"statement":"every PF input with all roots in [-1 - sqrt(2), 0] has a PF image; no larger [-R, 0] works"},"identity":{"certificate":{"basis":{"family":{"first_index":0,"initial_polynomials":[["1"],["1","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"name":"A008288"},"coefficient_family":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["0","0"],["2","4"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"direction":"input_by_transported","exceptional_bases":[],"input":{"first_index":0,"initial_polynomials":[["1"],["6","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["0","0"],["12","-8"],["-12","8"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["0","0"],["8","4"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"multiplier":["1"],"quotients":[{"row":[[{"coeff":{"coeffs":[["-12","-8"],["-6","-4"]]},"deriv_order":0}],[{"coeff":{"coeffs":[["8"],["4"]]},"deriv_order":0}]],"shift":0},{"row":[[{"coeff":{"coeffs":[["1"]]},"deriv_order":0}],[]],"shift":1}]},"status":"certified"},"input":{"first_index":0,"initial_polynomials":[["1"],["6","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["0","0"],["12","-8"],["-12","8"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["0","0"],["8","4"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"lift_summary":{"hypotheses":[{"evidence":"exact","name":"characteristic_parameter_positive","statement":"K = beta^2 + a beta - c = 2 > 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 = 1 >= 0","status":{"kind":"verified"}},{"evidence":"exact","name":"zero_in_source","statement":"K >= beta^2 (2 >= 1)","status":{"kind":"verified"}},{"evidence":"exact","name":"radius_positive","statement":"R = beta + sqrt(K) = 1 + sqrt(2) > 0","status":{"kind":"verified"}},{"evidence":"exact","name":"target_upper_end_nonpositive","statement":"a + 2 beta = 3 >= 0 and a^2 + 4c = 1 >= 0","status":{"kind":"verified"}},{"evidence":"exact","name":"initial_constant_nonnegative","statement":"l = 1 >= 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":"2l >= a or c >= l^2 - a l (with a^2 + 4c >= 0): every P_k(0) >= 0","status":{"kind":"verified"}}],"identity":{"method":"basis_map_division_input_by_transported","status":"certified"},"input_first_index":0,"input_interlacing":{"reason":"the map theorem does not prove that T_P preserves real-rootedness on the whole line","status":"not_proved"},"lean_replay":"not_attempted","operation":{"basis":"A008288","basis_family":{"first_index":0,"initial_polynomials":[["1"],["1","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"kind":"basis_map","source_interval":"[-1 - sqrt(2), 0]","target_interval":"[-3 - 2 sqrt(2), -3 + 2 sqrt(2)]"},"parent":{"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["0","0"],["2","4"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"relation":"Q_n = T_P(R_n), T_P(u^k) = P_(0 + k), P the basis family A008288"},"parent_proof":{"route":"basis_map_coefficient_roots(liu_wang, iterated_preserver)","statement":"every coefficient row R_n, n >= 0, is zero or real-rooted with every root in [-1, 0]","status":"proved"},"root_transfer":{"input_conclusion":"every input row Q_n, n >= 0, is zero or real-rooted with every root in [-3 - 2 sqrt(2), -3 + 2 sqrt(2)] (nonnegative coefficients when the coefficient row has a positive leading coefficient)","input_root_region":{"lower":{"closed":true,"exact":{"radicand":"2","rational_part":"-3","sqrt_coefficient":"-2"},"value":"-1564556493/268435456"},"upper":{"closed":true,"exact":{"radicand":"2","rational_part":"-3","sqrt_coefficient":"2"},"value":"-46056243/268435456"}},"parent_hypothesis":"every coefficient row R_n is zero or real-rooted with every root in the source interval of the map theorem","parent_root_region":{"lower":{"closed":true,"value":"-1"},"upper":{"closed":true,"value":"0"}},"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)"},"verdict":"proved"},"map_theorem":{"basis":{"first_index":0,"initial_polynomials":[["1"],["1","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","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":"A008288","conclusions":[{"hypotheses":["characteristic_parameter_positive","initial_slope_nonnegative"],"input_interval":{"lower":{"closed":true,"value":{"lower_bound":"-1296121037/536870912","radicand":"2","rational_part":"-1","sqrt_coefficient":"-1","text":"-1 - sqrt(2)","upper_bound":"-10368968295/4294967296"}},"upper":{"closed":true,"value":{"lower_bound":"1779033703/4294967296","radicand":"2","rational_part":"-1","sqrt_coefficient":"1","text":"-1 + sqrt(2)","upper_bound":"222379213/536870912"}}},"nonnegative_coefficients":false,"output_interval":{},"sharp":false,"statement":"every real polynomial with all roots in E = [-1 - sqrt(2), -1 + sqrt(2)] has a real-rooted image"},{"hypotheses":["characteristic_parameter_positive","initial_slope_nonnegative","target_interval"],"input_interval":{"lower":{"closed":true,"value":{"lower_bound":"-1296121037/536870912","radicand":"2","rational_part":"-1","sqrt_coefficient":"-1","text":"-1 - sqrt(2)","upper_bound":"-10368968295/4294967296"}},"upper":{"closed":true,"value":{"lower_bound":"1779033703/4294967296","radicand":"2","rational_part":"-1","sqrt_coefficient":"1","text":"-1 + sqrt(2)","upper_bound":"222379213/536870912"}}},"nonnegative_coefficients":false,"output_interval":{"lower":{"closed":true,"value":{"lower_bound":"-1564556493/268435456","radicand":"2","rational_part":"-3","sqrt_coefficient":"-2","text":"-3 - 2 sqrt(2)","upper_bound":"-12516451943/2147483648"}},"upper":{"closed":true,"value":{"lower_bound":"-368449945/2147483648","radicand":"2","rational_part":"-3","sqrt_coefficient":"2","text":"-3 + 2 sqrt(2)","upper_bound":"-46056243/268435456"}}},"sharp":false,"statement":"every real polynomial with all roots in E = [-1 - sqrt(2), -1 + sqrt(2)] has an image with all roots in I = [-3 - 2 sqrt(2), -3 + 2 sqrt(2)]"},{"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":"-1296121037/536870912","radicand":"2","rational_part":"-1","sqrt_coefficient":"-1","text":"-1 - sqrt(2)","upper_bound":"-10368968295/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":"-1564556493/268435456","radicand":"2","rational_part":"-3","sqrt_coefficient":"-2","text":"-3 - 2 sqrt(2)","upper_bound":"-12516451943/2147483648"}},"upper":{"closed":true,"value":{"lower_bound":"-368449945/2147483648","radicand":"2","rational_part":"-3","sqrt_coefficient":"2","text":"-3 + 2 sqrt(2)","upper_bound":"-46056243/268435456"}}},"sharp":false,"statement":"every PF input with all roots in [-1 - sqrt(2), 0] has a PF image; no larger [-R, 0] works"}],"hypotheses":[{"evidence":"exact","name":"characteristic_parameter_positive","statement":"K = beta^2 + a beta - c = 2 > 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 = 1 >= 0","status":{"kind":"verified"}},{"evidence":"exact","name":"zero_in_source","statement":"K >= beta^2 (2 >= 1)","status":{"kind":"verified"}},{"evidence":"exact","name":"radius_positive","statement":"R = beta + sqrt(K) = 1 + sqrt(2) > 0","status":{"kind":"verified"}},{"evidence":"exact","name":"target_upper_end_nonpositive","statement":"a + 2 beta = 3 >= 0 and a^2 + 4c = 1 >= 0","status":{"kind":"verified"}},{"evidence":"exact","name":"initial_constant_nonnegative","statement":"l = 1 >= 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":"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":"1","b":"1","c":"0","d":"1","initial_constant":"1","initial_slope":"1","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)"},"schema":"polytool.recurrence-basis-map-lift.v1"},"kind":"basis_map"}