{"certification":{"candidate":{"gauge":{"denominator":["0","1"],"kind":"closed","numerator":["1"]},"index_shift":-1,"operator":{"factor":{"terms":[{"coefficient_offset":1,"index_offset":0,"kind":"binomial"}]},"shape":"hadamard_multiplier"},"parent":{"first_index":0,"initial_polynomials":[["1"],["1","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","0","-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"n-79ebafb266da3b41"},"identifying_rows":2,"identity":{"certificate":{"certificate":{"factor":{"terms":[{"coefficient_offset":1,"index_offset":0,"kind":"binomial"}]},"hadamard":{"conjugated_input_relation":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["0","0","-48"],["0","0","-102"],["0","0","-69"],["0","0","-15"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","0","0","0"],["0","0","0","-48"],["0","0","0","-102"],["0","0","0","-69"],["0","0","0","-15"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0","0","0","0"],["0","0","0","0","-8"],["0","0","0","0","-17"],["0","0","0","0","-23/2"],["0","0","0","0","-5/2"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["0","0"],["-20","-40"],["-68","-176"],["-89","-246"],["-56","-136"],["-17","-26"],["-2","0"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","0","0"],["0","20","124"],["0","34","209"],["0","12","141/2"],["0","-4","-55/2"],["0","-2","-13"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["0","0","0","0"],["0","0","14","48"],["0","0","29","99"],["0","0","19","129/2"],["0","0","4","27/2"]]},"deriv_order":2,"shift":1},{"coeff":{"coeffs":[["0"],["20"],["68"],["89"],["56"],["17"],["2"]]},"deriv_order":0,"shift":2}]},"conjugation_x_shift":0,"exceptional_bases":[],"factor":{"terms":[{"coefficient_offset":1,"index_offset":0,"kind":"binomial"}]},"gauge":{"denominator":["0","1"],"kind":"closed","numerator":["1"]},"identifying_indices":[1,2],"input_leader_shift":2,"input_relation":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["0","0","-4"],["0","0","-5/2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-10","-10"],["-9","-29"],["-2","-13"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-7","24"],["0","-4","27/2"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["10"],["9"],["2"]]},"deriv_order":0,"shift":2}]},"input_valid_from_base":1,"multiplier":["0","0","0","1"],"parent":{"first_index":1,"initial_polynomials":[["1"],["1","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","0","-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_leader_shift":2,"parent_relation":{"terms":[{"coeff":{"coeffs":[["0","0","1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-1","-2"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"shift":2}]},"parent_valid_from_base":1,"quotients":[{"differentiations":[{"coeff":{"coeffs":[["0","0","0","0","0"],["0","0","0","0","0"],["0","0","0","0","0"],["0","0","0","0","0"],["0","0","160","1280","2560"],["0","0","544","4352","8704"],["0","0","712","5696","11392"],["0","0","448","3584","7168"],["0","0","136","1088","2176"],["0","0","16","128","256"]]},"deriv_order":0}],"shift":0}],"row_annihilator_system":{"generators":[{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","2"],["-2","-6"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","1","4"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0"],["2"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","0","0"],["0","0","0","0","0","0"],["0","0","0","0","0","0"],["0","0","0","0","0","0"],["0","0","0","-160","-1280","-2560"],["0","0","0","-272","-2176","-4352"],["0","0","0","-96","-768","-1536"],["0","0","0","32","256","512"],["0","0","0","16","128","256"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0"],["0","0","0","0","0","0","0"],["0","0","0","0","0","0","0"],["0","0","0","80","1136","5248","7936"],["0","0","0","136","1924","8864","13376"],["0","0","0","48","666","3024","4512"],["0","0","0","-16","-238","-1136","-1760"],["0","0","0","-8","-116","-544","-832"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0"],["0","0","0","0","56","640","2432","3072"],["0","0","0","0","116","1324","5024","6336"],["0","0","0","0","76","866","3280","4128"],["0","0","0","0","16","182","688","864"]]},"deriv_order":2}],"step_multiplier":{"coeffs":[["0","0","0"],["0","0","0"],["0","4","16"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","0"],["0","0","0","0"],["0","0","-4","-16"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0"],["0","0","2","16","32"]]},"deriv_order":1}],[{"coeff":{"coeffs":[["0","0","0","0","0"],["0","0","-2","-16","-32"]]},"deriv_order":0}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["2"],["-6"],["4"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["1","10"],["-2","-8"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","1","4"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","0","0","0"],["0","0","0","0","0","0","0"],["0","0","0","0","0","0","0"],["0","0","0","-80","-1136","-5248","-7936"],["0","0","0","-136","-2036","-9760","-15168"],["0","0","0","-48","-898","-4880","-8224"],["0","0","0","16","86","-80","-672"],["0","0","0","8","84","288","320"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0"],["0","0","0","0","-56","-640","-2432","-3072"],["0","0","0","0","-116","-1324","-5024","-6336"],["0","0","0","0","-76","-866","-3280","-4128"],["0","0","0","0","-16","-182","-688","-864"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["0","0","0","0","0"],["0","0","0","0","0"],["0","0","0","0","0"],["0","0","8","64","128"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","0","0"],["0","0","0","0","0"],["0","0","0","0","0"],["0","0","8","64","128"],["0","0","16","128","256"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0"],["0","0","0","0","0","0"],["0","0","-4","-24","0","128"],["0","0","-8","-96","-384","-512"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","0"],["0","0","0","0","0","0","0"],["0","0","0","4","48","192","256"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","0","0","0"],["0","0","0","0","0","0"],["0","0","4","24","0","-128"],["0","0","8","88","320","384"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0"],["0","0","0","0","0","0","0"],["0","0","0","-4","-48","-192","-256"]]},"deriv_order":1}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["0","0","8","64","128"]]},"start_base":1},"row_multiplier":["1"],"statement":"mu(x) w(n) M'' = sum_nu H_nu S^nu L + sum_l Z_l A_l (an invariant row-annihilator system of the parent) with M'' the input relation conjugated by lambda(n) binom(n, k+1); so the candidate rows satisfy the input rule at every base n >= 1 (the exceptional bases checked exactly), and agreement on the 2 identifying rows gives Q_n = lambda(n) sum_k u(n,k) [x^k]P_n x^k for every n >= 1"},"index_shift":-1,"input":{"first_index":1,"initial_polynomials":[["1"],["1","1"]],"recurrence":{"denominator":{"coeffs":[["0"],["1"],["2"]]},"terms":[{"coeff":{"coeffs":[["0","4"],["1","-23"],["2","13"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","-1","3"],["0","4","-27/2"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","0","2"],["0","0","-6"],["0","0","5/2"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent":{"first_index":0,"initial_polynomials":[["1"],["1","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","0","-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"}},"method":"hadamard_conjugation"},"status":"certified"},"input_first_index":1,"interlacing":{"reason":"the factor depends on n","status":"none"},"lift_summary":{"hypotheses":[{"evidence":"binom(n, k+1) is defined for every n >= 1","name":"factor_defined","statement":"the factor u(n, k) is defined on the index domain","status":{"kind":"verified"}},{"evidence":"binom(n, k+1): sum_k u(n,k) x^k / k! = L_(A-1)^(1)(-x) with A = n + a (zero when A < 1), a Laguerre polynomial with parameter 1 > -1, whose zeros are real and positive (Szego, Orthogonal Polynomials, Theorem 3.3.1); third condition of Theorem 40","name":"factor_multiplier_sequence","statement":"k -> u(n, k) is a nonnegative multiplier sequence for every n >= n0","status":{"kind":"verified"}},{"evidence":"lambda(n) = numerator(n) / denominator(n) != 0 for every integer n in [1, +inf) (exact; Taylor shift: the coefficients of lambda(n) = numerator(n) / denominator(n) at n = 1 + u have one sign)","name":"gauge_finite_nonzero","sign_decision":{"certificate":{"condition":"nonzero","denominator":["0","1"],"method":{"kind":"taylor_shift","shifted_denominator":["1","1"],"shifted_numerator":["1"]},"numerator":["1"],"range":{"first":"1","last":null}},"decision":"holds"},"statement":"lambda(n) is finite and nonzero for every n >= n0","status":{"kind":"verified"}}],"identity":{"method":"hadamard_conjugation","status":"certified"},"input_first_index":1,"input_interlacing":{"reason":"the factor depends on n","status":"not_proved"},"lean_replay":"not_attempted","operation":{"description":"x^k -> binom(n, k+1) x^k","kind":"preserver_image","operator":{"factor":{"terms":[{"coefficient_offset":1,"index_offset":0,"kind":"binomial"}]},"shape":"hadamard_multiplier"}},"parent":{"gauge":{"denominator":["0","1"],"kind":"closed","numerator":["1"]},"index_shift":-1,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["1","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","0","-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"relation":"Q_n = lambda(n) T_n(P_(n-1)) with T = x^k -> binom(n, k+1) x^k, for every n >= 1"},"parent_proof":{"route":"three_term_recurrence","statement":"every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign","status":"proved"},"root_transfer":{"input_conclusion":"every Q_n, n >= 1, is zero or real-rooted with roots in (-inf, 0]","input_root_region":{"upper":{"closed":true,"value":"0"}},"parent_hypothesis":"every parent row used is zero or real-rooted with all roots in (-inf, 0] (coefficients of one sign)","parent_root_region":{"upper":{"closed":true,"value":"0"}},"theorem":"Polya--Schur characterization of multiplier sequences (G. Polya and I. Schur, J. Reine Angew. Math. 144 (1914) 89--113; stated as Theorem 40 of P. Branden, Unimodality, log-concavity, real-rootedness and beyond, arXiv:1410.6601): a real sequence (lambda_k) is a multiplier sequence (x^k -> lambda_k x^k maps real-rooted polynomials to real-rooted polynomials or zero) iff sum_k binom(m,k) lambda_k x^k is real-rooted with zeros of one sign for every m, iff sum_k lambda_k x^k / k! (or its reflection) is C x^m e^(a x) prod (1 + alpha_j x) with a, alpha_j >= 0; a product of multiplier sequences is one (composition), and a nonzero factor lambda(n) of the row changes nothing"},"verdict":"proved"},"notes":[],"parent_interlacing_report":{"conclusion":{"first_index":0,"interlacing":"strict","interlacing_from":1,"root_region":{"upper":{"closed":false,"value":"0"}},"simple_roots":true,"statement":"every P_n, n >= 0, is nonzero and real-rooted, with simple roots from n = 0 on; P_(n-1) strictly interlaces P_n for n >= 1; every root lies in (-inf, 0)"},"hypotheses":[{"evidence":"f(n) a_n = 1 != 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of f(n) a_n = 1 at n = 2 + u have one sign)","name":"leading_coefficient_nonzero","sign_decision":{"certificate":{"condition":"nonzero","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1"]},"numerator":["1"],"range":{"first":"2","last":null}},"decision":"holds"},"statement":"a_n != 0 for every n >= 2","status":{"kind":"verified"}},{"evidence":"Q_0 has degree 0, Q_1 degree 1; simple real roots and strict interlacing checked exactly","name":"seeds_interlace","statement":"Q_0 and Q_1 have simple real roots, degrees e and e + 1, and Q_0 strictly interlaces Q_1","status":{"kind":"verified"}},{"evidence":"beta_2 = 1 (exact)","name":"first_coefficient_positive","statement":"beta_2 = c_2 L_0 / (a_2 L_1) > 0","status":{"kind":"verified"}},{"evidence":"beta_n = 1 > 0 for every integer n in [3, +inf) (exact; Taylor shift: the coefficients of beta_n = 1 at n = 3 + u have one sign)","name":"recurrence_coefficient_positive","sign_decision":{"certificate":{"condition":"positive","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1"]},"numerator":["1"],"range":{"first":"3","last":null}},"decision":"holds"},"statement":"beta_n = c_n / (a_n a_(n-1)) > 0 for every n >= 3","status":{"kind":"verified"}},{"evidence":"seeds checked exactly; positive-ratio induction at t = 0 with g(n) = (n + 1)/(n) (the exact ratio r_n): g(n) > 0 for n >= 2, r_2 >= g(2) exactly, and (t - alpha_n) - beta_n/g(n-1) - g(n) >= 0 for every integer n in [3, +inf) (exact; Taylor shift: the coefficients of (t - alpha_n) - beta_n/g(n-1) - g(n) at n = 3 + u have one sign)","name":"root_upper_bound","sign_decision":{"certificate":{"condition":"nonnegative","denominator":["0","1"],"method":{"kind":"taylor_shift","shifted_denominator":["3","1"],"shifted_numerator":[]},"numerator":[],"range":{"first":"3","last":null}},"decision":"holds"},"statement":"every root of Q_n is < 0 for every n >= 0 (region (-inf, 0) for P)","status":{"kind":"verified"}}],"lean_replay":"not_attempted","normal_form":"P_n = (a_n + b_n (x + 0)) P_(n-1) - c_n (x + 0)^2 P_(n-2) for n >= 2, with a_n = 1, b_n = 2, c_n = 1; Q_n(y) = y^(d_n) P_n(1/y + 0), d_n = deg P_0 + n - 0, satisfies Q_n = (a_n y + b_n) Q_(n-1) - c_n Q_(n-2)","recurrence":{"first_index":0,"initial_polynomials":[["1"],["1","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","0","-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"reference":"three-term recurrence Q_n = (a_n y + b_n) Q_(n-1) - c_n Q_(n-2) with a_n != 0 and beta_n = c_n / (a_n a_(n-1)) > 0: simple real roots and strict interlacing of consecutive rows (zero separation for orthogonal polynomials: G. Szeg\u0151, Orthogonal Polynomials, \u00a73.3; Favard, C. R. Acad. Sci. Paris 200 (1935)); root regions by a positive-ratio (chain-sequence) induction","requested_root_region":{"upper":{"closed":false,"value":"0"}},"schema":"polytool.recurrence-real-rootedness-theorem.v1","status":"proved","theorem":"three_term_recurrence"},"parent_proof":{"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":"no theorem matched (weighted_renewal_window: support must satisfy offset = 1 + ell * t_degree; fixed_delay_predecessor_window: only P_(n-1) and one term w(n) t P_(n-L) are supported)","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":"P_n = (a_n + b_n (x + 0)) P_(n-1) - c_n (x + 0)^2 P_(n-2) for n >= 2, with a_n = 1, b_n = 2, c_n = 1; Q_n(y) = y^(d_n) P_n(1/y + 0), d_n = deg P_0 + n - 0, satisfies Q_n = (a_n y + b_n) Q_(n-1) - c_n Q_(n-2): every P_n, n >= 0, is nonzero and real-rooted, with simple roots from n = 0 on; P_(n-1) strictly interlaces P_n for n >= 1; every root lies in (-inf, 0)","route":"three_term_recurrence","success":true,"variant":"three_term_recurrence"}],"conditional_on":[],"interlacing":{"from_index":1,"justification":{"premises":["every hypothesis of the theorem is verified exactly for every index: P_n = (a_n + b_n (x + 0)) P_(n-1) - c_n (x + 0)^2 P_(n-2) for n >= 2, with a_n = 1, b_n = 2, c_n = 1; Q_n(y) = y^(d_n) P_n(1/y + 0), d_n = deg P_0 + n - 0, satisfies Q_n = (a_n y + b_n) Q_(n-1) - c_n Q_(n-2)","every P_n, n >= 0, is nonzero and real-rooted, with simple roots from n = 0 on; P_(n-1) strictly interlaces P_n for n >= 1; every root lies in (-inf, 0)"],"theorem":"three_term_recurrence: three-term recurrence Q_n = (a_n y + b_n) Q_(n-1) - c_n Q_(n-2) with a_n != 0 and beta_n = c_n / (a_n a_(n-1)) > 0: simple real roots and strict interlacing of consecutive rows (zero separation for orthogonal polynomials: G. Szeg\u0151, Orthogonal Polynomials, \u00a73.3; Favard, C. R. Acad. Sci. Paris 200 (1935)); root regions by a positive-ratio (chain-sequence) induction"},"kind":"strict","orientation":"previous_interlaces_next"},"route":"three_term_recurrence","rows_checked":10,"statement":"every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign","status":"proved"},"rows_compared":16,"schema":"polytool.recurrence-preserver-image.v1","statement":"proved: Q_n = lambda(n) T_n(P_(n-1)) with T = x^k -> binom(n, k+1) x^k for every n >= 1, the side conditions hold for every n, and every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign; so every Q_n, n >= 1, is zero or real-rooted with roots in (-inf, 0]"},"kind":"preserver_image"}