{"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"],["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":[["-6","-4"],["5","4"],["-2","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-10","-23","-8"],["4","8","2"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-2","-8","-9","-2"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["2"],["1"]]},"deriv_order":0,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"denominator":{"coeffs":[["1"],["1"]]},"terms":[{"coeff":{"coeffs":[["2","0","2","4"],["2","3","-6","-6"],["0","3","4","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","-2","5","18","8"],["0","-2","-10","-12","-4"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","0","2","9","8","2"]]},"deriv_order":2,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["1"],"operator":{"schedule":{"first_degree":0,"first_index":0,"step":1},"shape":"reversal"},"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":[["4","24","50","40","8"],["2","16","41","38","8"],["0","2","8","9","2"]]},"deriv_order":0}],"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":[["-2","-12","-25","-20","-4"],["0","-2","-8","-9","-2"]]},"deriv_order":0}],"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":[["2","12","25","20","4"],["0","2","8","9","2"]]},"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 = x^(d_n) P(1/x), d_n = 0 + 1 (n - 0); 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":"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"],["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 = x^(d_n) P(1/x), d_n = 0 + 1 (n - 0), 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":"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_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 = 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"}