{"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"],["4","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["4","2"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"basis_map_A007318 of Triangle T(n, k) is coefficient of z^n*w^k in 1/(1 - 2*z - 2*w - 2*z*w) read by rows in order 00, 10, 01, 20, 11, 02, ..."},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["-72","-132","-120","-88","-32","-4"],["-60","-66","26","28","4","0"],["42","54","34","8","0","0"],["18","12","0","0","0","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-288","-876","-1164","-848","-328","-60","-4"],["-240","-546","-448","-190","-44","-4","0"],["6","-18","-8","2","0","0","0"],["18","12","0","0","0","0","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-216","-744","-1044","-760","-296","-56","-4"],["-180","-480","-474","-218","-48","-4","0"],["-36","-72","-42","-6","0","0","0"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["12","18","14","10","2"],["18","33","24","12","2"],["6","18","10","2","0"],["0","3","0","0","0"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["12","18","14","10","2"],["18","33","24","12","2"],["6","18","10","2","0"],["0","3","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"],["6","6","4","8","2"],["6","9","10","2","0"],["0","3","0","0","0"]]},"terms":[{"coeff":{"coeffs":[["-12","24","112","108","36","4"],["90","138","42","-12","-4","0"],["12","-18","-34","-8","0","0"],["-18","-12","0","0","0","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["72","336","612","548","248","52","4"],["108","336","390","206","48","4","0"],["36","72","42","6","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"],["4","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["4","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":[["-4","-2"],["1","2"],["-3","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-18","-24","-6"],["12","12","2"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-12","-24","-14","-2"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["1"],["1"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","1728","9504","23328","34560","35280","26280","14168","5216","1200","152","8"],["0","0","4320","24624","62208","93168","93384","66300","33560","11636","2552","312","16"],["0","0","3456","21168","56160","85392","83088","54636","24784","7636","1504","168","8"],["0","0","864","6480","19008","29520","27144","15492","5560","1228","152","8","0"],["0","0","0","432","1728","2736","2160","876","168","12","0","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","1728","9504","23328","34560","35280","26280","14168","5216","1200","152","8"],["0","0","4320","24624","62208","93168","93384","66300","33560","11636","2552","312","16"],["0","0","3456","21168","56160","85392","83088","54636","24784","7636","1504","168","8"],["0","0","864","6480","19008","29520","27144","15492","5560","1228","152","8","0"],["0","0","0","432","1728","2736","2160","876","168","12","0","0","0"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["0","0","0","1728","10368","26784","38880","34704","19584","6920","1464","168","8"],["0","0","0","5184","31104","80352","116640","104112","58752","20760","4392","504","24"],["0","0","0","5184","31104","80352","116640","104112","58752","20760","4392","504","24"],["0","0","0","1728","10368","26784","38880","34704","19584","6920","1464","168","8"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","3456","27648","95040","184896","224928","177984","92176","30608","6192","688","32"],["0","0","0","5184","51840","204768","438048","570672","475200","255768","87432","18072","2040","96"],["0","0","0","-5184","-10368","44064","204768","362448","357696","214248","78648","17064","1992","96"],["0","0","0","-12096","-65664","-146016","-165024","-87408","1728","29896","17432","4680","616","32"],["0","0","0","-5184","-31104","-80352","-116640","-104112","-58752","-20760","-4392","-504","-24","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-10368","-82944","-292032","-596160","-781920","-689472","-415344","-170160","-46256","-7920","-768","-32"],["0","0","0","0","-20736","-134784","-383616","-627264","-649728","-443232","-200544","-59088","-10800","-1104","-48"],["0","0","0","31104","207360","606528","1021248","1091232","768960","359568","109392","20592","2160","96","0"],["0","0","0","20736","145152","449280","808704","936576","729216","387456","139776","33424","5040","432","16"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","-20736","-165888","-594432","-1257984","-1745280","-1665792","-1116672","-527232","-173200","-38464","-5472","-448","-16"],["0","0","0","-41472","-331776","-1188864","-2515968","-3490560","-3331584","-2233344","-1054464","-346400","-76928","-10944","-896","-32"],["0","0","0","-20736","-165888","-594432","-1257984","-1745280","-1665792","-1116672","-527232","-173200","-38464","-5472","-448","-16"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","-10368","-72576","-219456","-373248","-387936","-247968","-89616","-11136","4048","1872","288","16"],["0","-31104","-222912","-689472","-1200096","-1280448","-848016","-327600","-54168","7752","5112","840","48"],["0","-31104","-233280","-751680","-1360800","-1513728","-1056240","-445104","-95688","-1032","4104","792","48"],["0","-10368","-88128","-312768","-614304","-737856","-560304","-265872","-73416","-9128","360","216","16"],["0","0","-5184","-31104","-80352","-116640","-104112","-58752","-20760","-4392","-504","-24","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","20736","155520","511488","965952","1149120","883872","427200","111888","3040","-7792","-2448","-320","-16"],["0","41472","331776","1168128","2381184","3106944","2704320","1583616","611232","145856","17840","144","-208","-16"],["0","20736","196992","801792","1864512","2766528","2757024","1885632","886800","282592","59056","7632","544","16"],["0","0","20736","145152","449280","808704","936576","729216","387456","139776","33424","5040","432","16"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","-20736","-165888","-594432","-1257984","-1745280","-1665792","-1116672","-527232","-173200","-38464","-5472","-448","-16"],["0","0","-41472","-331776","-1188864","-2515968","-3490560","-3331584","-2233344","-1054464","-346400","-76928","-10944","-896","-32"],["0","0","-20736","-165888","-594432","-1257984","-1745280","-1665792","-1116672","-527232","-173200","-38464","-5472","-448","-16"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["6","3","-2"],["0","3","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-12","-6","10","4"],["0","-12","-12","-2"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","12","24","14","2"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","-864","-4608","-10080","-10464","-2616","5776","7112","3744","1032","144","8"],["0","-3024","-13680","-24336","-17952","4188","20092","18244","8540","2208","296","16"],["0","-3888","-14832","-19440","-3936","17508","23564","15308","5860","1320","160","8"],["0","-2160","-7056","-6192","4128","11988","9956","4332","1076","144","8","0"],["0","-432","-1296","-1008","576","1284","708","156","12","0","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","1728","9504","23328","34560","35280","26280","14168","5216","1200","152","8"],["0","4320","24624","62208","93168","93384","66300","33560","11636","2552","312","16"],["0","3456","21168","56160","85392","83088","54636","24784","7636","1504","168","8"],["0","864","6480","19008","29520","27144","15492","5560","1228","152","8","0"],["0","0","432","1728","2736","2160","876","168","12","0","0","0"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["0","0","0","1728","10368","26784","38880","34704","19584","6920","1464","168","8"],["0","0","0","5184","31104","80352","116640","104112","58752","20760","4392","504","24"],["0","0","0","5184","31104","80352","116640","104112","58752","20760","4392","504","24"],["0","0","0","1728","10368","26784","38880","34704","19584","6920","1464","168","8"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","10368","72576","219456","373248","387936","247968","89616","11136","-4048","-1872","-288","-16"],["0","0","0","31104","222912","689472","1200096","1280448","848016","327600","54168","-7752","-5112","-840","-48"],["0","0","0","31104","233280","751680","1360800","1513728","1056240","445104","95688","1032","-4104","-792","-48"],["0","0","0","10368","88128","312768","614304","737856","560304","265872","73416","9128","-360","-216","-16"],["0","0","0","0","5184","31104","80352","116640","104112","58752","20760","4392","504","24","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-20736","-155520","-511488","-965952","-1149120","-883872","-427200","-111888","-3040","7792","2448","320","16"],["0","0","0","-41472","-331776","-1168128","-2381184","-3106944","-2704320","-1583616","-611232","-145856","-17840","-144","208","16"],["0","0","0","-20736","-196992","-801792","-1864512","-2766528","-2757024","-1885632","-886800","-282592","-59056","-7632","-544","-16"],["0","0","0","0","-20736","-145152","-449280","-808704","-936576","-729216","-387456","-139776","-33424","-5040","-432","-16"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","20736","165888","594432","1257984","1745280","1665792","1116672","527232","173200","38464","5472","448","16"],["0","0","0","0","41472","331776","1188864","2515968","3490560","3331584","2233344","1054464","346400","76928","10944","896","32"],["0","0","0","0","20736","165888","594432","1257984","1745280","1665792","1116672","527232","173200","38464","5472","448","16"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","20736","148608","466560","841536","960768","720864","357216","114448","22512","2448","112"],["0","0","62208","451008","1430784","2604960","2998944","2266704","1130400","364104","71928","7848","360"],["0","0","62208","461376","1492992","2765664","3232224","2474928","1247904","405624","80712","8856","408"],["0","0","20736","164160","559872","1082592","1310688","1033200","533472","176728","35688","3960","184"],["0","0","0","5184","31104","80352","116640","104112","58752","20760","4392","504","24"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","-41472","-321408","-1105920","-2223936","-2894400","-2549664","-1543872","-639120","-176240","-30672","-3024","-128","0"],["0","0","-82944","-663552","-2356992","-4897152","-6597504","-6035904","-3816960","-1665696","-492256","-94768","-11088","-688","-16"],["0","0","-41472","-362880","-1396224","-3122496","-4511808","-4422816","-3002304","-1414032","-455792","-97520","-13104","-992","-32"],["0","0","0","-20736","-145152","-449280","-808704","-936576","-729216","-387456","-139776","-33424","-5040","-432","-16"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","20736","165888","594432","1257984","1745280","1665792","1116672","527232","173200","38464","5472","448","16"],["0","0","0","41472","331776","1188864","2515968","3490560","3331584","2233344","1054464","346400","76928","10944","896","32"],["0","0","0","20736","165888","594432","1257984","1745280","1665792","1116672","527232","173200","38464","5472","448","16"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["0","0","144","576","912","720","292","56","4"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-2","-2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-4","-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 = 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"],["4","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["4","2"]]},"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) = (4) + (2) x, V_n(x) = 0, W_n(x) = (2) + (2) x; open hypotheses: multipliers_vanish_at_zero: [x^0] c_2(n, x) = 2 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 = 2 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 = 2 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) = (4) + (2) x, B_n(x) = (2) + (2) 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) = (4) + (2) x, B_n(x) = (2) + (2) 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"}