{"certification":{"candidate":{"basis":{"family":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"name":"A007318"},"coefficient_family":{"first_index":0,"initial_polynomials":[["1"],["1","4"]],"recurrence":{"denominator":{"coeffs":[["0"],["1"]]},"terms":[{"coeff":{"coeffs":[["-1","3"],["2","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["1","1"],["-1","-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"}},"coefficient_roots":{"parent_proof":{"route":"basis_map_coefficient_roots(hypergeometric_row)","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":"the leader is not a nonzero constant","route":"periodic_product","success":false,"variant":"P_(n+k) = c(x) P_n"},{"detail":"not applicable: expected one nonzero lag term","route":"product_recurrence","success":false,"variant":"product_recurrence"},{"detail":"no theorem matched (weighted_renewal_window: LHS must be a nonzero constant; fixed_delay_predecessor_window: LHS must be a nonzero constant)","route":"paper_theorem","success":false,"variant":"match_recurrence_theorems"},{"detail":"no unconditional all-index source claim with roots in (-inf, 0]","route":"root_domain","success":false,"variant":"identity (affine 1, 0)"},{"detail":"no unconditional all-index source claim with roots in (-inf, 0]","route":"root_domain","success":false,"variant":"f_polynomial"},{"detail":"no unconditional all-index source claim with roots in (-inf, 0]","route":"root_domain","success":false,"variant":"reversal"},{"detail":"no unconditional all-index source claim with roots in (-inf, 0]","route":"root_domain","success":false,"variant":"mobius (1, 0, -1, 1)"},{"detail":"no unconditional all-index source claim with roots in (-inf, 0]","route":"root_domain","success":false,"variant":"identity (affine 1, 0), induction start moved 1 row(s)"},{"detail":"no unconditional all-index source claim with roots in (-inf, 0]","route":"root_domain","success":false,"variant":"f_polynomial, induction start moved 1 row(s)"},{"detail":"no unconditional all-index source claim with roots in (-inf, 0]","route":"root_domain","success":false,"variant":"reversal, induction start moved 1 row(s)"},{"detail":"no unconditional all-index source claim with roots in (-inf, 0]","route":"root_domain","success":false,"variant":"mobius (1, 0, -1, 1), induction start moved 1 row(s)"},{"detail":"no unconditional all-index source claim with roots in (-inf, 0]","route":"root_domain","success":false,"variant":"identity (affine 1, 0), induction start moved 2 row(s)"},{"detail":"no unconditional all-index source claim with roots in (-inf, 0]","route":"root_domain","success":false,"variant":"f_polynomial, induction start moved 2 row(s)"},{"detail":"no unconditional all-index source claim with roots in (-inf, 0]","route":"root_domain","success":false,"variant":"reversal, induction start moved 2 row(s)"},{"detail":"no unconditional all-index source claim with roots in (-inf, 0]","route":"root_domain","success":false,"variant":"mobius (1, 0, -1, 1), induction start moved 2 row(s)"},{"detail":"no unconditional all-index source claim with roots in (-inf, 0]","route":"root_domain","success":false,"variant":"identity (affine 1, 0), induction start moved 3 row(s)"},{"detail":"no unconditional all-index source claim with roots in (-inf, 0]","route":"root_domain","success":false,"variant":"f_polynomial, induction start moved 3 row(s)"},{"detail":"no unconditional all-index source claim with roots in (-inf, 0]","route":"root_domain","success":false,"variant":"reversal, induction start moved 3 row(s)"},{"detail":"no unconditional all-index source claim with roots in (-inf, 0]","route":"root_domain","success":false,"variant":"mobius (1, 0, -1, 1), induction start moved 3 row(s)"},{"detail":"not applicable: c_2(n, x) = gamma(n) w(x) with w neither constant nor a constant times a square (x + v_0)^2","route":"three_term_recurrence","success":false,"variant":"three_term_recurrence"},{"detail":"not applicable: the rule is not f(n) P_n = c_0(n, x) P_(n-1) + c_1(n, x) P'_(n-1)","route":"liu_wang","success":false,"variant":"liu_wang"},{"detail":"HypothesisFailed: P_n = A_n(x) P_(n-1) + V_n(x) P'_(n-1) + W_n(x) P_(n-2) for n >= 2, with A_n(x) = ((2 n - 1)/(n)) + ((n + 3)/(n)) x, V_n(x) = 0, W_n(x) = ((-n + 1)/(n)) + ((-n + 1)/(n)) x; open hypotheses: multipliers_vanish_at_zero: [x^0] c_2(n, x) = -n + 1 is not the zero polynomial; lag_coefficient_nonpositive: W_n is not separable with a factor of one sign on (-inf, 0), and the sufficient monomial test (-1)^k [x^k] W_n <= 0 fails for k = 1 (not a disproof): fails at n = 2: [x^1] W_n = -1/2 there (exact); derivative_or_lag_coefficient_negative: W_n is not separable with a factor of one sign on (-inf, 0), and the sufficient monomial test (-1)^k [x^k] W_n <= 0 fails for k = 1 (not a disproof): fails at n = 2: [x^1] W_n = -1/2 there (exact)","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":"Unresolved: P_n = A_n(x) P_(n-1) + B_n(x) P_(n-2) for n >= 2, with A_n(x) = ((2 n - 1)/(n)) + ((n + 3)/(n)) x, B_n(x) = ((-n + 1)/(n)) + ((-n + 1)/(n)) x; open hypotheses: lag_coefficient_nonpositive: neither everywhere (B_n has degree 1 in x, so it is not <= 0 on the whole line) nor on x <= 0 (B_n is not separable with a factor of one sign on (-inf, 0), and the sufficient monomial test (-1)^k [x^k] B_n <= 0 fails for k = 1 (not a disproof): fails at n = 2: [x^1] B_n = -1/2 there (exact))","route":"liu_wang_three_term","success":false,"variant":"liu_wang_three_term"},{"detail":"row relation p(n, k) [x^k] P_n + q(n, k) [x^(k-1)] P_n = 0, n >= 0, with p = (-1) (k) (k), q = (-1) (k - n - 1) (k + 3); valuation v(n) = 0, degree d(n) = n: every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0): for n >= 0 the coefficients U_j (U_j = [x^(j + v(n))] P_n, v(n) = 0) satisfy U_j = U_0(n) prod_(t <= j) R(n, t), R(n, j) = (-1) (j - n - 1) (j + 3) / ((j) (j)), so sum_j U_j y^j is U_0(n) times the image of (1 + y)^(n) under a nonnegative multiplier sequence, and U_0(n) != 0 for n >= 0 by its scalar recurrence","route":"hypergeometric_row","success":true,"variant":"hypergeometric_row"}],"conditional_on":[],"route":"hypergeometric_row","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":["initial_row_nonzero","initial_row_real_rooted","initial_row_nonpositive_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":"an input root r <= 1 gives the root (r - a)/d <= 0; a larger root gives a positive root"},"identity":{"certificate":{"basis":{"family":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"name":"A007318"},"coefficient_family":{"first_index":0,"initial_polynomials":[["1"],["1","4"]],"recurrence":{"denominator":{"coeffs":[["0"],["1"]]},"terms":[{"coeff":{"coeffs":[["-1","3"],["2","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["1","1"],["-1","-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"direction":"input_by_transported","exceptional_bases":[],"input":{"first_index":0,"initial_polynomials":[["1"],["5","4"]],"recurrence":{"denominator":{"coeffs":[["0"],["1"]]},"terms":[{"coeff":{"coeffs":[["2","1"],["-2","-1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","3"],["3","1"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"multiplier":["2","1"],"quotients":[{"row":[[{"coeff":{"coeffs":[["2"],["1"]]},"deriv_order":0}]],"shift":0}]},"status":"certified"},"input":{"first_index":0,"initial_polynomials":[["1"],["5","4"]],"recurrence":{"denominator":{"coeffs":[["0"],["1"]]},"terms":[{"coeff":{"coeffs":[["2","1"],["-2","-1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","3"],["3","1"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"lift_summary":{"hypotheses":[{"evidence":"exact","name":"initial_row_nonzero","statement":"g = P_0 is nonzero","status":{"kind":"verified"}},{"evidence":"exact root isolation","name":"initial_row_real_rooted","statement":"g is real-rooted","status":{"kind":"verified"}},{"evidence":"exact root isolation","name":"initial_row_nonpositive_roots","statement":"every root of g is <= 0","status":{"kind":"verified"}}],"identity":{"method":"basis_map_division_input_by_transported","status":"certified"},"input_first_index":0,"input_interlacing":{"reason":"the parent route hypergeometric_row proves no interlacing of consecutive parent rows","status":"not_proved"},"lean_replay":"not_attempted","operation":{"basis":"A007318","basis_family":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"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"],["1","4"]],"recurrence":{"denominator":{"coeffs":[["0"],["1"]]},"terms":[{"coeff":{"coeffs":[["-1","3"],["2","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["1","1"],["-1","-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"relation":"Q_n = T_P(R_n), T_P(u^k) = P_(0 + k), P the basis family A007318"},"parent_proof":{"route":"basis_map_coefficient_roots(hypergeometric_row)","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":"geometric family P_k = g(t) (a + d t)^k: T(p) = g(t) p(a + d t), so the roots of T(p) are those of g and the points (r - a)/d for the roots r of p (elementary)"},"verdict":"proved"},"map_theorem":{"basis":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"basis_name":"A007318","conclusions":[{"hypotheses":["initial_row_nonzero","initial_row_real_rooted"],"input_interval":{},"nonnegative_coefficients":false,"output_interval":{},"sharp":true,"statement":"every real-rooted input has a real-rooted image (an affine substitution times g)"},{"hypotheses":["initial_row_nonzero","initial_row_real_rooted","initial_row_nonpositive_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":"an input root r <= 1 gives the root (r - a)/d <= 0; a larger root gives a positive root"}],"hypotheses":[{"evidence":"exact","name":"initial_row_nonzero","statement":"g = P_0 is nonzero","status":{"kind":"verified"}},{"evidence":"exact root isolation","name":"initial_row_real_rooted","statement":"g is real-rooted","status":{"kind":"verified"}},{"evidence":"exact root isolation","name":"initial_row_nonpositive_roots","statement":"every root of g is <= 0","status":{"kind":"verified"}}],"lean_replay":"not_attempted","schema":"polytool.recurrence-basis-map-theorem.v1","shape":{"constant":"1","initial_row":["1"],"kind":"geometric","slope":"1"},"status":"proved","theorem":"geometric family P_k = g(t) (a + d t)^k: T(p) = g(t) p(a + d t), so the roots of T(p) are those of g and the points (r - a)/d for the roots r of p (elementary)"},"schema":"polytool.recurrence-basis-map-lift.v1"},"kind":"basis_map"}