{"certification":{"candidate":{"basis":{"family":{"first_index":1,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","1"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"name":"A008277"},"coefficient_family":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"}},"coefficient_roots":{"parent_proof":{"route":"basis_map_coefficient_roots(periodic_product)","statement":"every coefficient row R_n, n >= 0, is zero or real-rooted with every root in (-inf, 0]","status":"proved"},"source_interval":{"upper":{"closed":true,"value":{"lower_bound":"1","radicand":"1","rational_part":"1","sqrt_coefficient":"0","text":"1","upper_bound":"1"}}},"target_interval":{"upper":{"closed":true,"value":"0"}},"upper_bound":{"attempts":[{"detail":"c and the seeds are nonzero, real-rooted and of one sign, so P_(n0 + k m + i) = c^m P_(n0 + i) is too","route":"periodic_product","success":true,"variant":"P_(n+k) = c(x) P_n"}],"conditional_on":[],"route":"periodic_product","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":["multiplier_slope_positive","kappa_nonnegative","initial_row_roots"],"input_interval":{"upper":{"closed":true,"value":{"lower_bound":"1","radicand":"1","rational_part":"1","sqrt_coefficient":"0","text":"1","upper_bound":"1"}}},"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, 1] with m = 0, target (-inf, 0]"},"identity":{"certificate":{"basis":{"family":{"first_index":1,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","1"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"name":"A008277"},"coefficient_family":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"direction":"input_by_transported","exceptional_bases":[],"input":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["3","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","2"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"multiplier":["1"],"quotients":[{"row":[[{"coeff":{"coeffs":[["1"]]},"deriv_order":0}]],"shift":0}]},"status":"certified"},"input":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["3","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","2"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"lift_summary":{"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"}}],"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":"A008277","basis_family":{"first_index":1,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","1"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"kind":"basis_map","source_interval":"(-inf, 1]","target_interval":"(-inf, 0]"},"parent":{"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"relation":"Q_n = T_P(R_n), T_P(u^k) = P_(1 + k), P the basis family A008277"},"parent_proof":{"route":"basis_map_coefficient_roots(periodic_product)","statement":"every coefficient row R_n, n >= 0, is zero or real-rooted with every root in (-inf, 0]","status":"proved"},"root_transfer":{"input_conclusion":"every input row Q_n, n >= 0, is zero or real-rooted with every root in (-inf, 0] (nonnegative coefficients when the coefficient row has a positive leading coefficient)","input_root_region":{"upper":{"closed":true,"value":"0"}},"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":{"upper":{"closed":true,"value":"0"}},"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)"},"verdict":"proved"},"map_theorem":{"basis":{"first_index":1,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","1"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"basis_name":"A008277","conclusions":[{"hypotheses":["multiplier_slope_positive","kappa_nonnegative","initial_row_roots"],"input_interval":{"upper":{"closed":true,"value":{"lower_bound":"1","radicand":"1","rational_part":"1","sqrt_coefficient":"0","text":"1","upper_bound":"1"}}},"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, 1] 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":"1","b":"1","initial_row":["1"],"kappa":"1","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)"},"schema":"polytool.recurrence-basis-map-lift.v1"},"kind":"basis_map"}