{"certification":{"candidate":{"gauge":{"denominator":["1"],"kind":"closed","numerator":["3/2","1/2"]},"index_shift":2,"operator":{"factor":{"terms":[{"coefficient_offset":1,"index_offset":2,"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":2,"kind":"binomial"}]},"hadamard":{"conjugated_input_relation":{"terms":[{"coeff":{"coeffs":[["-432","-576","-432"],["-4212/5","-4656/5","-2412/5"],["-3366/5","-2936/5","-996/5"],["-1412/5","-904/5","-36"],["-328/5","-136/5","-12/5"],["-8","-8/5","0"],["-2/5","0","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","288","144","-432"],["0","2328/5","84/5","-2412/5"],["0","1468/5","-472/5","-996/5"],["0","452/5","-272/5","-36"],["0","68/5","-56/5","-12/5"],["0","4/5","-4/5","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0","-72","144","-72"],["0","0","-402/5","804/5","-402/5"],["0","0","-166/5","332/5","-166/5"],["0","0","-6","12","-6"],["0","0","-2/5","4/5","-2/5"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["-864","-10368/5"],["-5472/5","-2880"],["-510","-7944/5"],["-471/5","-2176/5"],["1/5","-296/5"],["11/5","-16/5"],["1/5","0"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-2304/5","432/5"],["0","-4512/5","-1224/5"],["0","-3168/5","-321"],["0","-1042/5","-674/5"],["0","-164/5","-121/5"],["0","-2","-8/5"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["0","0","1872/5","1872/5"],["0","0","1992/5","1992/5"],["0","0","789/5","789/5"],["0","0","138/5","138/5"],["0","0","9/5","9/5"]]},"deriv_order":2,"shift":1},{"coeff":{"coeffs":[["1008"],["7608/5"],["943"],["1534/5"],["276/5"],["26/5"],["1/5"]]},"deriv_order":0,"shift":2}]},"conjugation_x_shift":0,"exceptional_bases":[],"factor":{"terms":[{"coefficient_offset":1,"index_offset":2,"kind":"binomial"}]},"gauge":{"denominator":["1"],"kind":"closed","numerator":["3/2","1/2"]},"identifying_indices":[1,2],"input_leader_shift":2,"input_relation":{"terms":[{"coeff":{"coeffs":[["-6","-12","-6"],["-16/5","-32/5","-16/5"],["-2/5","-4/5","-2/5"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-6","-108/5"],["-3/5","-12"],["1/5","-8/5"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-39/5","39/5"],["0","-9/5","9/5"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["21/5"],["2"],["1/5"]]},"deriv_order":0,"shift":2}]},"input_valid_from_base":1,"multiplier":["870912","1406592","987552","393624","97412","15326","1497","83","2"],"parent":{"first_index":1,"initial_polynomials":[["5","20","15","2"],["6","40","60","24","2"]],"recurrence":{"denominator":{"coeffs":[["25"],["15"],["2"]]},"terms":[{"coeff":{"coeffs":[["38","32"],["24","24"],["4","4"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-7","14","-7"],["-9","18","-9"],["-2","4","-2"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_leader_shift":2,"parent_relation":{"terms":[{"coeff":{"coeffs":[["33","-66","33"],["17","-34","17"],["2","-4","2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-102","-96"],["-40","-40"],["-4","-4"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["63"],["23"],["2"]]},"deriv_order":0,"shift":2}]},"parent_valid_from_base":1,"quotients":[{"differentiations":[{"coeff":{"coeffs":[["0","0","13934592","-27869184","13934592"],["0","0","192264192/5","-384528384/5","192264192/5"],["0","0","48328704","-96657408","48328704"],["0","0","36580608","-73161216","36580608"],["0","0","92856864/5","-185713728/5","92856864/5"],["0","0","33310232/5","-66620464/5","33310232/5"],["0","0","8657452/5","-17314904/5","8657452/5"],["0","0","1642554/5","-3285108/5","1642554/5"],["0","0","45155","-90310","45155"],["0","0","21926/5","-43852/5","21926/5"],["0","0","1428/5","-2856/5","1428/5"],["0","0","56/5","-112/5","56/5"],["0","0","1/5","-2/5","1/5"]]},"deriv_order":0}],"shift":0}],"row_annihilator_system":{"generators":[{"annihilator":{"terms":[{"coeff":{"coeffs":[["-30","-42"],["-11","-23"],["-1","-3"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","-9","9"],["0","-2","2"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["24"],["10"],["1"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","27869184","-376233984/5","334430208/5","-97542144/5"],["0","0","84685824","-1051232256/5","832177152/5","-204374016/5"],["0","0","585805824/5","-1342614528/5","927811584/5","-34200576"],["0","0","487836288/5","-1036631808/5","609754752/5","-60959232/5"],["0","0","272304384/5","-538952544/5","260991936/5","5656224/5"],["0","0","107312996/5","-198780776/5","75622564/5","15845216/5"],["0","0","30611044/5","-10665744","14824308/5","7893368/5"],["0","0","6366953/5","-10484066/5","1867273/5","449968"],["0","0","191638","-1498664/5","122758/5","417716/5"],["0","0","101734/5","-151868/5","-1466/5","10320"],["0","0","7232/5","-10352/5","-992/5","4112/5"],["0","0","309/5","-426/5","-15","192/5"],["0","0","6/5","-8/5","-2/5","4/5"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-83607552/5","36578304","-114960384/5","15676416/5"],["0","0","0","-263927808/5","100445184","-212668416/5","-25629696/5"],["0","0","0","-360751104/5","619325568/5","-156397824/5","-20435328"],["0","0","0","-285619968/5","453077568/5","-49295232/5","-118162368/5"],["0","0","0","-29338176","218616852/5","2838936/5","-74764908/5"],["0","0","0","-51571896/5","73087896/5","8539896/5","-30055896/5"],["0","0","0","-12707168/5","17281677/5","711630","-8132659/5"],["0","0","0","-2199502/5","2890803/5","163380","-1508201/5"],["0","0","0","-262538/5","335313/5","116988/5","-189763/5"],["0","0","0","-20606/5","25689/5","2088","-15523/5"],["0","0","0","-958/5","234","534/5","-746/5"],["0","0","0","-4","24/5","12/5","-16/5"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","67931136/5","-67931136/5","-67931136/5","67931136/5"],["0","0","0","0","153695232/5","-153695232/5","-153695232/5","153695232/5"],["0","0","0","0","31107456","-31107456","-31107456","31107456"],["0","0","0","0","92707776/5","-92707776/5","-92707776/5","92707776/5"],["0","0","0","0","36040236/5","-36040236/5","-36040236/5","36040236/5"],["0","0","0","0","1909464","-1909464","-1909464","1909464"],["0","0","0","0","1745187/5","-1745187/5","-1745187/5","1745187/5"],["0","0","0","0","217329/5","-217329/5","-217329/5","217329/5"],["0","0","0","0","17643/5","-17643/5","-17643/5","17643/5"],["0","0","0","0","843/5","-843/5","-843/5","843/5"],["0","0","0","0","18/5","-18/5","-18/5","18/5"]]},"deriv_order":2}],"step_multiplier":{"coeffs":[["0","-576","576"],["0","-480","480"],["0","-148","148"],["0","-20","20"],["0","-1","1"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","-22176","44352","-22176"],["0","-29376","58752","-29376"],["0","-15938","31876","-15938"],["0","-4535","9070","-4535"],["0","-714","1428","-714"],["0","-59","118","-59"],["0","-2","4","-2"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","16632","-33264","16632"],["0","0","16026","-32052","16026"],["0","0","6115","-12230","6115"],["0","0","1155","-2310","1155"],["0","0","108","-216","108"],["0","0","4","-8","4"]]},"deriv_order":1}],[{"coeff":{"coeffs":[["0","0","-149688","299376","-149688"],["0","0","-177498","354996","-177498"],["0","0","-87087","174174","-87087"],["0","0","-22625","45250","-22625"],["0","0","-3282","6564","-3282"],["0","0","-252","504","-252"],["0","0","-8","16","-8"]]},"deriv_order":0}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["6"],["5"],["1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-3","-4"],["0","-2"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-1","1"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","250822656/5","-1771435008/5","2790402048/5","-1269789696/5"],["0","0","0","1079184384/5","-5135394816/5","1406647296","-2977026048/5"],["0","0","0","1829910528/5","-1352951424","8039782656/5","-3104936064/5"],["0","0","0","1735454592/5","-5356366272/5","5506368768/5","-1885457088/5"],["0","0","0","1055661696/5","-2840267412/5","2513549736/5","-145788804"],["0","0","0","440429868/5","-1062842436/5","804395268/5","-36396540"],["0","0","0","130348772/5","-287859729/5","184673142/5","-5432437"],["0","0","0","5544735","-56865198/5","30559371/5","-1417848/5"],["0","0","0","4220832/5","-8132793/5","720618","308871/5"],["0","0","0","449728/5","-821313/5","293442/5","78143/5"],["0","0","0","6378","-55596/5","15522/5","8184/5"],["0","0","0","1353/5","-453","471/5","441/5"],["0","0","0","26/5","-42/5","6/5","2"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","-611380224/5","611380224/5","611380224/5","-611380224/5"],["0","0","0","0","-303823872","303823872","303823872","-303823872"],["0","0","0","0","-1707225984/5","1707225984/5","1707225984/5","-1707225984/5"],["0","0","0","0","-1145444544/5","1145444544/5","1145444544/5","-1145444544/5"],["0","0","0","0","-509777676/5","509777676/5","509777676/5","-509777676/5"],["0","0","0","0","-158006352/5","158006352/5","158006352/5","-158006352/5"],["0","0","0","0","-34801323/5","34801323/5","34801323/5","-34801323/5"],["0","0","0","0","-1089267","1089267","1089267","-1089267"],["0","0","0","0","-118689","118689","118689","-118689"],["0","0","0","0","-42873/5","42873/5","42873/5","-42873/5"],["0","0","0","0","-1848/5","1848/5","1848/5","-1848/5"],["0","0","0","0","-36/5","36/5","36/5","-36/5"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["0","0","13824","-27648","13824"],["0","0","17280","-34560","17280"],["0","0","8928","-17856","8928"],["0","0","2440","-4880","2440"],["0","0","372","-744","372"],["0","0","30","-60","30"],["0","0","1","-2","1"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","435456","-870912","435456"],["0","0","775872","-1551744","775872"],["0","0","598896","-1197792","598896"],["0","0","261588","-523176","261588"],["0","0","70712","-141424","70712"],["0","0","12113","-24226","12113"],["0","0","1284","-2568","1284"],["0","0","77","-154","77"],["0","0","2","-4","2"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","-108864","0","326592","-217728"],["0","0","-130464","-72576","536544","-333504"],["0","0","-64548","-86976","367596","-216072"],["0","0","-16872","-43032","136680","-76776"],["0","0","-2457","-11248","29867","-16162"],["0","0","-189","-1638","3843","-2016"],["0","0","-6","-126","270","-138"],["0","0","0","-4","8","-4"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","-36288","108864","-108864","36288"],["0","0","0","-43488","130464","-130464","43488"],["0","0","0","-21516","64548","-64548","21516"],["0","0","0","-5624","16872","-16872","5624"],["0","0","0","-819","2457","-2457","819"],["0","0","0","-63","189","-189","63"],["0","0","0","-2","6","-6","2"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","1415232","-1306368","-1632960","1524096"],["0","0","2167776","-1674432","-3154464","2661120"],["0","0","1440756","-868752","-2584764","2012760"],["0","0","542532","-223524","-1180548","861540"],["0","0","126569","-24840","-330027","228298"],["0","0","18728","899","-57982","38355"],["0","0","1716","558","-6264","3990"],["0","0","89","57","-381","235"],["0","0","2","2","-10","6"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","326592","-979776","979776","-326592"],["0","0","0","463968","-1391904","1391904","-463968"],["0","0","0","280620","-841860","841860","-280620"],["0","0","0","93648","-280944","280944","-93648"],["0","0","0","18619","-55857","55857","-18619"],["0","0","0","2205","-6615","6615","-2205"],["0","0","0","144","-432","432","-144"],["0","0","0","4","-12","12","-4"]]},"deriv_order":1}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["0","0","1","-2","1"]]},"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+2, k+1); so the candidate rows satisfy the input rule at every base n >= 1 (the exceptional bases checked exactly), and agreement on the 2 identifying rows gives Q_n = lambda(n) sum_k u(n,k) [x^k]P_n x^k for every n >= 1"},"index_shift":2,"input":{"first_index":1,"initial_polynomials":[["30","120","30"],["60","600","600","60"]],"recurrence":{"denominator":{"coeffs":[["1"],["6/5"],["1/5"]]},"terms":[{"coeff":{"coeffs":[["4","4"],["7/5","28/5"],["-1/5","8/5"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","21/5","-21/5"],["0","9/5","-9/5"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["6/5","12/5","6/5"],["8/5","16/5","8/5"],["2/5","4/5","2/5"]]},"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":1,"interlacing":{"reason":"the factor depends on n","status":"none"},"lift_summary":{"hypotheses":[{"evidence":"binom(n+2, k+1) is defined for every n >= 1","name":"factor_defined","statement":"the factor u(n, k) is defined on the index domain","status":{"kind":"verified"}},{"evidence":"binom(n+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 [1, +inf) (exact; Taylor shift: the coefficients of lambda(n) = numerator(n) / denominator(n) at n = 1 + u have one sign)","name":"gauge_finite_nonzero","sign_decision":{"certificate":{"condition":"nonzero","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["2","1/2"]},"numerator":["3/2","1/2"],"range":{"first":"1","last":null}},"decision":"holds"},"statement":"lambda(n) is finite and nonzero for every n >= n0","status":{"kind":"verified"}}],"identity":{"method":"hadamard_conjugation","status":"certified"},"input_first_index":1,"input_interlacing":{"reason":"the factor depends on n","status":"not_proved"},"lean_replay":"not_attempted","operation":{"description":"x^k -> binom(n+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":["1"],"kind":"closed","numerator":["3/2","1/2"]},"index_shift":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"},"relation":"Q_n = lambda(n) T_n(P_(n+2)) with T = x^k -> binom(n+2, k+1) x^k, for every n >= 1"},"parent_proof":{"route":"three_term_recurrence","statement":"every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign","status":"proved"},"root_transfer":{"input_conclusion":"every Q_n, n >= 1, is zero or real-rooted with roots in (-inf, 0]","input_root_region":{"upper":{"closed":true,"value":"0"}},"parent_hypothesis":"every parent row used is zero or real-rooted with all roots in (-inf, 0] (coefficients of one sign)","parent_root_region":{"upper":{"closed":true,"value":"0"}},"theorem":"Polya--Schur characterization of multiplier sequences (G. Polya and I. Schur, J. Reine Angew. Math. 144 (1914) 89--113; stated as Theorem 40 of P. Branden, Unimodality, log-concavity, real-rootedness and beyond, arXiv:1410.6601): a real sequence (lambda_k) is a multiplier sequence (x^k -> lambda_k x^k maps real-rooted polynomials to real-rooted polynomials or zero) iff sum_k binom(m,k) lambda_k x^k is real-rooted with zeros of one sign for every m, iff sum_k lambda_k x^k / k! (or its reflection) is C x^m e^(a x) prod (1 + alpha_j x) with a, alpha_j >= 0; a product of multiplier sequences is one (composition), and a nonzero factor lambda(n) of the row changes nothing"},"verdict":"proved"},"notes":[],"parent_interlacing_report":{"conclusion":{"first_index":0,"interlacing":"strict","interlacing_from":1,"root_region":{"upper":{"closed":false,"value":"0"}},"simple_roots":true,"statement":"every P_n, n >= 0, is nonzero and real-rooted, with simple roots from n = 0 on; P_(n-1) strictly interlaces P_n for n >= 1; every root lies in (-inf, 0)"},"hypotheses":[{"evidence":"f(n) = 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+2)) with T = x^k -> binom(n+2, k+1) x^k for every n >= 1, the side conditions hold for every n, and every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign; so every Q_n, n >= 1, is zero or real-rooted with roots in (-inf, 0]"},"kind":"preserver_image"}