{"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"],["2","4"]],"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 delannoy"},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["-12","-44","24","8","-112","-64"],["-32","-178","-180","-4","-16","0"],["-4","-40","-32","48","0","0"],["8","24","0","0","0","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-15","-74","-96","-276","-548","-352","-64"],["-40","-250","-396","-276","-224","-64","0"],["-8","-72","-104","16","0","0","0"],["8","24","0","0","0","0","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-3","-30","-120","-284","-436","-288","-64"],["-8","-72","-216","-272","-208","-64","0"],["-4","-32","-72","-32","0","0","0"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["2","6","-8","4","16"],["6","22","8","20","16"],["4","24","16","16","0"],["0","8","0","0","0"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["2","6","-8","4","16"],["6","22","8","20","16"],["4","24","16","16","0"],["0","8","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":[["0","0","0","0","0"],["-2","-2","-24","-12","16"],["4","0","16","16","0"],["0","8","0","0","0"]]},"terms":[{"coeff":{"coeffs":[["-8","-70","-172","-60","96","64"],["0","26","116","100","16","0"],["28","112","32","-48","0","0"],["-8","-24","0","0","0","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-1","-10","-24","44","228","224","64"],["0","8","72","208","208","64","0"],["4","32","72","32","0","0","0"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["1","2","1"],"operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["2","4"]],"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":[["-4","-8"],["2","8"],["-4","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-6","-30","-24"],["4","16","8"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-1","-8","-18","-8"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["2"],["2"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","4","76","576","2168","4016","3024","2112","9504","15744","9728","2048"],["0","0","16","312","2496","10512","25088","35744","38144","44736","42752","21504","4096"],["0","0","20","412","3520","16120","42992","69648","74560","61984","38272","13824","2048"],["0","0","8","192","1856","9376","26784","44160","43136","27776","11264","2048","0"],["0","0","0","16","256","1600","4864","7232","4608","1024","0","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","4","76","576","2168","4016","3024","2112","9504","15744","9728","2048"],["0","0","16","312","2496","10512","25088","35744","38144","44736","42752","21504","4096"],["0","0","20","412","3520","16120","42992","69648","74560","61984","38272","13824","2048"],["0","0","8","192","1856","9376","26784","44160","43136","27776","11264","2048","0"],["0","0","0","16","256","1600","4864","7232","4608","1024","0","0","0"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["0","0","0","8","192","1968","11200","38496","81408","103488","74496","27648","4096"],["0","0","0","24","576","5904","33600","115488","244224","310464","223488","82944","12288"],["0","0","0","24","576","5904","33600","115488","244224","310464","223488","82944","12288"],["0","0","0","8","192","1968","11200","38496","81408","103488","74496","27648","4096"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","8","256","3504","26944","128096","389376","754752","902400","623616","225280","32768"],["0","0","0","8","384","6576","58432","307296","1005312","2057280","2558208","1815552","667648","98304"],["0","0","0","-24","-384","-1296","13632","153312","679680","1643328","2260224","1704960","651264","98304"],["0","0","0","-40","-896","-8304","-40256","-102880","-99072","133824","455424","457728","200704","32768"],["0","0","0","-16","-384","-3936","-22400","-76992","-162816","-206976","-148992","-55296","-8192","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-8","-248","-3376","-26512","-132640","-440480","-981312","-1450176","-1377024","-793600","-249856","-32768"],["0","0","0","0","-48","-1248","-14112","-90816","-365376","-950400","-1597824","-1688832","-1059840","-356352","-49152"],["0","0","0","24","648","7632","51312","216288","590688","1043136","1154880","753408","261120","36864","0"],["0","0","0","16","448","5504","38912","174464","515584","1012224","1302528","1065216","527360","143360","16384"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","-4","-128","-1824","-15232","-82528","-303360","-768640","-1337856","-1568832","-1197056","-563200","-147456","-16384"],["0","0","0","-8","-256","-3648","-30464","-165056","-606720","-1537280","-2675712","-3137664","-2394112","-1126400","-294912","-32768"],["0","0","0","-4","-128","-1824","-15232","-82528","-303360","-768640","-1337856","-1568832","-1197056","-563200","-147456","-16384"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","-8","-224","-2704","-18304","-75424","-190592","-275136","-162816","88320","183296","94208","16384"],["0","-24","-688","-8496","-58848","-248672","-648768","-988224","-695424","115968","494592","274432","49152"],["0","-24","-720","-9264","-66720","-293472","-802752","-1313856","-1109376","-182016","384000","258048","49152"],["0","-8","-272","-3856","-30112","-142624","-421568","-763584","-783744","-358656","17408","69632","16384"],["0","0","-16","-384","-3936","-22400","-76992","-162816","-206976","-148992","-55296","-8192","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","4","120","1576","11856","56016","170720","328160","356544","118656","-179968","-230400","-102400","-16384"],["0","8","256","3600","29216","150944","515904","1171904","1725312","1539840","705280","66560","-61440","-16384"],["0","4","152","2472","22864","133840","519648","1359328","2380992","2723712","1950464","824320","184320","16384"],["0","0","16","448","5504","38912","174464","515584","1012224","1302528","1065216","527360","143360","16384"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","-4","-128","-1824","-15232","-82528","-303360","-768640","-1337856","-1568832","-1197056","-563200","-147456","-16384"],["0","0","-8","-256","-3648","-30464","-165056","-606720","-1537280","-2675712","-3137664","-2394112","-1126400","-294912","-32768"],["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"],["2","4","-8"],["0","4","0"]]},"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}]},"quotient":[{"coeff":{"coeffs":[["0","-8","-140","-1080","-5064","-16416","-36368","-47840","-27232","1920","7680","2048"],["0","-40","-664","-4560","-17392","-43168","-76448","-87488","-40000","13056","17408","4096"],["0","-72","-1148","-7224","-22856","-39456","-41168","-27872","2720","20352","11776","2048"],["0","-56","-864","-5088","-13792","-15072","1536","15360","16512","9216","2048","0"],["0","-16","-240","-1344","-3264","-2368","2624","3584","1024","0","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","4","76","576","2168","4016","3024","2112","9504","15744","9728","2048"],["0","16","312","2496","10512","25088","35744","38144","44736","42752","21504","4096"],["0","20","412","3520","16120","42992","69648","74560","61984","38272","13824","2048"],["0","8","192","1856","9376","26784","44160","43136","27776","11264","2048","0"],["0","0","16","256","1600","4864","7232","4608","1024","0","0","0"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["0","0","0","8","192","1968","11200","38496","81408","103488","74496","27648","4096"],["0","0","0","24","576","5904","33600","115488","244224","310464","223488","82944","12288"],["0","0","0","24","576","5904","33600","115488","244224","310464","223488","82944","12288"],["0","0","0","8","192","1968","11200","38496","81408","103488","74496","27648","4096"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","8","224","2704","18304","75424","190592","275136","162816","-88320","-183296","-94208","-16384"],["0","0","0","24","688","8496","58848","248672","648768","988224","695424","-115968","-494592","-274432","-49152"],["0","0","0","24","720","9264","66720","293472","802752","1313856","1109376","182016","-384000","-258048","-49152"],["0","0","0","8","272","3856","30112","142624","421568","763584","783744","358656","-17408","-69632","-16384"],["0","0","0","0","16","384","3936","22400","76992","162816","206976","148992","55296","8192","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-4","-120","-1576","-11856","-56016","-170720","-328160","-356544","-118656","179968","230400","102400","16384"],["0","0","0","-8","-256","-3600","-29216","-150944","-515904","-1171904","-1725312","-1539840","-705280","-66560","61440","16384"],["0","0","0","-4","-152","-2472","-22864","-133840","-519648","-1359328","-2380992","-2723712","-1950464","-824320","-184320","-16384"],["0","0","0","0","-16","-448","-5504","-38912","-174464","-515584","-1012224","-1302528","-1065216","-527360","-143360","-16384"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","4","128","1824","15232","82528","303360","768640","1337856","1568832","1197056","563200","147456","16384"],["0","0","0","0","8","256","3648","30464","165056","606720","1537280","2675712","3137664","2394112","1126400","294912","32768"],["0","0","0","0","4","128","1824","15232","82528","303360","768640","1337856","1568832","1197056","563200","147456","16384"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","16","456","5664","40112","177792","509280","939648","1080384","725760","257024","36864"],["0","0","48","1384","17376","124272","555776","1604832","2981760","3448128","2326272","826368","118784"],["0","0","48","1416","18144","132144","600576","1758816","3307392","3862080","2624256","936960","135168"],["0","0","16","504","6816","51920","244992","740256","1428096","1701312","1172736","422912","61440"],["0","0","0","16","384","3936","22400","76992","162816","206976","148992","55296","8192"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","-8","-248","-3400","-27088","-138544","-474080","-1096800","-1694400","-1687488","-1017088","-332800","-45056","0"],["0","0","-16","-512","-7248","-59680","-316000","-1122624","-2709184","-4401024","-4677504","-3099392","-1192960","-233472","-16384"],["0","0","-8","-280","-4296","-38096","-216368","-823008","-2127968","-3718848","-4292544","-3147520","-1387520","-331776","-32768"],["0","0","0","-16","-448","-5504","-38912","-174464","-515584","-1012224","-1302528","-1065216","-527360","-143360","-16384"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","4","128","1824","15232","82528","303360","768640","1337856","1568832","1197056","563200","147456","16384"],["0","0","0","8","256","3648","30464","165056","606720","1537280","2675712","3137664","2394112","1126400","294912","32768"],["0","0","0","4","128","1824","15232","82528","303360","768640","1337856","1568832","1197056","563200","147456","16384"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["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 = 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"],["2","4"]],"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 = 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) + (4) x, V_n(x) = 0, W_n(x) = (1) + (4) 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) + (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 = 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"}