{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"coefficients":[{"denominator":["1"],"numerator":["0"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["4","7","2"],["5","16","11","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"Triangle of coefficients of polynomials u(n,x) jointly generated with A207607; see the Formula section."},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["64","-8","-24"],["24","-14","-14"],["2","-3","-2"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","24","-18","-6"],["0","4","-7","-2"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["-28","20"],["-18","18"],["-2","4"]]},"deriv_order":1,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["7","4"]],"recurrence":{"denominator":{"coeffs":[["-12","6"],["-14","10"],["-2","4"]]},"terms":[{"coeff":{"coeffs":[["-42","-3","12"],["-20","8","10"],["-2","3","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","-20","11","4"],["0","-4","7","2"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["1"],"operator":{"coefficients":[{"denominator":["1"],"numerator":["0"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["4","7","2"],["5","16","11","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_leader_shift":2,"parent_valid_from_base":0,"quotients":[],"row_annihilation":{"kind":"system","system":{"generators":[{"annihilator":{"terms":[{"coeff":{"coeffs":[["3","-42","24"],["8","-26","20"],["1","-4","4"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-6","13","2","-8"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-4","15","-12","-4"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["6"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","-7168","19456","-12928","-2560","2500","500"],["0","0","-8192","26240","-21344","-2504","4550","850"],["0","0","-3264","12576","-12780","-312","3090","540"],["0","0","-544","2512","-3250","302","928","152"],["0","0","-32","176","-290","76","104","16"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["0","0","0","-884736","2654208","-1824768","-774144","570240","259200","27000"],["0","0","0","-663552","2488320","-2239488","-642816","785376","320760","32400"],["0","0","0","-165888","746496","-870912","-129600","355752","132192","12960"],["0","0","0","-13824","72576","-106272","1512","53136","18144","1728"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","-3538944","20348928","-43573248","38209536","-3801600","-11428992","1818720","1776600","216000"],["0","0","0","-4128768","26689536","-63848448","63406080","-10881792","-18910656","4121568","3266280","385200"],["0","0","0","-1916928","13750272","-36615168","41121792","-10223424","-12190032","3557052","2383056","272880"],["0","0","0","-442368","3483648","-10264320","13003200","-4324752","-3798900","1480248","861840","95904"],["0","0","0","-50688","434304","-1406304","2000088","-850860","-565344","299232","154368","16704"],["0","0","0","-2304","21312","-75312","119484","-63000","-31392","23616","10944","1152"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","884736","-4571136","7280640","-1115136","-6394752","3151296","1756872","-615420","-336600","-36000"],["0","0","0","663552","-3926016","7409664","-2495232","-6242400","4152600","1781460","-870048","-416880","-43200"],["0","0","0","165888","-1105920","2433024","-1287360","-1922184","1756620","564840","-402192","-171936","-17280"],["0","0","0","13824","-102528","258912","-189144","-182052","239184","53280","-61056","-23616","-2304"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","589824","-3981312","9621504","-8764416","-435456","4017600","5616","-831060","-226800","-18000"],["0","0","0","0","442368","-3317760","9040896","-9704448","689472","4528224","-361908","-1084104","-278640","-21600"],["0","0","0","0","110592","-912384","2778624","-3473280","682992","1641060","-303264","-469152","-114048","-8640"],["0","0","0","0","9216","-82944","279936","-402624","132516","188568","-63072","-67392","-15552","-1152"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","1105920","-9086976","29021184","-43792128","27484128","1943064","-8370144","513792","1100160","144000"],["0","0","0","921600","-8303616","29509632","-50688000","38445552","-1637100","-11646576","1520064","1738944","216000"],["0","0","0","290304","-2848896","11147616","-21454488","19061316","-2765196","-5730624","1223136","994752","118080"],["0","0","0","41472","-438912","1867104","-3958200","4001616","-946944","-1178496","369792","241920","27648"],["0","0","0","2304","-25920","117936","-270108","301968","-94608","-86400","36288","20736","2304"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-221184","2451456","-10202112","19222272","-13202784","-5305176","8495928","1259280","-1827360","-630720","-57600"],["0","0","0","-110592","1281024","-5723136","11964672","-9999504","-2119932","6492960","325728","-1648512","-520128","-46080"],["0","0","0","-13824","167040","-795744","1826712","-1806732","-73224","1179360","-84672","-368064","-107136","-9216"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","-147456","1400832","-5225472","9262080","-6699456","-1049760","3139452","120096","-629856","-178560","-14400"],["0","0","0","0","-73728","755712","-3068928","6020352","-5086368","-183384","2390256","-91584","-549504","-146304","-11520"],["0","0","0","0","-9216","101376","-445824","962496","-937764","76464","440208","-58752","-119232","-29952","-2304"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["42","-30"],["41","-37"],["12","-15"],["1","-2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-24","-2","10"],["-6","1","4"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-16","16","5"],["0","-4","7","2"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","0","-5888","16448","-10832","-2468","1940","400"],["0","0","-4160","14912","-13268","-1370","2816","520"],["0","0","-928","4144","-5050","224","1336","224"],["0","0","-64","352","-580","152","208","32"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","1792","-9792","17616","-9724","-2412","1920","400"],["0","0","1600","-9408","18708","-12334","-1974","2688","520"],["0","0","416","-2736","6234","-5048","-288","1248","224"],["0","0","32","-240","642","-656","48","192","32"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["0","0","0","-884736","2654208","-1824768","-774144","570240","259200","27000"],["0","0","0","-663552","2488320","-2239488","-642816","785376","320760","32400"],["0","0","0","-165888","746496","-870912","-129600","355752","132192","12960"],["0","0","0","-13824","72576","-106272","1512","53136","18144","1728"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","-14155776","54853632","-66355200","13160448","19961856","-3836160","-3196800","-378000"],["0","0","0","-20643840","89948160","-123641856","34495488","37446912","-9863424","-6819840","-782100"],["0","0","0","-12386304","60272640","-93892608","34532352","28363392","-10133424","-6018408","-670140"],["0","0","0","-3907584","21113856","-37165824","17349696","11004048","-5377536","-2811384","-304272"],["0","0","0","-681984","4073472","-8080128","4673664","2271960","-1563840","-732960","-77184"],["0","0","0","-62208","409536","-913680","644436","230040","-237168","-101088","-10368"],["0","0","0","-2304","16704","-41904","35676","8352","-14688","-5760","-576"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","4423680","-13123584","6617088","10368000","-6979968","-3197376","1152360","600300","63000"],["0","0","0","4202496","-15132672","10911744","11632896","-10960992","-3914856","2013444","920340","93600"],["0","0","0","1492992","-6303744","6054912","4463424","-6174792","-1641060","1287900","525528","51840"],["0","0","0","235008","-1134720","1371744","661608","-1471860","-255348","358560","132336","12672"],["0","0","0","13824","-74880","109152","29160","-123732","-8280","36720","12384","1152"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","2949120","-12238848","15224832","-1317888","-6997248","418752","1568880","405900","31500"],["0","0","0","0","2801664","-13639680","20247552","-4267008","-9586368","1425888","2512332","616320","46800"],["0","0","0","0","995328","-5557248","9745920","-3390336","-4718736","1260036","1492992","348624","25920"],["0","0","0","0","156672","-986112","2012544","-1008576","-973980","428688","389952","86976","6336"],["0","0","0","0","9216","-64512","150912","-100800","-69084","50400","37728","8064","576"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","4644864","-29288448","62530560","-49856256","711648","14683608","-1340496","-1986480","-252000"],["0","0","0","5050368","-34477056","83865600","-80418816","9869040","23986548","-3931992","-3723192","-450000"],["0","0","0","2207232","-16295040","44166240","-49540824","11344212","14850036","-3794436","-2717280","-314640"],["0","0","0","483840","-3858048","11497824","-14695992","4890960","4336596","-1634040","-963216","-107424"],["0","0","0","52992","-455616","1481616","-2119572","913860","596736","-322848","-165312","-17856"],["0","0","0","2304","-21312","75312","-119484","63000","31392","-23616","-10944","-1152"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-1105920","9824256","-27767808","26198784","5592096","-15843672","-1598976","3441780","1127160","100800"],["0","0","0","-774144","7197696","-22625280","25777152","1265616","-16182900","-101340","4165056","1258704","109440"],["0","0","0","-179712","1742976","-5991264","8017560","-922068","-5200884","592632","1645776","462816","39168"],["0","0","0","-13824","139392","-516960","792792","-221148","-515520","148320","211968","55872","4608"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","-737280","5087232","-12635136","11999232","205632","-5527008","115020","1192428","319680","25200"],["0","0","0","0","-516096","3926016","-10893312","12019968","-1144800","-5622264","564084","1396872","354672","27360"],["0","0","0","0","-119808","995328","-3058560","3875904","-815508","-1829628","366336","536544","129600","9792"],["0","0","0","0","-9216","82944","-279936","402624","-132516","-188568","63072","67392","15552","1152"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["0","0","1536","-3072","576","960","150"],["0","0","768","-2112","720","804","120"],["0","0","96","-336","198","168","24"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-2","-1"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"shift":2}]},"statement":"w(n) E = sum_nu H_nu S^nu L' (with any remainder removed by row annihilators of the parent), where L' is the parent rule at P'_n = P_(n+0) (valid from base 0) and E the input rule gauged by lambda(n)/delta(n) and composed with (or conjugated through) T = phi(n, D) = (1) D; so the candidate rows satisfy the input rule at every base n >= 0 (the exceptional bases checked exactly), and agreement on the 1 identifying rows gives Q_n = lambda(n) T_n(P_(n+0)) for every n >= 0"},"method":"operator_division"},"status":"certified"},"input_first_index":0,"interlacing":{"from_index":1,"justification":"the parent theorem (ThreeTermRecurrence) proves P_(m-1) strictly interlacing P_m for every m >= 1; T = phi(n, D) = (1) D is independent of n and maps every real-rooted polynomial to a real-rooted polynomial or zero, so by the Hermite--Kakeya--Obreschkoff theorem (both directions) T(P_(m-1)) and T(P_m) have weakly interlacing zeros; the nonzero gauge does not move zeros, so Q_(n-1) and Q_n interlace weakly (orientation not determined) for every n >= 1","kind":"weak","orientation":"unordered","status":"claimed"},"lean_declarations":["RealRooted.splits_add_C_mul_derivative_all","RealRooted.splits_C_mul_add_derivative","Polynomial.Splits.derivative"],"lift_summary":{"hypotheses":[{"evidence":"the polynomial with ascending coefficients [0, 1] is fixed; exact check: real-rooted = true, coefficients of one sign = true","name":"derivative_polynomial_real_rooted","statement":"the polynomial in D is real-rooted 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"}},{"evidence":"delta(n) != 0 for every integer n in [0, +inf) (exact; Taylor shift: the coefficients of delta(n) at n = 0 + u have one sign)","name":"operator_coefficients_defined","sign_decision":{"certificate":{"condition":"nonzero","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1"]},"numerator":["1"],"range":{"first":"0","last":null}},"decision":"holds"},"statement":"the operator coefficients are finite at every n >= n0 (their denominators do not vanish)","status":{"kind":"verified"}}],"identity":{"method":"forward_division","status":"certified"},"input_first_index":0,"input_interlacing":{"interlacing":{"from_index":1,"justification":{"premises":["the parent theorem (ThreeTermRecurrence) proves P_(m-1) strictly interlacing P_m for every m >= 1; T = phi(n, D) = (1) D is independent of n and maps every real-rooted polynomial to a real-rooted polynomial or zero, so by the Hermite--Kakeya--Obreschkoff theorem (both directions) T(P_(m-1)) and T(P_m) have weakly interlacing zeros; the nonzero gauge does not move zeros, so Q_(n-1) and Q_n interlace weakly (orientation not determined) for every n >= 1"],"theorem":"Hermite--Kakeya--Obreschkoff theorem (N. Obreschkoff, Verteilung und Berechnung der Nullstellen reeller Polynome, 1963; see S. Fisk, Polynomials, Roots, and Interlacing, arXiv:math/0612833): real polynomials f, g have weakly interlacing zeros iff alpha f + beta g is real-rooted or zero for all real alpha, beta; a linear T independent of n that maps every real-rooted polynomial to a real-rooted polynomial or zero therefore maps interlacing pairs to pairs with weakly interlacing zeros (orientation not determined)"},"kind":"weak","orientation":"unordered"},"status":"proved"},"lean_replay":"not_attempted","operation":{"description":"phi(n, D) = (1) D","kind":"preserver_image","operator":{"coefficients":[{"denominator":["1"],"numerator":["0"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["4","7","2"],["5","16","11","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"relation":"Q_n = lambda(n) T_n(P_(n+0)) with T = phi(n, D) = (1) D, 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":"Laguerre's theorem on differential operators: if phi is a real polynomial with only real roots, then phi(D) maps every real-rooted polynomial to a real-rooted polynomial or zero (write phi(D) = C D^j prod (1 + c_i D); D preserves real-rootedness by Rolle's theorem and p + c p' is real-rooted for every real c by Rolle's theorem applied to e^(x/c) p; Polya--Schur 1914); when the coefficients of phi have one sign, coefficients of one sign stay of one sign; applied to phi(n, .) for each n"},"verdict":"proved"},"notes":["the division remainder is removed by row annihilators of the shifted parent"],"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 = 1 != 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of f(n) a_n = 1 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":["1"]},"numerator":["1"],"range":{"first":"2","last":null}},"decision":"holds"},"statement":"a_n != 0 for every n >= 2","status":{"kind":"verified"}},{"evidence":"Q_0 has degree 2, Q_1 degree 3; 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 (exact)","name":"first_coefficient_positive","statement":"beta_2 = c_2 L_0 / (a_2 L_1) > 0","status":{"kind":"verified"}},{"evidence":"beta_n = 1 > 0 for every integer n in [3, +inf) (exact; Taylor shift: the coefficients of beta_n = 1 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"]},"numerator":["1"],"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) = (n + 4)/(n + 3) (the exact ratio r_n): g(n) > 0 for n >= 2, r_2 >= g(2) exactly, and (t - alpha_n) - beta_n/g(n-1) - g(n) >= 0 for every integer n in [3, +inf) (exact; Taylor shift: the coefficients of (t - alpha_n) - beta_n/g(n-1) - g(n) at n = 3 + u have one sign)","name":"root_upper_bound","sign_decision":{"certificate":{"condition":"nonnegative","denominator":["3","1"],"method":{"kind":"taylor_shift","shifted_denominator":["6","1"],"shifted_numerator":[]},"numerator":[],"range":{"first":"3","last":null}},"decision":"holds"},"statement":"every root of P_n is < 0 for every n >= 0 (region (-inf, 0) for P)","status":{"kind":"verified"}}],"lean_replay":"not_attempted","normal_form":"P_n = (a_n x + b_n) P_(n-1) - c_n P_(n-2) for n >= 2, with a_n = 1, b_n = 2, c_n = 1","recurrence":{"first_index":0,"initial_polynomials":[["4","7","2"],["5","16","11","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-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":"P_n = (a_n x + b_n) P_(n-1) - c_n P_(n-2) for n >= 2, with a_n = 1, b_n = 2, c_n = 1: 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 x + b_n) P_(n-1) - c_n P_(n-2) for n >= 2, with a_n = 1, b_n = 2, c_n = 1","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 = phi(n, D) = (1) D 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"}
