{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"euler_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["3","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"basis_map_A013609 of A Riordan array of coordination sequences."},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["-12","-70","-141","-104","-4","16"],["8","14","-44","-104","-42","8"],["0","12","24","-6","-18","0"],["0","0","4","6","0","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-8","-68","-210","-273","-100","60","32"],["0","-8","-74","-204","-196","-30","16"],["0","0","4","-8","-42","-26","0"],["0","0","0","4","6","0","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-4","-28","-70","-66","2","32","8"],["0","0","-8","-44","-80","-46","6","4"],["0","0","0","-4","-16","-18","-4","0"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["4","18","23","4","-4"],["0","10","26","12","-6"],["0","0","8","10","-2"],["0","0","0","2","0"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","4","18","23","4","-4"],["0","0","10","26","12","-6"],["0","0","0","8","10","-2"],["0","0","0","0","2","0"]]},"deriv_order":1,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"denominator":{"coeffs":[["4","8","5","0","0"],["0","10","10","-2","-2"],["0","0","8","4","-2"],["0","0","0","2","0"]]},"terms":[{"coeff":{"coeffs":[["20","72","77","12","-20","-8"],["-8","10","80","74","6","-8"],["0","-12","-12","24","18","0"],["0","0","-4","-6","0","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["4","20","30","2","-30","-22","-4"],["0","8","36","48","10","-14","-4"],["0","0","4","16","18","4","0"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["1"],"operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"euler_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["3","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":1,"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","-2","0"],["2","-2","-4"],["0","2","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-2","2","14","6"],["0","-4","-8","-2"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","2","8","9","2"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["16","264","1932","8232","22512","40986","49655","38412","16644","1984","-1392","-576","-64"],["0","72","1048","6672","24288","55370","81094","74594","38998","7488","-2384","-1312","-160"],["0","0","128","1632","8948","27424","50980","57968","37917","11228","-592","-1008","-144"],["0","0","0","112","1240","5776","14592","21388","17838","7408","778","-280","-56"],["0","0","0","0","48","456","1768","3560","3892","2162","470","0","-8"],["0","0","0","0","0","8","64","200","304","226","72","8","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","16","264","1932","8232","22512","40986","49655","38412","16644","1984","-1392","-576","-64"],["0","0","72","1048","6672","24288","55370","81094","74594","38998","7488","-2384","-1312","-160"],["0","0","0","128","1632","8948","27424","50980","57968","37917","11228","-592","-1008","-144"],["0","0","0","0","112","1240","5776","14592","21388","17838","7408","778","-280","-56"],["0","0","0","0","0","48","456","1768","3560","3892","2162","470","0","-8"],["0","0","0","0","0","0","8","64","200","304","226","72","8","0"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["8","144","1164","5568","17478","37716","56953","60060","43356","20576","6000","960","64"],["0","24","384","2724","11256","29922","53304","64251","51678","26712","8304","1392","96"],["0","0","24","336","2052","7152","15618","22068","20115","11448","3816","672","48"],["0","0","0","8","96","492","1400","2406","2544","1617","582","108","8"]]},"step_quotients":[[{"coeff":{"coeffs":[["8","144","1132","4992","12822","15444","-12959","-90804","-184456","-219664","-167424","-81344","-23936","-3840","-256"],["16","328","2968","15516","51156","107142","127706","27725","-182518","-342668","-318680","-173840","-55072","-9280","-640"],["0","64","1128","8784","39516","112224","204270","222788","96405","-90336","-172172","-120576","-43536","-7936","-576"],["0","0","96","1496","10224","40036","98192","153810","147340","70203","-6102","-26568","-13360","-2832","-224"],["0","0","0","64","880","5248","17704","36880","48436","38928","17118","2544","-752","-320","-32"],["0","0","0","0","16","192","984","2800","4812","5088","3234","1164","216","16","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["-16","-304","-2568","-12568","-38532","-72324","-62198","62182","285750","460308","447224","282960","116256","29632","4224","256"],["0","-80","-1456","-11896","-57432","-181260","-389844","-575050","-563642","-325868","-52232","72272","60704","21440","3712","256"],["0","0","-144","-2448","-18648","-83880","-247068","-499356","-705330","-695574","-470340","-210096","-58176","-8928","-576","0"],["0","0","0","-112","-1744","-12072","-48872","-128068","-227052","-276526","-230358","-128580","-46384","-10240","-1248","-64"],["0","0","0","0","-32","-448","-2752","-9728","-21808","-32224","-31632","-20352","-8322","-2060","-280","-16"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","16","352","3552","21760","90264","267696","584072","950144","1155201","1042446","686932","321816","102960","21152","2496","128"],["0","0","48","960","8736","47808","175176","452736","846744","1156944","1151715","823908","412980","139488","29904","3648","192"],["0","0","0","48","864","7008","33792","107592","237552","371640","413664","324387","175134","62712","14064","1776","96"],["0","0","0","0","16","256","1824","7616","20632","37920","48040","41808","24513","9352","2200","288","16"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","8","160","1420","7384","24982","57664","92489","102894","77808","38384","11536","1888","128"],["0","0","-16","-200","-904","-924","7684","39050","91954","130179","116184","64424","20992","3632","256"],["0","0","-32","-512","-3552","-13888","-33056","-47232","-33608","4656","31434","27088","10864","2112","160"],["0","0","0","-48","-656","-3880","-12936","-26468","-33724","-25518","-9486","0","1200","352","32"],["0","0","0","0","-16","-192","-984","-2800","-4812","-5088","-3234","-1164","-216","-16","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","-16","-312","-2744","-14372","-49844","-120362","-207106","-255443","-224058","-136768","-55920","-14384","-2080","-128"],["0","0","48","800","5936","25776","72352","136616","174420","146132","72789","13956","-5224","-3712","-816","-64"],["0","0","0","80","1232","8424","33640","86804","151212","180446","146742","79554","27680","5840","672","32"],["0","0","0","0","32","448","2752","9728","21808","32224","31632","20352","8322","2060","280","16"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","-16","-320","-2912","-15936","-58392","-150912","-282248","-385648","-383905","-274636","-137660","-46496","-9968","-1216","-64"],["0","0","0","-32","-576","-4672","-22528","-71728","-158368","-247760","-275776","-216258","-116756","-41808","-9376","-1184","-64"],["0","0","0","0","-16","-256","-1824","-7616","-20632","-37920","-48040","-41808","-24513","-9352","-2200","-288","-16"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["-4","-10","-8"],["4","2","-4"],["0","2","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["6","27","36","12"],["-6","-14","-4","2"],["0","-4","-8","-2"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["2","12","25","20","4"],["0","2","8","9","2"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","-24","-336","-2044","-7048","-15034","-20220","-16513","-7014","-424","848","304","32"],["0","0","-80","-976","-5084","-14664","-25312","-26148","-14819","-3050","908","520","64"],["0","0","0","-96","-1016","-4496","-10704","-14616","-11126","-3972","-126","248","40"],["0","0","0","0","-48","-440","-1640","-3160","-3284","-1710","-326","16","8"],["0","0","0","0","0","-8","-64","-200","-304","-226","-72","-8","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","-16","-232","-1468","-5296","-11920","-17146","-15363","-7686","-1272","560","272","32"],["0","0","0","-56","-704","-3796","-11400","-20650","-22648","-13935","-3442","668","488","64"],["0","0","0","0","-72","-784","-3584","-8856","-12618","-10084","-3814","-158","240","40"],["0","0","0","0","0","-40","-376","-1440","-2856","-3058","-1638","-318","16","8"],["0","0","0","0","0","0","-8","-64","-200","-304","-226","-72","-8","0"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["8","144","1164","5568","17478","37716","56953","60060","43356","20576","6000","960","64"],["0","24","384","2724","11256","29922","53304","64251","51678","26712","8304","1392","96"],["0","0","24","336","2052","7152","15618","22068","20115","11448","3816","672","48"],["0","0","0","8","96","492","1400","2406","2544","1617","582","108","8"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","-48","-960","-8712","-47376","-171684","-436032","-794310","-1043796","-980856","-643728","-282912","-77760","-11904","-768"],["32","576","4384","17376","30336","-38448","-366440","-1042104","-1762978","-1959736","-1450104","-695744","-203744","-32640","-2176"],["32","736","7312","41376","146376","328176","425212","143720","-539884","-1117762","-1088516","-612560","-198368","-33952","-2368"],["0","112","2112","17544","84192","256356","508536","637190","426960","-1452","-265454","-226224","-88272","-16768","-1248"],["0","0","144","2336","16632","68032","175388","292968","310810","189768","41436","-21408","-16192","-3840","-320"],["0","0","0","80","1120","6808","23456","50092","67960","57426","27984","6252","-88","-272","-32"],["0","0","0","0","16","192","984","2800","4812","5088","3234","1164","216","16","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","72","1488","14028","79776","304902","825732","1627497","2360004","2515080","1946448","1068096","399552","95616","13056","768"],["-48","-1040","-10096","-57880","-216912","-553212","-960036","-1069666","-579329","254380","775780","699968","349712","101312","15808","1024"],["0","-176","-3472","-30880","-163464","-572376","-1392852","-2406808","-2961542","-2558543","-1498214","-553480","-108688","-4144","2080","256"],["0","0","-240","-4272","-34128","-161352","-501120","-1072692","-1614972","-1713702","-1265481","-632868","-205368","-40608","-4368","-192"],["0","0","0","-144","-2288","-16168","-66856","-179060","-324700","-404830","-345606","-197958","-73410","-16700","-2104","-112"],["0","0","0","0","-32","-448","-2752","-9728","-21808","-32224","-31632","-20352","-8322","-2060","-280","-16"]]},"deriv_order":1},{"coeff":{"coeffs":[["16","400","4608","32416","155544","538488","1387160","2702360","4005633","4508049","3814270","2382612","1068408","330032","65952","7616","384"],["0","64","1456","15168","95776","408864","1245960","2789024","4647320","5777748","5321499","3571636","1700244","551328","114512","13632","704"],["0","0","96","1968","18336","102624","384144","1013064","1931040","2685528","2717094","1972203","1001094","341688","73872","9072","480"],["0","0","0","64","1168","9600","46880","151072","337368","533440","599592","474324","258025","92968","20952","2656","144"],["0","0","0","0","16","256","1824","7616","20632","37920","48040","41808","24513","9352","2200","288","16"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["8","160","1492","8632","34690","102328","227279","382494","483777","450422","298384","133648","37520","5856","384"],["16","296","2504","13028","47628","132658","294190","522211","722588","746383","546704","267032","80224","13168","896"],["0","0","-88","-1280","-7828","-25176","-40106","-2488","121585","256170","271542","165440","56992","10208","736"],["0","0","-64","-1080","-7920","-33012","-85536","-140442","-139532","-67047","9336","30008","15072","3216","256"],["0","0","0","-64","-896","-5440","-18688","-39680","-53248","-44016","-20352","-3708","536","304","32"],["0","0","0","0","-16","-192","-984","-2800","-4812","-5088","-3234","-1164","-216","-16","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["-16","-336","-3272","-19616","-80996","-243872","-552142","-953840","-1260666","-1265023","-946602","-512720","-192112","-46448","-6432","-384"],["0","16","352","3352","18312","63580","145460","216146","186510","39484","-108491","-141932","-84680","-27520","-4656","-320"],["0","0","112","2016","16232","77072","239444","510320","760462","792404","568056","270946","81456","14192","1216","32"],["0","0","0","112","1776","12520","51624","137796","248860","308750","261990","148932","54706","12300","1528","80"],["0","0","0","0","32","448","2752","9728","21808","32224","31632","20352","8322","2060","280","16"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","-16","-368","-3872","-24672","-106200","-326088","-734984","-1232392","-1540849","-1426351","-961568","-459476","-149456","-31120","-3712","-192"],["0","0","-48","-992","-9312","-52480","-197704","-524464","-1005112","-1404704","-1427491","-1040166","-529736","-181296","-39280","-4832","-256"],["0","0","0","-48","-880","-7264","-35616","-115208","-258184","-409560","-461704","-366195","-199647","-72064","-16264","-2064","-112"],["0","0","0","0","-16","-256","-1824","-7616","-20632","-37920","-48040","-41808","-24513","-9352","-2200","-288","-16"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["4","48","244","680","1121","1096","600","160","16"],["0","8","80","328","704","834","524","152","16"],["0","0","4","32","100","152","113","36","4"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-1","-2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-2","-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 = f(n, theta) = 1 + (1) theta; 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":{"reason":"no parent theorem report with an interlacing conclusion","status":"none"},"lean_declarations":["RealRooted.isMultiplierSequence_eval_of_roots_nonpos","RealRooted.isPFMultiplierSequence_eval_of_roots_nonpos","RealRooted.isMultiplierSequence_iff_preserves"],"lift_summary":{"hypotheses":[{"evidence":"the polynomial with ascending coefficients [1, 1] is fixed; exact check: real-rooted = true, coefficients of one sign = true","name":"euler_polynomial_roots_nonpositive","statement":"the polynomial in theta is real-rooted with every root <= 0 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":{"reason":"no parent theorem report with an interlacing conclusion","status":"not_proved"},"lean_replay":"not_attempted","operation":{"description":"f(n, theta) = 1 + (1) theta","kind":"preserver_image","operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"euler_polynomial"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["3","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"relation":"Q_n = lambda(n) T_n(P_(n+0)) with T = f(n, theta) = 1 + (1) theta, for every n >= 0"},"parent_proof":{"route":"liu_wang_three_term","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 multiplier sequences: if f is a real polynomial whose roots are all real and <= 0, then (f(k))_(k >= 0) is a multiplier sequence, so x^k -> f(k) x^k maps every real-rooted polynomial to a real-rooted polynomial or zero (Laguerre; see T. Craven and G. Csordas, Multiplier sequences for fields, Illinois J. Math. 21 (1977); Polya--Schur, Theorem 40 of P. Branden, arXiv:1410.6601: sum_k f(k) x^k / k! = f(theta) e^x = C e^x x^m prod (1 + x/a_j), a_j > 0); f(k) has one sign for k >= 0, so coefficients of one sign stay of one sign; applied to f(n, .) for each n"},"verdict":"proved"},"notes":["the division remainder is removed by row annihilators of the shifted parent"],"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":"not applicable: expected one nonzero lag term","route":"product_recurrence","success":false,"variant":"product_recurrence"},{"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":"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":"HypothesisFailed: 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) = (2) + (2) x, V_n(x) = 0, W_n(x) = (1) + (2) x; open hypotheses: multipliers_vanish_at_zero: [x^0] c_2(n, x) = 1 is not the zero polynomial; lag_coefficient_nonpositive: W_n is not separable with a factor of one sign on (-inf, 0), and the sufficient monomial test (-1)^k [x^k] W_n <= 0 fails for k = 0 (not a disproof): fails at n = 2: [x^0] W_n = 1 there (exact); derivative_or_lag_coefficient_negative: W_n is not separable with a factor of one sign on (-inf, 0), and the sufficient monomial test (-1)^k [x^k] W_n <= 0 fails for k = 0 (not a disproof): fails at n = 2: [x^0] W_n = 1 there (exact)","route":"liu_wang_derivative_lag","success":false,"variant":"liu_wang_derivative_lag"},{"detail":"not applicable: the rule is not f(n) P_n = c_0(n, x) P_(n-1) + gamma(n) (x - L)(x - U) P'_(n-1)","route":"ma_wang_interval","success":false,"variant":"ma_wang_interval"},{"detail":"P_n = A_n(x) P_(n-1) + B_n(x) P_(n-2) for n >= 2, with A_n(x) = (2) + (2) x, B_n(x) = (1) + (2) x: every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, -1/2] (so its coefficients have one sign); for n >= 1, P_(n-1) interlaces P_n (weakly, in the sense of Liu and Wang), and deg P_n - deg P_(n-1) is 0 or 1 for n >= 2","route":"liu_wang_three_term","success":true,"variant":"liu_wang_three_term"}],"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) + B_n(x) P_(n-2) for n >= 2, with A_n(x) = (2) + (2) x, B_n(x) = (1) + (2) x","every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, -1/2] (so its coefficients have one sign); for n >= 1, P_(n-1) interlaces P_n (weakly, in the sense of Liu and Wang), and deg P_n - deg P_(n-1) is 0 or 1 for n >= 2"],"theorem":"liu_wang_three_term: L. L. Liu and Y. Wang, Adv. Appl. Math. 38 (2007) 542-560, Theorem 2.1 and Corollary 2.4 (A unified approach to polynomial sequences with only real zeros; the lag row as the interlacer, b_n = 0), weak interlacing of consecutive rows, with nonnegativity of the coefficients replaced, where a root region is certified, by an exact root-location induction"},"kind":"weak","orientation":"previous_interlaces_next"},"route":"liu_wang_three_term","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 = f(n, theta) = 1 + (1) theta 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"}