{"certification":{"candidate":{"gauge":{"denominator":["2","3","1"],"kind":"closed","numerator":["1"]},"index_shift":0,"operator":{"factor":{"terms":[{"coefficient_offset":1,"index_offset":2,"kind":"binomial"}]},"shape":"hadamard_multiplier"},"parent":{"first_index":0,"initial_polynomials":[["1"],["2","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-1","2","-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"n-2245b35ec7cd4857"},"identifying_rows":2,"identity":{"certificate":{"certificate":{"factor":{"terms":[{"coefficient_offset":1,"index_offset":2,"kind":"binomial"}]},"hadamard":{"conjugated_input_relation":{"terms":[{"coeff":{"coeffs":[["-2592","-3456","-2592"],["-10152","-12384","-7992"],["-16848","-18336","-9756"],["-15522","-14584","-6060"],["-8704","-6744","-2028"],["-3048","-1816","-348"],["-652","-264","-24"],["-78","-16","0"],["-4","0","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","1728","864","-2592"],["0","6192","1800","-7992"],["0","9168","588","-9756"],["0","7292","-1232","-6060"],["0","3372","-1344","-2028"],["0","908","-560","-348"],["0","132","-108","-24"],["0","8","-8","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0","-432","864","-432"],["0","0","-1332","2664","-1332"],["0","0","-1626","3252","-1626"],["0","0","-1010","2020","-1010"],["0","0","-338","676","-338"],["0","0","-58","116","-58"],["0","0","-4","8","-4"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["-4752","-9216"],["-14148","-31632"],["-16596","-44764"],["-9707","-34038"],["-2760","-15074"],["-172","-3898"],["106","-546"],["27","-32"],["2","0"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-4464","4464"],["0","-16044","9996"],["0","-23752","6544"],["0","-18825","-459"],["0","-8651","-2389"],["0","-2311","-1121"],["0","-333","-219"],["0","-20","-16"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["0","0","3024","3024"],["0","0","8604","8604"],["0","0","9642","9642"],["0","0","5520","5520"],["0","0","1716","1716"],["0","0","276","276"],["0","0","18","18"]]},"deriv_order":2,"shift":1},{"coeff":{"coeffs":[["4032"],["13920"],["20140"],["16080"],["7791"],["2355"],["435"],["45"],["2"]]},"deriv_order":0,"shift":2}]},"conjugation_x_shift":0,"exceptional_bases":[],"factor":{"terms":[{"coefficient_offset":1,"index_offset":2,"kind":"binomial"}]},"gauge":{"denominator":["2","3","1"],"kind":"closed","numerator":["1"]},"identifying_indices":[0,1],"input_leader_shift":2,"input_relation":{"terms":[{"coeff":{"coeffs":[["-6","-12","-6"],["-10","-20","-10"],["-4","-8","-4"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-22","-64"],["-5","-65"],["2","-16"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-42","42"],["0","-18","18"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["28"],["15"],["2"]]},"deriv_order":0,"shift":2}]},"input_valid_from_base":0,"multiplier":["1","3","3","1"],"parent":{"first_index":0,"initial_polynomials":[["1"],["2","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-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"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-2","-2"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"shift":2}]},"parent_valid_from_base":0,"quotients":[{"differentiations":[{"coeff":{"coeffs":[["0","0","16128","-32256","16128"],["0","0","104064","-208128","104064"],["0","0","295984","-591968","295984"],["0","0","489168","-978336","489168"],["0","0","521484","-1042968","521484"],["0","0","376432","-752864","376432"],["0","0","187812","-375624","187812"],["0","0","64824","-129648","64824"],["0","0","15188","-30376","15188"],["0","0","2304","-4608","2304"],["0","0","204","-408","204"],["0","0","8","-16","8"]]},"deriv_order":0}],"shift":0}],"row_annihilator_system":{"generators":[{"annihilator":{"terms":[{"coeff":{"coeffs":[["-2","-2"],["-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","13248","-31104","22464","-4608"],["0","0","81264","-186912","130032","-24384"],["0","0","217520","-487920","323280","-52880"],["0","0","334052","-726656","451156","-58552"],["0","0","325648","-682224","387504","-30928"],["0","0","210540","-421280","210940","-200"],["0","0","91496","-173168","71848","9824"],["0","0","26428","-46784","14284","6072"],["0","0","4864","-7952","1312","1776"],["0","0","516","-768","-12","264"],["0","0","24","-32","-8","16"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-17856","53568","-53568","17856"],["0","0","0","-99888","275472","-251280","75696"],["0","0","0","-241216","606432","-489216","124000"],["0","0","0","-329492","749484","-510492","90500"],["0","0","0","-280212","573372","-306108","12948"],["0","0","0","-153752","282072","-102888","-25432"],["0","0","0","-54424","89448","-15624","-19400"],["0","0","0","-11988","17676","612","-6300"],["0","0","0","-1492","1980","516","-1004"],["0","0","0","-80","96","48","-64"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","12096","-12096","-12096","12096"],["0","0","0","0","58608","-58608","-58608","58608"],["0","0","0","0","119496","-119496","-119496","119496"],["0","0","0","0","133632","-133632","-133632","133632"],["0","0","0","0","89592","-89592","-89592","89592"],["0","0","0","0","36912","-36912","-36912","36912"],["0","0","0","0","9144","-9144","-9144","9144"],["0","0","0","0","1248","-1248","-1248","1248"],["0","0","0","0","72","-72","-72","72"]]},"deriv_order":2}],"step_multiplier":{"coeffs":[["0","-2","2"],["0","-4","4"],["0","-2","2"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","-2","4","-2"],["0","-4","8","-4"],["0","-2","4","-2"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","4","-8","4"],["0","0","4","-8","4"]]},"deriv_order":1}],[{"coeff":{"coeffs":[["0","0","-4","8","-4"],["0","0","-4","8","-4"]]},"deriv_order":0}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0"],["1"],["2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-3","1"],["0","-4"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-2","2"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","12672","-50112","62208","-24768"],["0","0","0","69792","-255888","302400","-116304"],["0","0","0","166000","-558888","619776","-226888"],["0","0","0","223560","-684816","698952","-237696"],["0","0","0","187756","-519228","475188","-143716"],["0","0","0","101956","-253188","200508","-49276"],["0","0","0","35800","-79632","51864","-8032"],["0","0","0","7840","-15624","7728","56"],["0","0","0","972","-1740","564","204"],["0","0","0","52","-84","12","20"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","-12096","12096","12096","-12096"],["0","0","0","0","-58608","58608","58608","-58608"],["0","0","0","0","-119496","119496","119496","-119496"],["0","0","0","0","-133632","133632","133632","-133632"],["0","0","0","0","-89592","89592","89592","-89592"],["0","0","0","0","-36912","36912","36912","-36912"],["0","0","0","0","-9144","9144","9144","-9144"],["0","0","0","0","-1248","1248","1248","-1248"],["0","0","0","0","-72","72","72","-72"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["0","0","4","-8","4"],["0","0","12","-24","12"],["0","0","12","-24","12"],["0","0","4","-8","4"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","12","-24","12"],["0","0","44","-88","44"],["0","0","60","-120","60"],["0","0","36","-72","36"],["0","0","8","-16","8"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","-12","12","12","-12"],["0","0","-24","8","56","-40"],["0","0","-12","-20","76","-44"],["0","0","0","-16","32","-16"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","-8","24","-24","8"],["0","0","0","-16","48","-48","16"],["0","0","0","-8","24","-24","8"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","16","-24","0","8"],["0","0","36","-44","-20","28"],["0","0","24","-16","-40","32"],["0","0","4","4","-20","12"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","8","-24","24","-8"],["0","0","0","16","-48","48","-16"],["0","0","0","8","-24","24","-8"]]},"deriv_order":1}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["0","0","4","-8","4"]]},"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+2, k+1); 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":[["6"],["7"],["2"]]},"terms":[{"coeff":{"coeffs":[["4","-2"],["13","1"],["-2","16"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","6","-6"],["0","18","-18"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["2","4","2"],["-6","-12","-6"],["4","8","4"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent":{"first_index":0,"initial_polynomials":[["1"],["2","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-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+2, k+1) 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+2, 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 [0, +inf) (exact; Taylor shift: the coefficients of lambda(n) = numerator(n) / denominator(n) at n = 0 + u have one sign)","name":"gauge_finite_nonzero","sign_decision":{"certificate":{"condition":"nonzero","denominator":["2","3","1"],"method":{"kind":"taylor_shift","shifted_denominator":["2","3","1"],"shifted_numerator":["1"]},"numerator":["1"],"range":{"first":"0","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":0,"input_interlacing":{"reason":"the factor depends on n","status":"not_proved"},"lean_replay":"not_attempted","operation":{"description":"x^k -> binom(n+2, k+1) x^k","kind":"preserver_image","operator":{"factor":{"terms":[{"coefficient_offset":1,"index_offset":2,"kind":"binomial"}]},"shape":"hadamard_multiplier"}},"parent":{"gauge":{"denominator":["2","3","1"],"kind":"closed","numerator":["1"]},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["2","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-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+2, k+1) 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) a_n = 4 != 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of f(n) a_n = 4 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":["4"]},"numerator":["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/16 (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 > 0 for every integer n in [3, +inf) (exact; Taylor shift: the coefficients of beta_n = 1/16 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/16"]},"numerator":["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 + 1/4)/(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"}},{"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 + 1/4)/(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_lower_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 > -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, b_n = 2, c_n = 1; 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"],["2","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-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 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: coefficient of P_(n-1) must be 1 after normalization; fixed_delay_predecessor_window: coefficient of P_(n-1) must be 1 (+ w(n) t) after normalization)","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, b_n = 2, c_n = 1; 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, b_n = 2, c_n = 1; 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+2, k+1) 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"}