{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"schedule":{"first_degree":0,"first_index":0,"step":1},"shape":"reversal"},"parent":{"first_index":0,"initial_polynomials":[["1"],["1","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","2"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"Triangular array:  row n gives the coefficients of the polynomial p(n,x) defined in Comments."},"identifying_rows":2,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["0"],["-6"],["-4"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["1","-6","-8"],["1","12","4"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-1","-12","-4"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["0"],["2"]]},"deriv_order":0,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0,1],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["1"],["4","1"]],"recurrence":{"denominator":{"coeffs":[["-2"],["2"]]},"terms":[{"coeff":{"coeffs":[["-4","4","2"],["4","-8","-2"],["0","4","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","4","30","4"],["0","-4","-12","-1"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","0","4","12","1"]]},"deriv_order":2,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":1,"multiplier":["1"],"operator":{"schedule":{"first_degree":0,"first_index":0,"step":1},"shape":"reversal"},"parent":{"first_index":0,"initial_polynomials":[["1"],["1","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","2"]]},"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":[["-4","-16"],["4","-24"],["4","-8"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-1","10","20","-8"],["-1","-10","20","8"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","1","10","-20","-8"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["4"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","0"],["0","-4","-48","-16","0"],["0","-2","-20","40","16"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["0","0","0","-512","-18432","-227328","-1032192","-909312","-294912","-32768","0","0","0"],["0","0","0","-768","-26112","-285696","-866304","1732608","2285568","835584","98304","0","0"],["0","0","0","-384","-12288","-116736","-147456","1732608","-589824","-1867776","-786432","-98304","0"],["0","0","0","-64","-1920","-15360","14336","337920","-675840","-114688","491520","245760","32768"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","-1024","-31744","-270336","208896","8503296","8503296","2883584","327680","0","0","0"],["0","0","0","-3072","-94720","-807936","301056","19722240","-4546560","-18333696","-7831552","-983040","0","0"],["0","0","0","-3584","-108800","-897024","552960","19955712","-27451392","-17629184","9109504","6684672","983040","0"],["0","0","0","-2048","-60800","-472320","612352","10670080","-25006080","3088384","16875520","2949120","-1409024","-327680"],["0","0","0","-576","-16640","-119040","282624","2897920","-9461760","5726208","5570560","-2703360","-2162688","-327680"],["0","0","0","-64","-1792","-11520","45056","309248","-1351680","1236992","720896","-737280","-458752","-65536"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","256","9216","108544","331776","-1818624","-10174464","-9076736","-2949120","-327680","0","0","0","0"],["0","0","0","512","18944","235520","905216","-2088960","-13074432","11042816","19595264","7602176","917504","0","0","0"],["0","0","0","384","14592","187392","749568","-1781760","-10985472","19267584","7274496","-10125312","-5701632","-786432","0","0"],["0","0","0","128","4992","65024","240128","-995328","-4673536","13746176","-1622016","-9797632","-2523136","393216","131072","0"],["0","0","0","16","640","8320","25088","-200960","-634880","3436544","-2539520","-3215360","1605632","2129920","655360","65536"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","-128","-5888","-100352","-733184","-1634304","3268608","5865472","3211264","753664","65536","0","0","0"],["0","0","0","0","-192","-8448","-132864","-798720","-251904","9805824","-1007616","-12779520","-8503296","-2162688","-196608","0","0"],["0","0","0","0","-96","-4032","-57984","-266496","672768","5154816","-10309632","-5382144","8527872","7421952","2064384","196608","0"],["0","0","0","0","-16","-640","-8320","-25088","200960","634880","-3436544","2539520","3215360","-1605632","-2129920","-655360","-65536"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","-512","-16128","-147456","-118784","2408448","-1941504","-2097152","196608","393216","65536","0"],["0","0","0","-1280","-38784","-319744","161792","6533120","-11882496","-1728512","7569408","2883584","32768","-65536"],["0","0","0","-1152","-33792","-253440","442368","5910528","-16220160","6045696","10223616","-1474560","-2359296","-393216"],["0","0","0","-448","-12800","-88320","253952","2222080","-8110080","5955584","4587520","-3194880","-2228224","-327680"],["0","0","0","-64","-1792","-11520","45056","309248","-1351680","1236992","720896","-737280","-458752","-65536"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","128","4480","50944","157696","-507904","-1634304","2367488","1736704","-425984","-425984","-65536","0","0"],["0","0","0","192","6976","83456","277760","-1005568","-3971072","9240576","925696","-5324800","-1687552","131072","65536","0"],["0","0","0","96","3648","45696","151296","-771072","-2955264","10309632","-3416064","-6955008","-49152","1081344","196608","0"],["0","0","0","16","640","8320","25088","-200960","-634880","3436544","-2539520","-3215360","1605632","2129920","655360","65536"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","-64","-2816","-44288","-266240","-83968","3268608","-335872","-4259840","-2834432","-720896","-65536","0","0"],["0","0","0","0","-64","-2688","-38656","-177664","448512","3436544","-6873088","-3588096","5685248","4947968","1376256","131072","0"],["0","0","0","0","-16","-640","-8320","-25088","200960","634880","-3436544","2539520","3215360","-1605632","-2129920","-655360","-65536"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0"],["-8","16"],["-12","24"],["-4","8"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["2","-12","-16","0"],["3","14","-12","8"],["1","10","-20","-8"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-2","-24","-8","0"],["0","-1","-10","20","8"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","-4","-48","-16","0"],["0","-2","-20","40","16"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["0","0","0","-512","-18432","-227328","-1032192","-909312","-294912","-32768","0","0","0"],["0","0","0","-768","-26112","-285696","-866304","1732608","2285568","835584","98304","0","0"],["0","0","0","-384","-12288","-116736","-147456","1732608","-589824","-1867776","-786432","-98304","0"],["0","0","0","-64","-1920","-15360","14336","337920","-675840","-114688","491520","245760","32768"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","3072","104448","1142784","3465216","-6930432","-9142272","-3342336","-393216","0","0","0"],["0","0","0","10240","338944","3495936","8122368","-33497088","-9682944","16285696","8716288","1179648","0","0"],["0","0","0","13824","443904","4263936","6193152","-57212928","28164096","41877504","-786432","-6684672","-1179648","0"],["0","0","0","9728","302336","2674176","1130496","-46104576","58269696","22003712","-27394048","-10616832","589824","393216"],["0","0","0","3776","113408","913152","-716800","-19032064","40378368","-5742592","-24051712","-540672","3866624","720896"],["0","0","0","768","22272","161280","-356352","-3883008","12165120","-6733824","-7274496","2949120","2555904","393216"],["0","0","0","64","1792","11520","-45056","-309248","1351680","-1236992","-720896","737280","458752","65536"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-768","-29184","-390144","-2009088","-1732608","9216000","9977856","3440640","393216","0","0","0","0"],["0","0","0","-1792","-68864","-931840","-4825088","-3489792","24797184","-1343488","-19398656","-8716288","-1114112","0","0","0"],["0","0","0","-1664","-64640","-876800","-4327424","491520","38768640","-19816448","-22446080","6062080","6258688","983040","0","0"],["0","0","0","-768","-30144","-406272","-1816320","2936832","25774080","-36839424","-16932864","13369344","5849088","-196608","-196608","0"],["0","0","0","-176","-6976","-92672","-354048","1420544","7026688","-20619264","2367488","15855616","3391488","-1835008","-720896","-65536"],["0","0","0","-16","-640","-8320","-25088","200960","634880","-3436544","2539520","3215360","-1605632","-2129920","-655360","-65536"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","384","18176","325632","2650112","8736768","4399104","-2260992","-2424832","-688128","-65536","0","0","0"],["0","0","0","0","704","32000","534272","3731456","6789120","-22880256","-22454272","-65536","5488640","1900544","196608","0","0"],["0","0","0","0","480","20928","323712","1863936","-168960","-24766464","12324864","30941184","8478720","-3096576","-1671168","-196608","0"],["0","0","0","0","144","6016","85632","380416","-1097984","-7507968","17182720","4636672","-14585856","-8290304","-622592","393216","65536"],["0","0","0","0","16","640","8320","25088","-200960","-634880","3436544","-2539520","-3215360","1605632","2129920","655360","65536"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","1536","52992","604160","2256896","319488","6660096","5799936","983040","-262144","-65536","0"],["0","0","0","4352","141696","1416448","2949120","-12615680","16773120","5611520","-10027008","-4653056","-294912","65536"],["0","0","0","4736","146944","1298432","622592","-20992000","33472512","-2523136","-21757952","-2719744","2490368","524288"],["0","0","0","2496","74368","585728","-616448","-12441600","29847552","-10174464","-16941056","4308992","4882432","786432"],["0","0","0","640","18432","130560","-327680","-3207168","10813440","-6963200","-6291456","3440640","2621440","393216"],["0","0","0","64","1792","11520","-45056","-309248","1351680","-1236992","-720896","737280","458752","65536"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-384","-14208","-184064","-940032","-1507328","-2396160","-8626176","-5996544","-819200","294912","65536","0","0"],["0","0","0","-704","-26432","-342528","-1584384","161792","10508288","-7208960","2940928","10567680","3784704","131072","-65536","0"],["0","0","0","-480","-18368","-238720","-989440","2020352","13772800","-23040000","-4530176","8560640","81920","-1736704","-327680","0"],["0","0","0","-144","-5632","-73344","-265216","1196288","5308416","-17182720","4161536","13012992","917504","-2523136","-786432","-65536"],["0","0","0","-16","-640","-8320","-25088","200960","634880","-3436544","2539520","3215360","-1605632","-2129920","-655360","-65536"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","192","8704","144640","999424","1718272","-6537216","-5529600","1048576","2080768","655360","65536","0","0"],["0","0","0","0","256","11136","171520","976384","-196608","-13242368","7880704","16367616","2818048","-2785280","-1179648","-131072","0"],["0","0","0","0","112","4672","66304","291584","-873728","-5789696","13746176","2842624","-11743232","-5816320","65536","458752","65536"],["0","0","0","0","16","640","8320","25088","-200960","-634880","3436544","-2539520","-3215360","1605632","2129920","655360","65536"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["0","-8","-96","-32","0"],["0","-4","-40","80","32"]]},"start_base":1}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["0","-2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-1","-2"]]},"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 = x^(d_n) P(1/x), d_n = 0 + 1 (n - 0); 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) T_n(P_(n+0)) for every n >= 0"},"method":"operator_division"},"status":"certified"},"input_first_index":0,"interlacing":{"reason":"the schedule d_n depends on n","status":"none"},"lean_declarations":["RealRooted.X_pow_mul_reverse_eq_zero_or_splits","RealRooted.reflect_eq_zero_or_splits"],"lean_route":"reversed","lift_summary":{"hypotheses":[{"evidence":"lambda(n) = 1","name":"gauge_finite_nonzero","statement":"lambda(n) is finite and nonzero for every n >= n0","status":{"kind":"verified"}}],"identity":{"method":"forward_division","status":"certified"},"input_first_index":0,"input_interlacing":{"reason":"the schedule d_n depends on n","status":"not_proved"},"lean_replay":"not_attempted","operation":{"description":"x^(d_n) P(1/x), d_n = 0 + 1 (n - 0)","kind":"preserver_image","operator":{"schedule":{"first_degree":0,"first_index":0,"step":1},"shape":"reversal"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["1","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","2"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"relation":"Q_n = lambda(n) T_n(P_(n+0)) with T = x^(d_n) P(1/x), d_n = 0 + 1 (n - 0), for every n >= 0"},"parent_proof":{"route":"liu_wang_derivative_lag","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":"a real affine substitution x -> a x + b (a != 0), the reversal x^d p(1/x) (d >= deg p) and a real Mobius map (c x + e)^d p((a x + b)/(c x + e)) (a e - b c != 0, d >= deg p) map real roots to real roots: a root r of p gives the root (r - b)/a, 1/r (and 0) or (e r - b)/(a - c r) (and -e/c); for an input row that is a polynomial the degree condition holds automatically"},"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 every root in (-inf, 0) (so its coefficients have one sign); for n >= 1, P_n has simple roots and P_(n-1) strictly interlaces P_n (no common root), and deg P_n = deg P_(n-1) + 1 for n >= 2"},"hypotheses":[{"evidence":"checked exactly","name":"seed_roots_negative","statement":"P_0 and P_1 are nonzero and real-rooted with every root < 0","status":{"kind":"verified"}},{"evidence":"degrees 0 and 1, leading coefficients of one sign","name":"seed_degree_step","statement":"deg P_1 = deg P_0 + 1, with leading coefficients of one sign","status":{"kind":"verified"}},{"evidence":"Bezout test, exact","name":"seed_strict_interlacing","statement":"P_0 strictly interlaces P_1 (simple real roots, no common root)","status":{"kind":"verified"}},{"evidence":"lambda_n = 2 > 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of lambda_n = 2 at n = 2 + u have one sign)","name":"degree_step_positive","sign_decision":{"certificate":{"condition":"positive","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["2"]},"numerator":["2"],"range":{"first":"2","last":null}},"decision":"holds"},"statement":"lambda_n = [x^1] A_n + (deg P_(n-1)) [x^2] V_n > 0 for every n >= 2 (deg P_n = deg P_(n-1) + 1 with leading coefficients of one sign)","status":{"kind":"verified"}},{"evidence":"[x^0] c_1 and [x^0] c_2 are zero polynomials","name":"multipliers_vanish_at_zero","statement":"V_n(0) = 0 and W_n(0) = 0 for every n >= 2","status":{"kind":"verified"}},{"evidence":"A_n(0) = 1 > 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of A_n(0) = 1 at n = 2 + u have one sign)","name":"constant_term_positive","sign_decision":{"certificate":{"condition":"positive","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) > 0 for every n >= 2","status":{"kind":"verified"}},{"evidence":"V_n = 0","name":"derivative_coefficient_nonpositive","statement":"V_n(x) <= 0 for every x < 0 and every n >= 2","status":{"kind":"verified"}},{"evidence":"W_n(x) = gamma(n) w(x) / f(n) with w(x) = 2 x, which is negative on (-inf, 0) (no root there, exact): gamma(n)/f(n) = 1 >= 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of gamma(n)/f(n) = 1 at n = 2 + u have one sign)","name":"lag_coefficient_nonpositive","sign_decision":{"certificate":{"condition":"nonnegative","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1"]},"numerator":["1"],"range":{"first":"2","last":null}},"decision":"holds"},"statement":"W_n(x) <= 0 for every x < 0 and every n >= 2","status":{"kind":"verified"}},{"evidence":"W_n(x) = gamma(n) w(x) / f(n) with w(x) = 2 x, which is negative on (-inf, 0) (no root there, exact): gamma(n)/f(n) = 1 > 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of gamma(n)/f(n) = 1 at n = 2 + u have one sign)","name":"derivative_or_lag_coefficient_negative","sign_decision":{"certificate":{"condition":"positive","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1"]},"numerator":["1"],"range":{"first":"2","last":null}},"decision":"holds"},"statement":"for every n >= 2 and x < 0, V_n(x) < 0 or W_n(x) < 0 (V_n < 0 on (-inf, 0) for every n, or W_n < 0 there for every n)","status":{"kind":"verified"}}],"lean_declarations":["RealRooted.threeTerm_interlaces_of_nonnegCoeffs","RealRooted.LiuWang.strictInterl_nonpos_lag_sequence"],"lean_replay":"not_attempted","lean_route":"sign","normal_form":"P_n = A_n(x) P_(n-1) + V_n(x) P'_(n-1) + W_n(x) P_(n-2) for n >= 2, with A_n(x) = (1) + (2) x, V_n(x) = 0, W_n(x) = (2) x","recurrence":{"first_index":0,"initial_polynomials":[["1"],["1","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","2"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"reference":"L. L. Liu and Y. Wang, A unified approach to polynomial sequences with only real zeros, Adv. in Appl. Math. 38 (2007) 542-560, Theorem 2.1 with the interlacers f' and the lag row (strict form, as in the derivative-lag theorems of the RealRooted library, https://github.com/PerAlexandersson/RealRooted), with nonnegativity of the coefficients replaced by an exact induction keeping every root in (-inf, 0)","schema":"polytool.recurrence-real-rootedness-theorem.v1","status":"proved","theorem":"liu_wang_derivative_lag"},"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: support must satisfy offset = 1 + ell * t_degree; fixed_delay_predecessor_window: more than one weighted lag)","route":"paper_theorem","success":false,"variant":"match_recurrence_theorems"},{"detail":"not applicable: c_2(n, x) = gamma(n) w(x) with w neither constant nor a constant times a square (x + v_0)^2","route":"three_term_recurrence","success":false,"variant":"three_term_recurrence"},{"detail":"not applicable: the rule is not f(n) P_n = c_0(n, x) P_(n-1) + c_1(n, x) P'_(n-1)","route":"liu_wang","success":false,"variant":"liu_wang"},{"detail":"P_n = A_n(x) P_(n-1) + V_n(x) P'_(n-1) + W_n(x) P_(n-2) for n >= 2, with A_n(x) = (1) + (2) x, V_n(x) = 0, W_n(x) = (2) x: every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0) (so its coefficients have one sign); for n >= 1, P_n has simple roots and P_(n-1) strictly interlaces P_n (no common root), and deg P_n = deg P_(n-1) + 1 for n >= 2","route":"liu_wang_derivative_lag","success":true,"variant":"liu_wang_derivative_lag"}],"conditional_on":[],"interlacing":{"from_index":1,"justification":{"premises":["every hypothesis of the theorem is verified exactly for every index: P_n = A_n(x) P_(n-1) + V_n(x) P'_(n-1) + W_n(x) P_(n-2) for n >= 2, with A_n(x) = (1) + (2) x, V_n(x) = 0, W_n(x) = (2) x","every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0) (so its coefficients have one sign); for n >= 1, P_n has simple roots and P_(n-1) strictly interlaces P_n (no common root), and deg P_n = deg P_(n-1) + 1 for n >= 2"],"theorem":"liu_wang_derivative_lag: L. L. Liu and Y. Wang, A unified approach to polynomial sequences with only real zeros, Adv. in Appl. Math. 38 (2007) 542-560, Theorem 2.1 with the interlacers f' and the lag row (strict form, as in the derivative-lag theorems of the RealRooted library, https://github.com/PerAlexandersson/RealRooted), with nonnegativity of the coefficients replaced by an exact induction keeping every root in (-inf, 0)"},"kind":"strict","orientation":"previous_interlaces_next"},"route":"liu_wang_derivative_lag","rows_checked":10,"statement":"every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign","status":"proved"},"rows_compared":16,"schema":"polytool.recurrence-preserver-image.v1","statement":"proved: Q_n = lambda(n) T_n(P_(n+0)) with T = x^(d_n) P(1/x), d_n = 0 + 1 (n - 0) 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"}