{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","1"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"basis_map_A007318 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":[["0","14","22","9","1"],["8","44","60","26","3"],["24","42","24","3","0"],["8","6","0","0","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-96","-330","-462","-326","-115","-18","-1"],["-72","-180","-166","-72","-14","-1","0"],["8","10","6","1","0","0","0"],["8","6","0","0","0","0","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-96","-344","-484","-335","-116","-18","-1"],["-80","-224","-226","-98","-17","-1","0"],["-16","-32","-18","-2","0","0","0"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["0","-14","-22","-9","-1"],["-8","-14","0","6","1"],["0","8","8","1","0"],["0","2","0","0","0"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-14","-22","-9","-1"],["-8","-14","0","6","1"],["0","8","8","1","0"],["0","2","0","0","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":[["8","6","-14","-14","-2"],["-8","-24","-16","4","1"],["0","2","8","1","0"],["0","2","0","0","0"]]},"terms":[{"coeff":{"coeffs":[["-8","-6","14","14","2"],["16","22","-12","-20","-3"],["0","-24","-24","-3","0"],["-8","-6","0","0","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["32","152","276","239","99","17","1"],["48","160","190","94","17","1","0"],["16","32","18","2","0","0","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":"derivative_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","1"]]},"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":[["-2","0"],["-4","-2"],["0","-2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["8","4","-6","-2"],["0","8","8","1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-8","-16","-9","-1"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["2"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","-7168","-47104","-136192","-227840","-244016","-174848","-85092","-27972","-6054","-818","-62","-2"],["-4096","-27648","-71680","-77824","11200","134288","174736","120812","50784","13196","2046","172","6"],["0","8192","50176","128256","173056","123072","28432","-23276","-22316","-8356","-1610","-156","-6"],["0","1024","0","-17664","-54016","-75376","-57248","-23144","-3512","672","330","44","2"],["0","0","-1024","-3584","-3328","2560","7536","6280","2544","522","52","2","0"],["0","0","0","256","1024","1600","1216","452","72","4","0","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","-7168","-47104","-136192","-227840","-244016","-174848","-85092","-27972","-6054","-818","-62","-2"],["-4096","-27648","-71680","-77824","11200","134288","174736","120812","50784","13196","2046","172","6"],["0","8192","50176","128256","173056","123072","28432","-23276","-22316","-8356","-1610","-156","-6"],["0","1024","0","-17664","-54016","-75376","-57248","-23144","-3512","672","330","44","2"],["0","0","-1024","-3584","-3328","2560","7536","6280","2544","522","52","2","0"],["0","0","0","256","1024","1600","1216","452","72","4","0","0","0"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["-32768","-245760","-823296","-1624064","-2093568","-1850112","-1143488","-495072","-147984","-29560","-3720","-264","-8"],["0","49152","344064","1062912","1904640","2188032","1681152","874656","305280","69336","9672","744","24"],["0","0","-24576","-159744","-451584","-726528","-730752","-475200","-199728","-52776","-8280","-696","-24"],["0","0","0","4096","24576","62976","89600","76992","40704","12936","2328","216","8"]]},"step_quotients":[[{"coeff":{"coeffs":[["32768","278528","1069056","2447360","3717632","3943680","2993600","1638560","643056","177544","33280","3984","272","8"],["65536","540672","1990656","4311040","6091776","5888256","3968128","1864800","601248","128456","17112","1272","40","0"],["0","-65536","-565248","-2150400","-4762624","-6818304","-6619008","-4443328","-2064528","-654024","-136736","-17808","-1296","-40"],["0","0","0","45056","290816","815616","1300480","1294912","832704","345816","90288","14016","1168","40"],["0","0","0","16384","98304","251904","358400","307968","162816","51744","9312","864","32","0"],["0","0","0","0","-4096","-24576","-62976","-89600","-76992","-40704","-12936","-2328","-216","-8"]]},"deriv_order":0},{"coeff":{"coeffs":[["-131072","-1179648","-4800512","-11665408","-18819072","-21174272","-16956160","-9644544","-3780800","-929472","-92688","21056","9444","1548","124","4"],["0","65536","557056","2072576","4403200","5788672","4639232","1800064","-423104","-1000864","-635056","-229408","-51152","-6896","-512","-16"],["0","0","98304","786432","2863104","6279168","9248256","9643008","7299648","4041024","1623888","463296","90168","11208","792","24"],["0","0","0","-81920","-614400","-2054144","-4033536","-5158656","-4504192","-2736928","-1158480","-336672","-65104","-7920","-544","-16"],["0","0","0","0","16384","114688","352256","622592","697856","515584","253056","81408","16644","2060","140","4"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","131072","1245184","5406720","14204928","25194496","31868928","29607936","20500480","10623264","4101680","1164824","237828","33664","3112","168","4"],["0","0","-196608","-1769472","-7225344","-17694720","-28944384","-33331200","-27746304","-16877568","-7496112","-2404464","-545004","-84240","-8376","-480","-12"],["0","0","0","98304","835584","3194880","7249920","10847232","11241984","8252160","4312704","1591704","406380","69312","7464","456","12"],["0","0","0","0","-16384","-131072","-466944","-974848","-1320448","-1213440","-768640","-334464","-98052","-18704","-2200","-144","-4"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","-8192","-61440","-203776","-392704","-485760","-401984","-224976","-84168","-20352","-2992","-240","-8"],["0","0","-16384","-110592","-325632","-547328","-576768","-393792","-173856","-48120","-7848","-680","-24","0"],["0","0","0","24576","159744","451584","726528","730752","475200","199728","52776","8280","696","24"],["0","0","0","8192","45056","101376","116224","64384","4416","-14832","-8280","-1896","-200","-8"],["0","0","0","0","-4096","-24576","-62976","-89600","-76992","-40704","-12936","-2328","-216","-8"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-8192","-61440","-207872","-419328","-561024","-523072","-346768","-163368","-53640","-11788","-1620","-124","-4"],["0","0","32768","262144","958464","2121728","3172352","3379200","2631296","1509504","633432","190048","39068","5124","380","12"],["0","0","0","-49152","-368640","-1234944","-2436096","-3140352","-2775168","-1715232","-742608","-221976","-44340","-5580","-396","-12"],["0","0","0","0","16384","114688","352256","622592","697856","515584","253056","81408","16644","2060","140","4"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","-65536","-589824","-2408448","-5898240","-9648128","-11110400","-9248768","-5625856","-2498704","-801488","-181668","-28080","-2792","-160","-4"],["0","0","0","65536","557056","2129920","4833280","7231488","7494656","5501440","2875136","1061136","270920","46208","4976","304","8"],["0","0","0","0","-16384","-131072","-466944","-974848","-1320448","-1213440","-768640","-334464","-98052","-18704","-2200","-144","-4"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0"],["0","-2"],["0","0"],["0","2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-16","-26","-12","-2"],["8","20","16","3"],["0","-8","-8","-1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-16","-40","-34","-11","-1"],["0","8","16","9","1"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["6144","37376","102656","171648","199584","173256","114748","56800","20064","4766","706","58","2"],["5120","26112","56832","66688","37392","-11080","-41756","-39392","-20612","-6386","-1136","-106","-4"],["1024","2048","-6912","-33536","-61680","-64128","-39232","-12080","60","1298","386","46","2"],["0","-512","-2560","-4480","-1536","5688","9512","6868","2624","526","52","2","0"],["0","0","0","256","1024","1600","1216","452","72","4","0","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","3584","21760","57216","85312","79352","47748","18672","4650","702","58","2"],["0","2048","12800","31232","34176","5920","-27448","-33968","-19548","-6282","-1132","-106","-4"],["0","0","-3072","-17152","-39936","-49472","-33840","-11020","164","1302","386","46","2"],["0","0","-512","-1280","896","6592","9656","6876","2624","526","52","2","0"],["0","0","0","256","1024","1600","1216","452","72","4","0","0","0"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["-32768","-245760","-823296","-1624064","-2093568","-1850112","-1143488","-495072","-147984","-29560","-3720","-264","-8"],["0","49152","344064","1062912","1904640","2188032","1681152","874656","305280","69336","9672","744","24"],["0","0","-24576","-159744","-451584","-726528","-730752","-475200","-199728","-52776","-8280","-696","-24"],["0","0","0","4096","24576","62976","89600","76992","40704","12936","2328","216","8"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","-65536","-491520","-1646592","-3248128","-4187136","-3700224","-2286976","-990144","-295968","-59120","-7440","-528","-16"],["0","-98304","-638976","-1781760","-2746368","-2471424","-1174272","-68160","264096","166608","49992","8184","696","24"],["0","-32768","-98304","159744","1245184","2717184","3260928","2438464","1178496","368400","72896","8736","576","16"],["0","0","49152","270336","591872","599040","134400","-331904","-396960","-212496","-63120","-10512","-912","-32"],["0","0","0","-24576","-147456","-377856","-537600","-461952","-244224","-77616","-13968","-1296","-48","0"],["0","0","0","0","4096","24576","62976","89600","76992","40704","12936","2328","216","8"]]},"deriv_order":0},{"coeff":{"coeffs":[["131072","1212416","5079040","12750848","21389312","25303552","21711872","13684928","6344416","2144272","517768","86216","9320","584","16","0"],["-131072","-1245184","-5505024","-14917632","-27492352","-36209664","-34936320","-24956800","-13213152","-5149568","-1456136","-291840","-39988","-3532","-180","-4"],["0","327680","2686976","10043392","22654976","34402304","37130752","29303552","17130560","7432048","2374408","548368","88496","9392","584","16"],["0","0","-294912","-2277376","-7905280","-16295936","-22206464","-21078272","-14310784","-7026912","-2493336","-630912","-110408","-12584","-832","-24"],["0","0","0","114688","843776","2758656","5278720","6554368","5535360","3243040","1321296","369960","69224","8200","552","16"],["0","0","0","0","-16384","-114688","-352256","-622592","-697856","-515584","-253056","-81408","-16644","-2060","-140","-4"]]},"deriv_order":1},{"coeff":{"coeffs":[["262144","2490368","10813440","28409856","50388992","63737856","59215872","41000960","21246528","8203360","2329648","475656","67328","6224","336","8","0"],["0","-524288","-4784128","-19857408","-49594368","-83083264","-98531328","-85100544","-54255616","-25615488","-8910608","-2254832","-406308","-50416","-4072","-192","-4"],["0","0","393216","3440640","13615104","32194560","50638848","55815168","44250624","25502976","10679520","3217224","683628","99168","9288","504","12"],["0","0","0","-131072","-1097728","-4128768","-9199616","-13488128","-13668864","-9789440","-4981632","-1787808","-443788","-73712","-7752","-464","-12"],["0","0","0","0","16384","131072","466944","974848","1320448","1213440","768640","334464","98052","18704","2200","144","4"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["32768","245760","815104","1570816","1943040","1607936","899904","336672","81408","11968","960","32","0","0"],["65536","475136","1548288","3020800","3984384","3819264","2787712","1579552","684864","217280","47248","6480","496","16"],["0","-65536","-434176","-1265664","-2145280","-2365952","-1815936","-1024192","-442704","-146952","-35144","-5384","-456","-16"],["0","0","32768","184320","421888","478720","221184","-84544","-172608","-101592","-31128","-5240","-456","-16"],["0","0","0","-16384","-94208","-227328","-295424","-218368","-85824","-11040","3624","1464","184","8"],["0","0","0","0","4096","24576","62976","89600","76992","40704","12936","2328","216","8"]]},"deriv_order":0},{"coeff":{"coeffs":[["-131072","-1179648","-4833280","-11919360","-19712000","-23059456","-19619584","-12297856","-5690944","-1929712","-470616","-79736","-8824","-568","-16","0"],["0","196608","1638400","6184960","13971456","21015552","22167040","16826496","9292352","3735904","1085304","224192","31988","2988","164","4"],["0","0","-163840","-1261568","-4362240","-8943616","-12093952","-11356416","-7599040","-3663648","-1273488","-316136","-54628","-6204","-412","-12"],["0","0","0","81920","598016","1939456","3681280","4536064","3806336","2221344","905424","255264","48460","5860","404","12"],["0","0","0","0","-16384","-114688","-352256","-622592","-697856","-515584","-253056","-81408","-16644","-2060","-140","-4"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","-131072","-1179648","-4816896","-11796480","-19296256","-22220800","-18497536","-11251712","-4997408","-1602976","-363336","-56160","-5584","-320","-8","0"],["0","0","196608","1703936","6668288","15564800","24111104","26099712","20251648","11376128","4620976","1343328","274084","38032","3400","176","4"],["0","0","0","-98304","-819200","-3063808","-6782976","-9872384","-9921536","-7038720","-3544064","-1257240","-308328","-50608","-5264","-312","-8"],["0","0","0","0","16384","131072","466944","974848","1320448","1213440","768640","334464","98052","18704","2200","144","4"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["1024","5120","10752","12288","8272","3312","756","88","4"],["0","-1024","-4608","-8448","-8064","-4240","-1192","-160","-8"],["0","0","256","1024","1600","1216","452","72","4"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-1","-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 + (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":{"reason":"no parent theorem report with an interlacing conclusion","status":"none"},"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 [1, 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":{"reason":"no parent theorem report with an interlacing conclusion","status":"not_proved"},"lean_replay":"not_attempted","operation":{"description":"phi(n, D) = 1 + (1) D","kind":"preserver_image","operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","1"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"relation":"Q_n = lambda(n) T_n(P_(n+0)) with T = phi(n, D) = 1 + (1) D, 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 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_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) + (1) x, V_n(x) = 0, W_n(x) = (1) + (1) 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) + (1) x, B_n(x) = (1) + (1) x: every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, -1] (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) + (1) x, B_n(x) = (1) + (1) x","every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, -1] (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 = phi(n, D) = 1 + (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"}