{"certification":{"candidate":{"gauge":{"denominator":["3","4","1"],"kind":"closed","numerator":["1"]},"index_shift":1,"operator":{"factor":{"terms":[{"coefficient_offset":1,"index_offset":1,"kind":"binomial"}]},"shape":"hadamard_multiplier"},"parent":{"first_index":0,"initial_polynomials":[["2"],["3","2"]],"recurrence":{"denominator":{"coeffs":[["3"],["7"],["2"]]},"terms":[{"coeff":{"coeffs":[["6","0"],["8","8"],["4","4"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["3","-6","3"],["-1","2","-1"],["-2","4","-2"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"n-c963abfc0266d66c"},"identifying_rows":2,"identity":{"certificate":{"certificate":{"factor":{"terms":[{"coefficient_offset":1,"index_offset":1,"kind":"binomial"}]},"hadamard":{"conjugated_input_relation":{"terms":[{"coeff":{"coeffs":[["-960","-1920","-2880"],["-4112","-7264","-8016"],["-7384","-11136","-8688"],["-7260","-8952","-4740"],["-4278","-4080","-1380"],["-1548","-1056","-204"],["-336","-144","-12"],["-40","-8","0"],["-2","0","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","960","1920","-2880"],["0","3632","4384","-8016"],["0","5568","3120","-8688"],["0","4476","264","-4740"],["0","2040","-660","-1380"],["0","528","-324","-204"],["0","72","-60","-12"],["0","4","-4","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0","-480","960","-480"],["0","0","-1336","2672","-1336"],["0","0","-1448","2896","-1448"],["0","0","-790","1580","-790"],["0","0","-230","460","-230"],["0","0","-34","68","-34"],["0","0","-2","4","-2"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["-4680","-10080"],["-14316","-31776"],["-17506","-40792"],["-11021","-27888"],["-3731","-11024"],["-594","-2528"],["-4","-312"],["11","-16"],["1","0"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-360","3060"],["0","-3912","5712"],["0","-8878","1915"],["0","-8682","-2316"],["0","-4412","-2254"],["0","-1220","-796"],["0","-174","-129"],["0","-10","-8"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["0","0","2700","2700"],["0","0","7200","7200"],["0","0","7437","7437"],["0","0","3876","3876"],["0","0","1086","1086"],["0","0","156","156"],["0","0","9","9"]]},"deriv_order":2,"shift":1},{"coeff":{"coeffs":[["4320"],["14184"],["19284"],["14294"],["6349"],["1736"],["286"],["26"],["1"]]},"deriv_order":0,"shift":2}]},"conjugation_x_shift":0,"exceptional_bases":[],"factor":{"terms":[{"coefficient_offset":1,"index_offset":1,"kind":"binomial"}]},"gauge":{"denominator":["3","4","1"],"kind":"closed","numerator":["1"]},"identifying_indices":[0,1],"input_leader_shift":2,"input_relation":{"terms":[{"coeff":{"coeffs":[["-4","-8","-4"],["-6","-12","-6"],["-2","-4","-2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-26","-56"],["-5","-44"],["1","-8"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-30","30"],["0","-9","9"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["30"],["11"],["1"]]},"deriv_order":0,"shift":2}]},"input_valid_from_base":0,"multiplier":["141750","290925","258660","130089","40472","7975","972","67","2"],"parent":{"first_index":0,"initial_polynomials":[["3","2"],["4","8","2"]],"recurrence":{"denominator":{"coeffs":[["12"],["11"],["2"]]},"terms":[{"coeff":{"coeffs":[["18","12"],["16","16"],["4","4"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","0","0"],["-5","10","-5"],["-2","4","-2"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_leader_shift":2,"parent_relation":{"terms":[{"coeff":{"coeffs":[["18","-36","18"],["13","-26","13"],["2","-4","2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-66","-60"],["-32","-32"],["-4","-4"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["42"],["19"],["2"]]},"deriv_order":0,"shift":2}]},"parent_valid_from_base":0,"quotients":[{"differentiations":[{"coeff":{"coeffs":[["0","0","14580000","-29160000","14580000"],["0","0","71199000","-142398000","71199000"],["0","0","157034700","-314069400","157034700"],["0","0","208122210","-416244420","208122210"],["0","0","185668623","-371337246","185668623"],["0","0","118181946","-236363892","118181946"],["0","0","55435597","-110871194","55435597"],["0","0","19490276","-38980552","19490276"],["0","0","5166310","-10332620","5166310"],["0","0","1028284","-2056568","1028284"],["0","0","151382","-302764","151382"],["0","0","15994","-31988","15994"],["0","0","1147","-2294","1147"],["0","0","50","-100","50"],["0","0","1","-2","1"]]},"deriv_order":0}],"shift":0}],"row_annihilator_system":{"generators":[{"annihilator":{"terms":[{"coeff":{"coeffs":[["-20","-22"],["-9","-17"],["-1","-3"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","-7","7"],["0","-2","2"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["15"],["8"],["1"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","19926000","-76788000","93798000","-36936000"],["0","0","107697600","-375580800","428068800","-160185600"],["0","0","264172320","-832131360","871745760","-303786720"],["0","0","390529548","-1111945464","1052302284","-330886368"],["0","0","389250081","-1004490054","841229865","-225989892"],["0","0","276998153","-650557706","470120953","-96561400"],["0","0","145242746","-312092544","188456850","-21607052"],["0","0","57039564","-112818456","54518220","1260672"],["0","0","16866998","-30911284","11221574","2822712"],["0","0","3738734","-6392268","1568334","1085200"],["0","0","611688","-982440","129816","240936"],["0","0","71648","-108832","2720","34464"],["0","0","5681","-8214","-615","3148"],["0","0","273","-378","-63","168"],["0","0","6","-8","-2","4"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-3402000","35721000","-61236000","28917000"],["0","0","0","-42136200","182177100","-237945600","97904700"],["0","0","0","-143278740","414061470","-398286720","127503990"],["0","0","0","-245589966","556941933","-377113968","65762001"],["0","0","0","-257538330","496100646","-219586302","-18976014"],["0","0","0","-180827548","309862536","-77242428","-51792560"],["0","0","0","-89128896","139936464","-12486240","-38321328"],["0","0","0","-31580276","46352682","2035464","-16807870"],["0","0","0","-8103148","11279304","1750836","-4926992"],["0","0","0","-1494648","1993980","495984","-995316"],["0","0","0","-193340","249186","81648","-137494"],["0","0","0","-16654","20865","8232","-12443"],["0","0","0","-858","1050","474","-666"],["0","0","0","-20","24","12","-16"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","25515000","-25515000","-25515000","25515000"],["0","0","0","0","106798500","-106798500","-106798500","106798500"],["0","0","0","0","197822250","-197822250","-197822250","197822250"],["0","0","0","0","215816535","-215816535","-215816535","215816535"],["0","0","0","0","155118726","-155118726","-155118726","155118726"],["0","0","0","0","77617344","-77617344","-77617344","77617344"],["0","0","0","0","27784464","-27784464","-27784464","27784464"],["0","0","0","0","7180782","-7180782","-7180782","7180782"],["0","0","0","0","1331424","-1331424","-1331424","1331424"],["0","0","0","0","172884","-172884","-172884","172884"],["0","0","0","0","14934","-14934","-14934","14934"],["0","0","0","0","771","-771","-771","771"],["0","0","0","0","18","-18","-18","18"]]},"deriv_order":2}],"step_multiplier":{"coeffs":[["0","-225","225"],["0","-240","240"],["0","-94","94"],["0","-16","16"],["0","-1","1"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","-4860","9720","-4860"],["0","-8532","17064","-8532"],["0","-6057","12114","-6057"],["0","-2229","4458","-2229"],["0","-449","898","-449"],["0","-47","94","-47"],["0","-2","4","-2"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","5670","-11340","5670"],["0","0","6849","-13698","6849"],["0","0","3258","-6516","3258"],["0","0","763","-1526","763"],["0","0","88","-176","88"],["0","0","4","-8","4"]]},"deriv_order":1}],[{"coeff":{"coeffs":[["0","0","-39690","79380","-39690"],["0","0","-59283","118566","-59283"],["0","0","-36504","73008","-36504"],["0","0","-11857","23714","-11857"],["0","0","-2142","4284","-2142"],["0","0","-204","408","-204"],["0","0","-8","16","-8"]]},"deriv_order":0}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["2"],["3"],["1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-3","-2"],["0","-2"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-1","1"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","-61236000","-301077000","785862000","-423549000"],["0","0","0","-137586600","-1565381700","3543523200","-1840554900"],["0","0","0","58869180","-3670603290","7164599040","-3552864930"],["0","0","0","556132662","-5159670651","8650943316","-4047405327"],["0","0","0","916529355","-4869566289","6989544513","-3036507579"],["0","0","0","846096381","-3271148157","4004007171","-1578955395"],["0","0","0","517806814","-1615853118","1678285794","-580239490"],["0","0","0","223843560","-597161922","522793164","-149474802"],["0","0","0","70252754","-166124826","121491390","-25619318"],["0","0","0","16131670","-34655394","20915778","-2392054"],["0","0","0","2688708","-5341254","2616384","36162"],["0","0","0","317066","-590211","229224","43921"],["0","0","0","25099","-44229","13161","5969"],["0","0","0","1197","-2013","435","381"],["0","0","0","26","-42","6","10"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","-178605000","178605000","178605000","-178605000"],["0","0","0","0","-798619500","798619500","798619500","-798619500"],["0","0","0","0","-1598352750","1598352750","1598352750","-1598352750"],["0","0","0","0","-1906360245","1906360245","1906360245","-1906360245"],["0","0","0","0","-1517464152","1517464152","1517464152","-1517464152"],["0","0","0","0","-853558860","853558860","853558860","-853558860"],["0","0","0","0","-349725936","349725936","349725936","-349725936"],["0","0","0","0","-105834402","105834402","105834402","-105834402"],["0","0","0","0","-23681532","23681532","23681532","-23681532"],["0","0","0","0","-3873036","3873036","3873036","-3873036"],["0","0","0","0","-450306","450306","450306","-450306"],["0","0","0","0","-35265","35265","35265","-35265"],["0","0","0","0","-1668","1668","1668","-1668"],["0","0","0","0","-36","36","36","-36"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["0","0","3375","-6750","3375"],["0","0","5400","-10800","5400"],["0","0","3555","-7110","3555"],["0","0","1232","-2464","1232"],["0","0","237","-474","237"],["0","0","24","-48","24"],["0","0","1","-2","1"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","56700","-113400","56700"],["0","0","133380","-266760","133380"],["0","0","134973","-269946","134973"],["0","0","76773","-153546","76773"],["0","0","26852","-53704","26852"],["0","0","5914","-11828","5914"],["0","0","801","-1602","801"],["0","0","61","-122","61"],["0","0","2","-4","2"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","-28350","18900","47250","-37800"],["0","0","-43065","9810","109575","-76320"],["0","0","-26874","-10794","102210","-64542"],["0","0","-8814","-12040","50522","-29668"],["0","0","-1602","-4808","14422","-8012"],["0","0","-153","-966","2391","-1272"],["0","0","-6","-98","214","-110"],["0","0","0","-4","8","-4"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","-9450","28350","-28350","9450"],["0","0","0","-14355","43065","-43065","14355"],["0","0","0","-8958","26874","-26874","8958"],["0","0","0","-2938","8814","-8814","2938"],["0","0","0","-534","1602","-1602","534"],["0","0","0","-51","153","-153","51"],["0","0","0","-2","6","-6","2"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","255150","-302400","-160650","207900"],["0","0","491535","-506610","-461385","476460"],["0","0","409221","-348981","-529701","469461"],["0","0","192219","-124451","-327755","259987"],["0","0","55694","-22820","-121442","88568"],["0","0","10189","-1364","-27839","19014"],["0","0","1149","215","-3877","2513"],["0","0","73","41","-301","187"],["0","0","2","2","-10","6"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","66150","-198450","198450","-66150"],["0","0","0","119385","-358155","358155","-119385"],["0","0","0","91416","-274248","274248","-91416"],["0","0","0","38482","-115446","115446","-38482"],["0","0","0","9614","-28842","28842","-9614"],["0","0","0","1425","-4275","4275","-1425"],["0","0","0","116","-348","348","-116"],["0","0","0","4","-12","12","-4"]]},"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+1, 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":1,"input":{"first_index":0,"initial_polynomials":[["1"],["1","1"]],"recurrence":{"denominator":{"coeffs":[["12"],["7"],["1"]]},"terms":[{"coeff":{"coeffs":[["12","0"],["9","12"],["-1","8"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","12","-12"],["0","9","-9"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","0","0"],["-2","-4","-2"],["2","4","2"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent":{"first_index":0,"initial_polynomials":[["2"],["3","2"]],"recurrence":{"denominator":{"coeffs":[["3"],["7"],["2"]]},"terms":[{"coeff":{"coeffs":[["6","0"],["8","8"],["4","4"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["3","-6","3"],["-1","2","-1"],["-2","4","-2"]]},"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+1, 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+1, 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":["3","4","1"],"method":{"kind":"taylor_shift","shifted_denominator":["3","4","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+1, k+1) x^k","kind":"preserver_image","operator":{"factor":{"terms":[{"coefficient_offset":1,"index_offset":1,"kind":"binomial"}]},"shape":"hadamard_multiplier"}},"parent":{"gauge":{"denominator":["3","4","1"],"kind":"closed","numerator":["1"]},"index_shift":1,"recurrence":{"first_index":0,"initial_polynomials":[["2"],["3","2"]],"recurrence":{"denominator":{"coeffs":[["3"],["7"],["2"]]},"terms":[{"coeff":{"coeffs":[["6","0"],["8","8"],["4","4"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["3","-6","3"],["-1","2","-1"],["-2","4","-2"]]},"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+1, 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) = 2 n^2 + 7 n + 3 != 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of f(n) = 2 n^2 + 7 n + 3 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":["25","15","2"]},"numerator":["3","7","2"],"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 = 8 n^2 + 16 n + 6 != 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of f(n) a_n = 8 n^2 + 16 n + 6 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":["70","48","8"]},"numerator":["6","16","8"],"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/25 (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^4 + 1/8 n^3 - 7/64 n^2 - 11/64 n + 3/32)/(n^4 + 2 n^3 + 1/2 n^2 - 1/2 n - 3/16) > 0 for every integer n in [3, +inf) (exact; Taylor shift: the coefficients of beta_n = (1/16 n^4 + 1/8 n^3 - 7/64 n^2 - 11/64 n + 3/32)/(n^4 + 2 n^3 + 1/2 n^2 - 1/2 n - 3/16) at n = 3 + u have one sign)","name":"recurrence_coefficient_positive","sign_decision":{"certificate":{"condition":"positive","denominator":["-3/16","-1/2","1/2","2","1"],"method":{"kind":"taylor_shift","shifted_denominator":["2205/16","329/2","145/2","14","1"],"shifted_numerator":["225/32","595/64","281/64","7/8","1/16"]},"numerator":["3/32","-11/64","-7/64","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 + 3/4)/(n + 3/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":["-27/64","-351/128","-333/64","77/32","351/16","259/8","89/4","15/2","1"],"method":{"kind":"taylor_shift","shifted_denominator":["6251175/128","13276305/128","6122277/64","1602077/32","260301/16","26899/8","1727/4","63/2","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^2 + 5/4 n + 3/2)/(n^2 + 5/2 n + 3/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":["-27/64","-459/128","-711/64","-1375/128","1379/64","2517/32","1743/16","675/8","153/4","19/2","1"],"method":{"kind":"taylor_shift","shifted_denominator":["6251175/8","32803785/16","308374479/128","213765665/128","48414773/64","7488429/32","801213/16","58563/8","2799/4","79/2","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 + 8 n + 3)/(n^2 + 7/2 n + 3/2), b_n = (2 n^2 + 4 n)/(n^2 + 7/2 n + 3/2), c_n = (n^2 + 1/2 n - 3/2)/(n^2 + 7/2 n + 3/2); 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":[["2"],["3","2"]],"recurrence":{"denominator":{"coeffs":[["3"],["7"],["2"]]},"terms":[{"coeff":{"coeffs":[["6","0"],["8","8"],["4","4"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["3","-6","3"],["-1","2","-1"],["-2","4","-2"]]},"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 + 8 n + 3)/(n^2 + 7/2 n + 3/2), b_n = (2 n^2 + 4 n)/(n^2 + 7/2 n + 3/2), c_n = (n^2 + 1/2 n - 3/2)/(n^2 + 7/2 n + 3/2); 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 + 8 n + 3)/(n^2 + 7/2 n + 3/2), b_n = (2 n^2 + 4 n)/(n^2 + 7/2 n + 3/2), c_n = (n^2 + 1/2 n - 3/2)/(n^2 + 7/2 n + 3/2); 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+1)) with T = x^k -> binom(n+1, 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"}