{"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","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":[["32","64","42","10","0"],["64","184","160","40","-1"],["0","48","80","32","1"],["0","0","8","6","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-128","-544","-912","-734","-278","-42","-2"],["0","-64","-232","-320","-188","-39","-2"],["0","0","16","16","-4","-3","0"],["0","0","0","8","6","0","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-64","-288","-488","-388","-144","-21","-1"],["0","0","-64","-208","-240","-114","-19","-1"],["0","0","0","-16","-32","-18","-2","0"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["-32","-64","-42","-10","0"],["0","8","12","0","-1"],["0","0","8","8","1"],["0","0","0","2","0"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-32","-64","-42","-10","0"],["0","0","8","12","0","-1"],["0","0","0","8","8","1"],["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":[["-32","-72","-46","-4","2"],["0","8","-4","-10","-3"],["0","0","8","2","1"],["0","0","0","2","0"]]},"terms":[{"coeff":{"coeffs":[["32","72","46","4","-2"],["-64","-88","-24","6","3"],["0","-48","-56","-14","-1"],["0","0","-8","-6","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["64","224","296","180","48","4","0"],["0","64","176","176","78","15","1"],["0","0","16","32","18","2","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","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":[["-16384","-114688","-357376","-653312","-776960","-629504","-353232","-136512","-35316","-5756","-524","-20","0"],["0","20480","133120","377856","614400","630592","423840","186816","52232","8464","614","-4","-2"],["0","0","-4096","-24576","-61184","-81152","-60288","-22656","-1292","2260","850","120","6"],["0","0","0","-2048","-11776","-29440","-41728","-36576","-20248","-6932","-1382","-144","-6"],["0","0","0","0","0","512","2176","3712","3232","1512","370","44","2"],["0","0","0","0","0","256","1024","1600","1216","452","72","4","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","-16384","-114688","-357376","-653312","-776960","-629504","-353232","-136512","-35316","-5756","-524","-20","0"],["0","0","20480","133120","377856","614400","630592","423840","186816","52232","8464","614","-4","-2"],["0","0","0","-4096","-24576","-61184","-81152","-60288","-22656","-1292","2260","850","120","6"],["0","0","0","0","-2048","-11776","-29440","-41728","-36576","-20248","-6932","-1382","-144","-6"],["0","0","0","0","0","0","512","2176","3712","3232","1512","370","44","2"],["0","0","0","0","0","0","256","1024","1600","1216","452","72","4","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":[["0","12288","81920","238080","395520","413760","282944","127064","36644","6424","612","24","0"],["0","0","-4096","-26624","-73472","-112128","-103040","-57952","-19212","-3304","-170","20","2"],["0","0","0","-2048","-11776","-28672","-38528","-31264","-15800","-4968","-940","-96","-4"],["0","0","0","0","0","768","3200","5312","4448","1964","442","48","2"],["0","0","0","0","0","256","1024","1600","1216","452","72","4","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","8192","53248","152064","250624","263168","183168","85032","25740","4788","484","20","0"],["0","0","0","-6144","-36864","-94464","-134656","-116384","-62144","-19820","-3336","-170","20","2"],["0","0","0","0","-1024","-5632","-13824","-19840","-18128","-10680","-3924","-836","-92","-4"],["0","0","0","0","0","512","2816","6400","7744","5352","2108","450","48","2"],["0","0","0","0","0","0","256","1024","1600","1216","452","72","4","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 = 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","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 = 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) + (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 = 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"}