{"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"],["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","4"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","4"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"basis_map_A013611 of Square array A(n,r), the number of neighbors at a sharp Manhattan distance r in a finite n-hypercube lattice, read by upwards antidiagonals; A(n,r) = Sum_{k=0..min(n,r)} binomial(r-1,k-1)*binomial(n,k)* 2^k."},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["2","16","42","40","0"],["4","46","160","160","-16"],["0","12","80","128","16"],["0","0","8","24","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-2","-34","-228","-734","-1112","-672","-128"],["0","-4","-58","-320","-752","-624","-128"],["0","0","4","16","-16","-48","0"],["0","0","0","8","24","0","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-1","-18","-122","-388","-576","-336","-64"],["0","0","-4","-52","-240","-456","-304","-64"],["0","0","0","-4","-32","-72","-32","0"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["-2","-16","-42","-40","0"],["0","2","12","0","-16"],["0","0","8","32","16"],["0","0","0","8","0"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-2","-16","-42","-40","0"],["0","0","2","12","0","-16"],["0","0","0","8","32","16"],["0","0","0","0","8","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":[["-2","-18","-46","-16","32"],["0","2","-4","-40","-48"],["0","0","8","8","16"],["0","0","0","8","0"]]},"terms":[{"coeff":{"coeffs":[["2","18","46","16","-32"],["-4","-22","-24","24","48"],["0","-12","-56","-56","-16"],["0","0","-8","-24","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["1","14","74","180","192","64","0"],["0","4","44","176","312","240","64"],["0","0","4","32","72","32","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"],["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","4"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","4"]]},"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":[["-1","0"],["-2","-4"],["0","-4"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["1","2","-12","-16"],["0","4","16","8"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-1","-8","-18","-8"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["-2","-56","-698","-5104","-24280","-78688","-176616","-273024","-282528","-184192","-67072","-10240","0"],["0","10","260","2952","19200","78824","211920","373632","417856","270848","78592","-2048","-4096"],["0","0","-8","-192","-1912","-10144","-30144","-45312","-10336","72320","108800","61440","12288"],["0","0","0","-16","-368","-3680","-20864","-73152","-161984","-221824","-176896","-73728","-12288"],["0","0","0","0","0","64","1088","7424","25856","48384","47360","22528","4096"],["0","0","0","0","0","32","512","3200","9728","14464","9216","2048","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","-2","-56","-698","-5104","-24280","-78688","-176616","-273024","-282528","-184192","-67072","-10240","0"],["0","0","10","260","2952","19200","78824","211920","373632","417856","270848","78592","-2048","-4096"],["0","0","0","-8","-192","-1912","-10144","-30144","-45312","-10336","72320","108800","61440","12288"],["0","0","0","0","-16","-368","-3680","-20864","-73152","-161984","-221824","-176896","-73728","-12288"],["0","0","0","0","0","0","64","1088","7424","25856","48384","47360","22528","4096"],["0","0","0","0","0","0","32","512","3200","9728","14464","9216","2048","0"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["-1","-30","-402","-3172","-16356","-57816","-142936","-247536","-295968","-236480","-119040","-33792","-4096"],["0","6","168","2076","14880","68376","210144","437328","610560","554688","309504","95232","12288"],["0","0","-12","-312","-3528","-22704","-91344","-237600","-399456","-422208","-264960","-89088","-12288"],["0","0","0","8","192","1968","11200","38496","81408","103488","74496","27648","4096"]]},"step_quotients":[[{"coeff":{"coeffs":[["1","34","522","4780","29044","123240","374200","819280","1286112","1420352","1064960","509952","139264","16384"],["2","66","972","8420","47592","184008","496016","932400","1202496","1027648","547584","162816","20480","0"],["0","-8","-276","-4200","-37208","-213072","-827376","-2221664","-4129056","-5232192","-4375552","-2279424","-663552","-81920"],["0","0","0","88","2272","25488","162560","647456","1665408","2766528","2889216","1794048","598016","81920"],["0","0","0","32","768","7872","44800","153984","325632","413952","297984","110592","16384","0"],["0","0","0","0","-32","-768","-7872","-44800","-153984","-325632","-413952","-297984","-110592","-16384"]]},"deriv_order":0},{"coeff":{"coeffs":[["-1","-36","-586","-5696","-36756","-165424","-529880","-1205568","-1890400","-1858944","-741504","673792","1208832","792576","253952","32768"],["0","2","68","1012","8600","45224","144976","225008","-211552","-2001728","-5080448","-7341056","-6547456","-3530752","-1048576","-131072"],["0","0","12","384","5592","49056","289008","1205376","3649824","8082048","12991104","14825472","11541504","5738496","1622016","196608"],["0","0","0","-40","-1200","-16048","-126048","-644832","-2252096","-5473856","-9267840","-10773504","-8333312","-4055040","-1114112","-131072"],["0","0","0","0","32","896","11008","77824","348928","1031168","2024448","2605056","2130432","1054720","286720","32768"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","1","38","660","6936","49208","248976","925248","2562560","5311632","8203360","9318592","7610496","4308992","1593344","344064","32768"],["0","0","-6","-216","-3528","-34560","-226128","-1041600","-3468288","-8438784","-14992224","-19235712","-17440128","-10782720","-4288512","-983040","-98304"],["0","0","0","12","408","6240","56640","338976","1405248","4126080","8625408","12733632","13004160","8871936","3821568","933888","98304"],["0","0","0","0","-8","-256","-3648","-30464","-165056","-606720","-1537280","-2675712","-3137664","-2394112","-1126400","-294912","-32768"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","-2","-60","-796","-6136","-30360","-100496","-224976","-336672","-325632","-191488","-61440","-8192"],["0","0","-4","-108","-1272","-8552","-36048","-98448","-173856","-192480","-125568","-43520","-6144","0"],["0","0","0","24","624","7056","45408","182688","475200","798912","844416","529920","178176","24576"],["0","0","0","8","176","1584","7264","16096","4416","-59328","-132480","-121344","-51200","-8192"],["0","0","0","0","-16","-384","-3936","-22400","-76992","-162816","-206976","-148992","-55296","-8192"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-2","-60","-812","-6552","-35064","-130768","-346768","-653472","-858240","-754432","-414720","-126976","-16384"],["0","0","2","64","936","8288","49568","211200","657824","1509504","2533728","3040768","2500352","1311744","389120","49152"],["0","0","0","-12","-360","-4824","-38064","-196272","-693792","-1715232","-2970432","-3551616","-2837760","-1428480","-405504","-49152"],["0","0","0","0","16","448","5504","38912","174464","515584","1012224","1302528","1065216","527360","143360","16384"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","-1","-36","-588","-5760","-37688","-173600","-578048","-1406464","-2498704","-3205952","-2906688","-1797120","-714752","-163840","-16384"],["0","0","0","4","136","2080","18880","112992","468416","1375360","2875136","4244544","4334720","2957312","1273856","311296","32768"],["0","0","0","0","-4","-128","-1824","-15232","-82528","-303360","-768640","-1337856","-1568832","-1197056","-563200","-147456","-16384"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0"],["0","-8"],["0","0"],["0","8"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-4","-26","-48","-32"],["2","20","64","48"],["0","-8","-32","-16"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-1","-10","-34","-44","-16"],["0","2","16","36","16"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","3","80","930","6180","25860","70736","127064","146576","102784","39168","6144","0"],["0","0","-4","-104","-1148","-7008","-25760","-57952","-76848","-52864","-10880","5120","2048"],["0","0","0","-8","-184","-1792","-9632","-31264","-63200","-79488","-60160","-24576","-4096"],["0","0","0","0","0","48","800","5312","17792","31424","28288","12288","2048"],["0","0","0","0","0","16","256","1600","4864","7232","4608","1024","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","2","52","594","3916","16448","45792","85032","102960","76608","30976","5120","0"],["0","0","0","-6","-144","-1476","-8416","-29096","-62144","-79280","-53376","-10880","5120","2048"],["0","0","0","0","-4","-88","-864","-4960","-18128","-42720","-62784","-53504","-23552","-4096"],["0","0","0","0","0","8","176","1600","7744","21408","33728","28800","12288","2048"],["0","0","0","0","0","0","16","256","1600","4864","7232","4608","1024","0"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["-1","-30","-402","-3172","-16356","-57816","-142936","-247536","-295968","-236480","-119040","-33792","-4096"],["0","6","168","2076","14880","68376","210144","437328","610560","554688","309504","95232","12288"],["0","0","-12","-312","-3528","-22704","-91344","-237600","-399456","-422208","-264960","-89088","-12288"],["0","0","0","8","192","1968","11200","38496","81408","103488","74496","27648","4096"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","-16","-480","-6432","-50752","-261696","-925056","-2286976","-3960576","-4735488","-3783680","-1904640","-540672","-65536"],["0","-24","-624","-6960","-42912","-154464","-293568","-68160","1056384","2665728","3199488","2095104","712704","98304"],["0","-8","-96","624","19456","169824","815232","2438464","4713984","5894400","4665344","2236416","589824","65536"],["0","0","48","1056","9248","37440","33600","-331904","-1587840","-3399936","-4039680","-2691072","-933888","-131072"],["0","0","0","-96","-2304","-23616","-134400","-461952","-976896","-1241856","-893952","-331776","-49152","0"],["0","0","0","0","64","1536","15744","89600","307968","651264","827904","595968","221184","32768"]]},"deriv_order":0},{"coeff":{"coeffs":[["2","74","1240","12452","83552","395368","1356992","3421232","6344416","8577088","8284288","5517824","2385920","598016","65536","0"],["-2","-76","-1344","-14568","-107392","-565776","-2183520","-6239200","-13213152","-20598272","-23298176","-18677760","-10236928","-3616768","-737280","-65536"],["0","20","656","9808","88496","537536","2320672","7325888","17130560","29728192","37990528","35095552","22654976","9617408","2392064","262144"],["0","0","-72","-2224","-30880","-254624","-1387904","-5269568","-14310784","-28107648","-39893376","-40378368","-28264448","-12886016","-3407872","-393216"],["0","0","0","112","3296","43104","329920","1638592","5535360","12972160","21140736","23677440","17721344","8396800","2260992","262144"],["0","0","0","0","-64","-1792","-22016","-155648","-697856","-2062336","-4048896","-5210112","-4260864","-2109440","-573440","-65536"]]},"deriv_order":1},{"coeff":{"coeffs":[["1","38","660","6936","49208","248976","925248","2562560","5311632","8203360","9318592","7610496","4308992","1593344","344064","32768","0"],["0","-8","-292","-4848","-48432","-324544","-1539552","-5318784","-13563904","-25615488","-35642432","-36077312","-26003712","-12906496","-4169728","-786432","-65536"],["0","0","24","840","13296","125760","791232","3488448","11062656","25502976","42718080","51475584","43752192","25387008","9510912","2064384","196608"],["0","0","0","-32","-1072","-16128","-143744","-843008","-3417216","-9789440","-19926528","-28604928","-28402432","-18870272","-7938048","-1900544","-196608"],["0","0","0","0","16","512","7296","60928","330112","1213440","3074560","5351424","6275328","4788224","2252800","589824","65536"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["1","30","398","3068","15180","50248","112488","168336","162816","95744","30720","4096","0","0"],["2","58","756","5900","31128","119352","348464","789776","1369728","1738240","1511936","829440","253952","32768"],["0","-8","-212","-2472","-16760","-73936","-226992","-512096","-885408","-1175616","-1124608","-689152","-233472","-32768"],["0","0","16","360","3296","14960","27648","-42272","-345216","-812736","-996096","-670720","-233472","-32768"],["0","0","0","-32","-736","-7104","-36928","-109184","-171648","-88320","115968","187392","94208","16384"],["0","0","0","0","32","768","7872","44800","153984","325632","413952","297984","110592","16384"]]},"deriv_order":0},{"coeff":{"coeffs":[["-1","-36","-590","-5820","-38500","-180152","-613112","-1537232","-2845472","-3859424","-3764928","-2551552","-1129472","-290816","-32768","0"],["0","6","200","3020","27288","164184","692720","2103312","4646176","7471808","8682432","7174144","4094464","1529856","335872","32768"],["0","0","-20","-616","-8520","-69872","-377936","-1419552","-3799520","-7327296","-10187904","-10116352","-6992384","-3176448","-843776","-98304"],["0","0","0","40","1168","15152","115040","567008","1903168","4442688","7243392","8168448","6202880","3000320","827392","98304"],["0","0","0","0","-32","-896","-11008","-77824","-348928","-1031168","-2024448","-2605056","-2130432","-1054720","-286720","-32768"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","-1","-36","-588","-5760","-37688","-173600","-578048","-1406464","-2498704","-3205952","-2906688","-1797120","-714752","-163840","-16384","0"],["0","0","6","208","3256","30400","188368","815616","2531456","5688064","9241952","10746624","8770688","4868096","1740800","360448","32768"],["0","0","0","-12","-400","-5984","-52992","-308512","-1240192","-3519360","-7088128","-10057920","-9866496","-6477824","-2695168","-638976","-65536"],["0","0","0","0","8","256","3648","30464","165056","606720","1537280","2675712","3137664","2394112","1126400","294912","32768"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["1","20","168","768","2068","3312","3024","1408","256"],["0","-4","-72","-528","-2016","-4240","-4768","-2560","-512"],["0","0","4","64","400","1216","1808","1152","256"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-1","-4"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-2","-4"]]},"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"],["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","4"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","4"]]},"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) + (4) x, V_n(x) = 0, W_n(x) = (1) + (4) x; open hypotheses: seed_degree_step: degrees 0 and 0 (exact); seed_strict_interlacing: the Bezout test fails or the degrees do not differ by one (exact); 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) + (4) x, B_n(x) = (1) + (4) x: every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, -1/4] (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) + (4) x, B_n(x) = (1) + (4) x","every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, -1/4] (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"}