{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":2,"operator":{"factor":{"terms":[{"coefficient_offset":0,"index_offset":1,"kind":"binomial"}]},"shape":"hadamard_multiplier"},"parent":{"first_index":1,"initial_polynomials":[["1"],["1","1"]],"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-f7935c36a3c0ec8c"},"identifying_rows":3,"identity":{"certificate":{"certificate":{"factor":{"terms":[{"coefficient_offset":0,"index_offset":1,"kind":"binomial"}]},"hadamard":{"conjugated_input_relation":{"terms":[{"coeff":{"coeffs":[["-576","-432","-288","-144"],["-1296","-864","-480","-168"],["-1136","-636","-264","-48"],["-484","-204","-48","0"],["-100","-24","0","0"],["-8","0","0","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","432","144","-144","-432"],["0","864","96","-456","-504"],["0","636","-108","-384","-144"],["0","204","-108","-96","0"],["0","24","-24","0","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0","-144","72","288","-216"],["0","0","-240","228","264","-252"],["0","0","-132","192","12","-72"],["0","0","-24","48","-24","0"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["0","0","0","24","-72","72","-24"],["0","0","0","28","-84","84","-28"],["0","0","0","8","-24","24","-8"]]},"deriv_order":3,"shift":0},{"coeff":{"coeffs":[["5616","-5688","1320"],["10452","-9180","1580"],["7702","-5512","604"],["2808","-1460","72"],["506","-144","0"],["36","0","0"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-2232","-1896","2064"],["0","-3756","-4324","2872"],["0","-2384","-3456","1208"],["0","-676","-1172","144"],["0","-72","-144","0"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["0","0","84","1896","84"],["0","0","214","2428","502"],["0","0","158","1028","302"],["0","0","36","144","36"]]},"deriv_order":2,"shift":1},{"coeff":{"coeffs":[["0","0","0","96","0","-96"],["0","0","0","48","0","-48"]]},"deriv_order":3,"shift":1},{"coeff":{"coeffs":[["-5712","624"],["-10244","1162"],["-7256","783"],["-2539","227"],["-439","24"],["-30","0"]]},"deriv_order":0,"shift":2},{"coeff":{"coeffs":[["0","3480","-744"],["0","5570","-626"],["0","3309","15"],["0","865","119"],["0","84","24"]]},"deriv_order":1,"shift":2},{"coeff":{"coeffs":[["0","0","-684","-684"],["0","0","-894","-894"],["0","0","-384","-384"],["0","0","-54","-54"]]},"deriv_order":2,"shift":2},{"coeff":{"coeffs":[["672"],["1088"],["690"],["215"],["33"],["2"]]},"deriv_order":0,"shift":3}]},"conjugation_x_shift":0,"exceptional_bases":[],"factor":{"terms":[{"coefficient_offset":0,"index_offset":1,"kind":"binomial"}]},"gauge":{"kind":"none"},"identifying_indices":[1,2,3],"input_leader_shift":3,"input_relation":{"terms":[{"coeff":{"coeffs":[["-24","-72","-72","-24"],["-28","-84","-84","-28"],["-8","-24","-24","-8"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["234","-948","330"],["182","-740","230"],["36","-144","36"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","48","0","-48"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["-238","104"],["-169","107"],["-30","24"]]},"deriv_order":0,"shift":2},{"coeff":{"coeffs":[["0","114","-114"],["0","54","-54"]]},"deriv_order":1,"shift":2},{"coeff":{"coeffs":[["28"],["15"],["2"]]},"deriv_order":0,"shift":3}]},"input_valid_from_base":1,"multiplier":["1","4","6","4","1"],"parent":{"first_index":1,"initial_polynomials":[["1","6","1"],["1","15","15","1"]],"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":1,"quotients":[{"differentiations":[{"coeff":{"coeffs":[["0","0","0","34944","-120576","152064","-82176","15744"],["0","0","0","204320","-702640","882000","-473360","89680"],["0","0","0","514848","-1763128","2200296","-1170600","218584"],["0","0","0","731944","-2493504","3088848","-1624960","297672"],["0","0","0","645640","-2185048","2681304","-1390024","248128"],["0","0","0","365952","-1228224","1488960","-757056","130368"],["0","0","0","133232","-442472","528024","-261560","42776"],["0","0","0","30056","-98496","115152","-55040","8328"],["0","0","0","3816","-12296","13992","-6360","848"],["0","0","0","208","-656","720","-304","32"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","-27840","89472","-101376","45696","-5952"],["0","0","0","0","-155920","496576","-554208","242368","-28816"],["0","0","0","0","-371752","1170880","-1282128","538624","-55624"],["0","0","0","0","-491528","1527008","-1631856","648800","-52424"],["0","0","0","0","-393264","1201056","-1243584","457056","-21264"],["0","0","0","0","-194656","582016","-578112","188800","1952"],["0","0","0","0","-58184","169472","-159312","42944","5080"],["0","0","0","0","-9608","27104","-23664","4448","1720"],["0","0","0","0","-672","1824","-1440","96","192"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","5472","-10944","0","10944","-5472"],["0","0","0","0","0","29040","-58080","0","58080","-29040"],["0","0","0","0","0","64512","-129024","0","129024","-64512"],["0","0","0","0","0","77520","-155040","0","155040","-77520"],["0","0","0","0","0","54240","-108480","0","108480","-54240"],["0","0","0","0","0","22032","-44064","0","44064","-22032"],["0","0","0","0","0","4800","-9600","0","9600","-4800"],["0","0","0","0","0","432","-864","0","864","-432"]]},"deriv_order":2}],"shift":0},{"differentiations":[{"coeff":{"coeffs":[["0","0","0","-5376","16128","-16128","5376"],["0","0","0","-30208","90624","-90624","30208"],["0","0","0","-72592","217776","-217776","72592"],["0","0","0","-97528","292584","-292584","97528"],["0","0","0","-80456","241368","-241368","80456"],["0","0","0","-42176","126528","-126528","42176"],["0","0","0","-14048","42144","-42144","14048"],["0","0","0","-2872","8616","-8616","2872"],["0","0","0","-328","984","-984","328"],["0","0","0","-16","48","-48","16"]]},"deriv_order":0}],"shift":1}],"row_annihilator_system":{"generators":[{"annihilator":{"terms":[{"coeff":{"coeffs":[["-1","-3"],["-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","0","30336","-73536","13824","96384","-91776","24768"],["0","0","0","145184","-340544","28896","504736","-459904","121632"],["0","0","0","291456","-654656","-35216","1119024","-971056","250448"],["0","0","0","319624","-677432","-165952","1366208","-1122952","280504"],["0","0","0","209120","-409504","-211392","1000000","-773408","185184"],["0","0","0","83616","-146688","-134336","446976","-322272","72704"],["0","0","0","19984","-29936","-46192","118352","-78304","16096"],["0","0","0","2616","-3080","-8160","16800","-9880","1704"],["0","0","0","144","-112","-576","960","-464","48"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","-37824","106752","-76032","-34176","58560","-17280"],["0","0","0","0","-172544","481568","-341952","-138112","238528","-67488"],["0","0","0","0","-324560","892560","-629152","-222304","384624","-101168"],["0","0","0","0","-325088","876448","-608768","-181504","308960","-70048"],["0","0","0","0","-186752","490112","-331392","-78976","125440","-18432"],["0","0","0","0","-61472","155520","-100480","-16960","20640","2752"],["0","0","0","0","-10736","25840","-15584","-928","-1072","2480"],["0","0","0","0","-768","1728","-960","192","-576","384"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","10272","-24096","20928","-20928","24096","-10272"],["0","0","0","0","0","43408","-100880","83296","-78688","93968","-41104"],["0","0","0","0","0","73472","-168640","130496","-114368","144448","-65408"],["0","0","0","0","0","63264","-142752","101568","-80832","111648","-52896"],["0","0","0","0","0","28960","-63776","40768","-29248","46496","-23200"],["0","0","0","0","0","6608","-14032","7904","-5600","10576","-5456"],["0","0","0","0","0","576","-1152","576","-576","1152","-576"]]},"deriv_order":2},{"coeff":{"coeffs":[["0","0","0","0","0","0","-768","2304","-1536","-1536","2304","-768"],["0","0","0","0","0","0","-2688","8064","-5376","-5376","8064","-2688"],["0","0","0","0","0","0","-3456","10368","-6912","-6912","10368","-3456"],["0","0","0","0","0","0","-1920","5760","-3840","-3840","5760","-1920"],["0","0","0","0","0","0","-384","1152","-768","-768","1152","-384"]]},"deriv_order":3}],"step_multiplier":{"coeffs":[["0","-2","2"],["0","-4","4"],["0","-2","2"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","-4","8","-4"],["0","-6","12","-6"],["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":[["1"],["3"],["2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-1","-1"],["0","-4"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-2","2"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","28416","-85248","56832","56832","-85248","28416"],["0","0","0","0","129904","-386256","259616","239648","-362640","119728"],["0","0","0","0","245032","-719928","486320","410288","-624984","203272"],["0","0","0","0","246328","-712040","480208","368336","-560776","177944"],["0","0","0","0","142192","-401872","267168","187808","-280592","85296"],["0","0","0","0","47104","-129024","82688","55040","-77568","21760"],["0","0","0","0","8296","-21752","12976","8624","-10648","2504"],["0","0","0","0","600","-1480","784","528","-488","56"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","-9408","21312","-18432","21504","-25920","10944"],["0","0","0","0","0","-39840","89184","-72192","79872","-100704","43680"],["0","0","0","0","0","-67616","148960","-110336","113408","-153568","69152"],["0","0","0","0","0","-58432","125888","-82432","76288","-116672","55360"],["0","0","0","0","0","-26880","56064","-30720","24576","-46848","23808"],["0","0","0","0","0","-6176","12256","-5120","3584","-9952","5408"],["0","0","0","0","0","-544","992","-256","256","-992","544"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","768","-2304","1536","1536","-2304","768"],["0","0","0","0","0","0","2688","-8064","5376","5376","-8064","2688"],["0","0","0","0","0","0","3456","-10368","6912","6912","-10368","3456"],["0","0","0","0","0","0","1920","-5760","3840","3840","-5760","1920"],["0","0","0","0","0","0","384","-1152","768","768","-1152","384"]]},"deriv_order":2}],"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","24","-48","24"],["0","0","76","-152","76"],["0","0","88","-176","88"],["0","0","44","-88","44"],["0","0","8","-16","8"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","-4","-12","36","-20"],["0","0","-8","-40","104","-56"],["0","0","-4","-44","100","-52"],["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","12","-12","-12","12"],["0","0","28","-20","-44","36"],["0","0","20","-4","-52","36"],["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","0","-8","24","-24","8"]]},"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+1, k); so the candidate rows satisfy the input rule at every base n >= 1 (the exceptional bases checked exactly), and agreement on the 3 identifying rows gives Q_n = lambda(n) sum_k u(n,k) [x^k]P_n x^k for every n >= 1"},"index_shift":2,"input":{"first_index":1,"initial_polynomials":[["1","12","1"],["1","45","45","1"],["1","112","420","112","1"]],"recurrence":{"denominator":{"coeffs":[["1"],["3"],["2"]]},"terms":[{"coeff":{"coeffs":[["1","1"],["-11","37"],["30","-24"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","48","-48"],["0","-54","54"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-12","24","36"],["34","-124","-14"],["-36","144","-36"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["0","-48","0","48"]]},"deriv_order":1,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["12","36","36","12"],["-20","-60","-60","-20"],["8","24","24","8"]]},"deriv_order":0,"offset":3,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent":{"first_index":1,"initial_polynomials":[["1"],["1","1"]],"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":1,"interlacing":{"reason":"the factor depends on n","status":"none"},"lift_summary":{"hypotheses":[{"evidence":"binom(n+1, k) 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+1, 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":1,"input_interlacing":{"reason":"the factor depends on n","status":"not_proved"},"lean_replay":"not_attempted","operation":{"description":"x^k -> binom(n+1, k) x^k","kind":"preserver_image","operator":{"factor":{"terms":[{"coefficient_offset":0,"index_offset":1,"kind":"binomial"}]},"shape":"hadamard_multiplier"}},"parent":{"gauge":{"kind":"none"},"index_shift":2,"recurrence":{"first_index":1,"initial_polynomials":[["1"],["1","1"]],"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+2)) with T = x^k -> binom(n+1, k) x^k, for every n >= 1"},"parent_proof":{"route":"three_term_recurrence","statement":"every parent row P_n, n >= 1, 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":1,"interlacing":"strict","interlacing_from":2,"root_region":{"upper":{"closed":false,"value":"0"}},"simple_roots":true,"statement":"every P_n, n >= 1, is nonzero and real-rooted, with simple roots from n = 1 on; P_(n-1) strictly interlaces P_n for n >= 2; every root lies in (-inf, 0)"},"hypotheses":[{"evidence":"f(n) a_n = 4 != 0 for every integer n in [3, +inf) (exact; Taylor shift: the coefficients of f(n) a_n = 4 at n = 3 + 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":"3","last":null}},"decision":"holds"},"statement":"a_n != 0 for every n >= 3","status":{"kind":"verified"}},{"evidence":"Q_1 has degree 0, Q_2 degree 1; simple real roots and strict interlacing checked exactly","name":"seeds_interlace","statement":"Q_1 and Q_2 have simple real roots, degrees e and e + 1, and Q_1 strictly interlaces Q_2","status":{"kind":"verified"}},{"evidence":"beta_3 = 1/8 (exact)","name":"first_coefficient_positive","statement":"beta_3 = c_3 L_1 / (a_3 L_2) > 0","status":{"kind":"verified"}},{"evidence":"beta_n = 1/16 > 0 for every integer n in [4, +inf) (exact; Taylor shift: the coefficients of beta_n = 1/16 at n = 4 + 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":"4","last":null}},"decision":"holds"},"statement":"beta_n = c_n / (a_n a_(n-1)) > 0 for every n >= 4","status":{"kind":"verified"}},{"evidence":"seeds checked exactly; positive-ratio induction at t = 0 with g(n) = 1/4 (the exact ratio r_n): g(n) > 0 for n >= 3, r_3 >= g(3) exactly, and (t - alpha_n) - beta_n/g(n-1) - g(n) >= 0 for every integer n in [4, +inf) (exact; Taylor shift: the coefficients of (t - alpha_n) - beta_n/g(n-1) - g(n) at n = 4 + u have one sign)","name":"root_upper_bound","sign_decision":{"certificate":{"condition":"nonnegative","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":[]},"numerator":[],"range":{"first":"4","last":null}},"decision":"holds"},"statement":"every root of Q_n is < 0 for every n >= 1 (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 (the exact ratio r_n): g(n) > 0 for n >= 3, r_3 >= g(3) exactly, and (t - alpha_n) - beta_n/g(n-1) - g(n) >= 0 for every integer n in [4, +inf) (exact; Taylor shift: the coefficients of (t - alpha_n) - beta_n/g(n-1) - g(n) at n = 4 + u have one sign)","name":"root_lower_bound","sign_decision":{"certificate":{"condition":"nonnegative","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":[]},"numerator":[],"range":{"first":"4","last":null}},"decision":"holds"},"statement":"every root of Q_n is > -1 for every n >= 1 (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 >= 3, 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_1 + n - 1, satisfies Q_n = (a_n y + b_n) Q_(n-1) - c_n Q_(n-2)","recurrence":{"first_index":1,"initial_polynomials":[["1"],["1","1"]],"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 >= 3, 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_1 + n - 1, satisfies Q_n = (a_n y + b_n) Q_(n-1) - c_n Q_(n-2): every P_n, n >= 1, is nonzero and real-rooted, with simple roots from n = 1 on; P_(n-1) strictly interlaces P_n for n >= 2; every root lies in (-inf, 0)","route":"three_term_recurrence","success":true,"variant":"three_term_recurrence"}],"conditional_on":[],"interlacing":{"from_index":2,"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 >= 3, 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_1 + n - 1, satisfies Q_n = (a_n y + b_n) Q_(n-1) - c_n Q_(n-2)","every P_n, n >= 1, is nonzero and real-rooted, with simple roots from n = 1 on; P_(n-1) strictly interlaces P_n for n >= 2; 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 >= 1, 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+2)) with T = x^k -> binom(n+1, k) x^k for every n >= 1, the side conditions hold for every n, and every parent row P_n, n >= 1, 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"}