{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"factor":{"terms":[{"coefficient_offset":0,"index_offset":0,"kind":"binomial"}]},"shape":"hadamard_multiplier"},"parent":{"first_index":0,"initial_polynomials":[["1"],["1","1"]],"recurrence":{"denominator":{"coeffs":[["0"],["1"]]},"terms":[{"coeff":{"coeffs":[["-1","-1"],["2","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["1","-2","1"],["-1","2","-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"n-b13531ad79e7c629"},"identifying_rows":2,"identity":{"certificate":{"certificate":{"factor":{"terms":[{"coefficient_offset":0,"index_offset":0,"kind":"binomial"}]},"hadamard":{"conjugated_input_relation":{"terms":[{"coeff":{"coeffs":[["-4","-4","-4"],["-14","-12","-8"],["-18","-12","-4"],["-10","-4","0"],["-2","0","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","4","4","-8"],["0","12","4","-16"],["0","12","-4","-8"],["0","4","-4","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0","-2","4","-2"],["0","0","-4","8","-4"],["0","0","-2","4","-2"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["-4","-14"],["-6","-35"],["0","-29"],["3","-8"],["1","0"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-10","10"],["0","-31","7"],["0","-31","-11"],["0","-10","-8"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["0","0","12","12"],["0","0","21","21"],["0","0","9","9"]]},"deriv_order":2,"shift":1},{"coeff":{"coeffs":[["8"],["20"],["18"],["7"],["1"]]},"deriv_order":0,"shift":2}]},"conjugation_x_shift":0,"exceptional_bases":[],"factor":{"terms":[{"coefficient_offset":0,"index_offset":0,"kind":"binomial"}]},"gauge":{"kind":"none"},"identifying_indices":[0,1],"input_leader_shift":2,"input_relation":{"terms":[{"coeff":{"coeffs":[["-2","-4","-2"],["-4","-8","-4"],["-2","-4","-2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-2","-14"],["0","-21"],["1","-8"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-12","12"],["0","-9","9"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["4"],["4"],["1"]]},"deriv_order":0,"shift":2}]},"input_valid_from_base":0,"multiplier":["2","7","9","5","1"],"parent":{"first_index":0,"initial_polynomials":[["1"],["1","1"]],"recurrence":{"denominator":{"coeffs":[["0"],["1"]]},"terms":[{"coeff":{"coeffs":[["-1","-1"],["2","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["1","-2","1"],["-1","2","-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_leader_shift":2,"parent_relation":{"terms":[{"coeff":{"coeffs":[["1","-2","1"],["1","-2","1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-3","-3"],["-2","-2"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["2"],["1"]]},"deriv_order":0,"shift":2}]},"parent_valid_from_base":0,"quotients":[{"differentiations":[{"coeff":{"coeffs":[["0","0","8","-16","8"],["0","0","44","-88","44"],["0","0","102","-204","102"],["0","0","129","-258","129"],["0","0","96","-192","96"],["0","0","42","-84","42"],["0","0","10","-20","10"],["0","0","1","-2","1"]]},"deriv_order":0}],"shift":0}],"row_annihilator_system":{"generators":[{"annihilator":{"terms":[{"coeff":{"coeffs":[["-1","-1"],["-1","-3"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","-2","2"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["1"],["1"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","16","-36","24","-4"],["0","0","92","-200","124","-16"],["0","0","224","-467","262","-19"],["0","0","299","-592","287","6"],["0","0","236","-438","168","34"],["0","0","110","-188","46","32"],["0","0","28","-43","2","13"],["0","0","3","-4","-1","2"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-20","60","-60","20"],["0","0","0","-112","288","-240","64"],["0","0","0","-257","567","-363","53"],["0","0","0","-309","585","-243","-33"],["0","0","0","-205","333","-51","-77"],["0","0","0","-71","99","15","-43"],["0","0","0","-10","12","6","-8"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","24","-24","-24","24"],["0","0","0","0","102","-102","-102","102"],["0","0","0","0","171","-171","-171","171"],["0","0","0","0","141","-141","-141","141"],["0","0","0","0","57","-57","-57","57"],["0","0","0","0","9","-9","-9","9"]]},"deriv_order":2}],"step_multiplier":{"coeffs":[["0","-1","1"],["0","-2","2"],["0","-1","1"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","-2","4","-2"],["0","-5","10","-5"],["0","-4","8","-4"],["0","-1","2","-1"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","4","-8","4"],["0","0","6","-12","6"],["0","0","2","-4","2"]]},"deriv_order":1}],[{"coeff":{"coeffs":[["0","0","-8","16","-8"],["0","0","-12","24","-12"],["0","0","-4","8","-4"]]},"deriv_order":0}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0"],["0"],["1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-1","1"],["0","-2"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-1","1"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","20","-108","156","-68"],["0","0","0","120","-516","672","-276"],["0","0","0","291","-1011","1149","-429"],["0","0","0","366","-1038","978","-306"],["0","0","0","252","-588","420","-84"],["0","0","0","90","-174","78","6"],["0","0","0","13","-21","3","5"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","-48","48","48","-48"],["0","0","0","0","-204","204","204","-204"],["0","0","0","0","-342","342","342","-342"],["0","0","0","0","-282","282","282","-282"],["0","0","0","0","-114","114","114","-114"],["0","0","0","0","-18","18","18","-18"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["0","0","1","-2","1"],["0","0","3","-6","3"],["0","0","3","-6","3"],["0","0","1","-2","1"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","2","-4","2"],["0","0","9","-18","9"],["0","0","16","-32","16"],["0","0","14","-28","14"],["0","0","6","-12","6"],["0","0","1","-2","1"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","-2","2","2","-2"],["0","0","-5","1","13","-9"],["0","0","-4","-6","24","-14"],["0","0","-1","-7","17","-9"],["0","0","0","-2","4","-2"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","-2","6","-6","2"],["0","0","0","-5","15","-15","5"],["0","0","0","-4","12","-12","4"],["0","0","0","-1","3","-3","1"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","6","-10","2","2"],["0","0","17","-23","-5","11"],["0","0","17","-15","-21","19"],["0","0","7","-1","-19","13"],["0","0","1","1","-5","3"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","4","-12","12","-4"],["0","0","0","10","-30","30","-10"],["0","0","0","8","-24","24","-8"],["0","0","0","2","-6","6","-2"]]},"deriv_order":1}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["0","0","1","-2","1"]]},"start_base":0},"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); so the candidate rows satisfy the input rule at every base n >= 0 (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 >= 0"},"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["1"],["1","1"]],"recurrence":{"denominator":{"coeffs":[["0"],["0"],["1"]]},"terms":[{"coeff":{"coeffs":[["-2","4"],["4","-11"],["-1","8"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","-6","6"],["0","9","-9"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["2","4","2"],["-4","-8","-4"],["2","4","2"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent":{"first_index":0,"initial_polynomials":[["1"],["1","1"]],"recurrence":{"denominator":{"coeffs":[["0"],["1"]]},"terms":[{"coeff":{"coeffs":[["-1","-1"],["2","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["1","-2","1"],["-1","2","-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"}},"method":"hadamard_conjugation"},"status":"certified"},"input_first_index":0,"interlacing":{"reason":"the factor depends on n","status":"none"},"lift_summary":{"hypotheses":[{"evidence":"binom(n, k) is defined for every n >= 0","name":"factor_defined","statement":"the factor u(n, k) is defined on the index domain","status":{"kind":"verified"}},{"evidence":"binom(n, k): sum_k u(n,k) x^k / k! = L_(A-0)^(0)(-x) with A = n + a (zero when A < 0), a Laguerre polynomial with parameter 0 > -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) = 1","name":"gauge_finite_nonzero","statement":"lambda(n) is finite and nonzero for every n >= n0","status":{"kind":"verified"}}],"identity":{"method":"hadamard_conjugation","status":"certified"},"input_first_index":0,"input_interlacing":{"reason":"the factor depends on n","status":"not_proved"},"lean_replay":"not_attempted","operation":{"description":"x^k -> binom(n, k) x^k","kind":"preserver_image","operator":{"factor":{"terms":[{"coefficient_offset":0,"index_offset":0,"kind":"binomial"}]},"shape":"hadamard_multiplier"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["1","1"]],"recurrence":{"denominator":{"coeffs":[["0"],["1"]]},"terms":[{"coeff":{"coeffs":[["-1","-1"],["2","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["1","-2","1"],["-1","2","-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"relation":"Q_n = lambda(n) T_n(P_(n+0)) with T = x^k -> binom(n, k) x^k, for every n >= 0"},"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 >= 0, 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) = n != 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of f(n) = n at n = 2 + u have one sign)","name":"left_factor_nonzero","sign_decision":{"certificate":{"condition":"nonzero","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["2","1"]},"numerator":["0","1"],"range":{"first":"2","last":null}},"decision":"holds"},"statement":"the left-hand factor f(n) is nonzero for every n >= 2","status":{"kind":"verified"}},{"evidence":"f(n) a_n = 4 n - 2 != 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of f(n) a_n = 4 n - 2 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":["6","4"]},"numerator":["-2","4"],"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/12 (exact)","name":"first_coefficient_positive","statement":"beta_2 = c_2 L_0 / (a_2 L_1) > 0","status":{"kind":"verified"}},{"evidence":"beta_n = (1/16 n^2 - 1/8 n + 1/16)/(n^2 - 2 n + 3/4) > 0 for every integer n in [3, +inf) (exact; Taylor shift: the coefficients of beta_n = (1/16 n^2 - 1/8 n + 1/16)/(n^2 - 2 n + 3/4) at n = 3 + u have one sign)","name":"recurrence_coefficient_positive","sign_decision":{"certificate":{"condition":"positive","denominator":["3/4","-2","1"],"method":{"kind":"taylor_shift","shifted_denominator":["15/4","4","1"],"shifted_numerator":["1/4","1/4","1/16"]},"numerator":["1/16","-1/8","1/16"],"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) = (1/4 n)/(n - 1/2) (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":["-3/16","23/16","-17/4","6","-4","1"],"method":{"kind":"taylor_shift","shifted_denominator":["375/8","1775/16","415/4","48","11","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"}},{"evidence":"on the reflected rows (-1)^(deg) p_n(-y): seeds checked exactly; positive-ratio induction at t = 1 with g(n) = (1/4 n)/(n - 1/2) (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_lower_bound","sign_decision":{"certificate":{"condition":"nonnegative","denominator":["-3/16","23/16","-17/4","6","-4","1"],"method":{"kind":"taylor_shift","shifted_denominator":["375/8","1775/16","415/4","48","11","1"],"shifted_numerator":[]},"numerator":[],"range":{"first":"3","last":null}},"decision":"holds"},"statement":"every root of Q_n is > -1 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 - 1)) P_(n-1) - c_n (x - 1)^2 P_(n-2) for n >= 2, with a_n = (4 n - 2)/(n), b_n = (2 n - 1)/(n), c_n = (n - 1)/(n); Q_n(y) = y^(d_n) P_n(1/y + 1), 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","1"]],"recurrence":{"denominator":{"coeffs":[["0"],["1"]]},"terms":[{"coeff":{"coeffs":[["-1","-1"],["2","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["1","-2","1"],["-1","2","-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 leader is not a nonzero constant","route":"periodic_product","success":false,"variant":"P_(n+k) = c(x) P_n"},{"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":"P_n = (a_n + b_n (x - 1)) P_(n-1) - c_n (x - 1)^2 P_(n-2) for n >= 2, with a_n = (4 n - 2)/(n), b_n = (2 n - 1)/(n), c_n = (n - 1)/(n); Q_n(y) = y^(d_n) P_n(1/y + 1), 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 - 1)) P_(n-1) - c_n (x - 1)^2 P_(n-2) for n >= 2, with a_n = (4 n - 2)/(n), b_n = (2 n - 1)/(n), c_n = (n - 1)/(n); Q_n(y) = y^(d_n) P_n(1/y + 1), 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+0)) with T = x^k -> binom(n, k) x^k for every n >= 0, 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 >= 0, is zero or real-rooted with roots in (-inf, 0]"},"kind":"preserver_image"}