{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"coefficients":[{"denominator":["1"],"numerator":["0"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["3"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-1","1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"Triangle of coefficients of polynomials v(n,x) jointly generated with A208508; see the Formula section."},"identifying_rows":3,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["2","-2","2"],["6","-15","1"],["4","3","-1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0","-2","2"],["0","8","-10","2"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["-2","-2"],["6","1"],["-4","1"]]},"deriv_order":1,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0,1,2],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["0"],["0"],["1"]],"recurrence":{"denominator":{"coeffs":[["-12","-2"],["14","-1"],["-4","1"]]},"terms":[{"coeff":{"coeffs":[["0","-16","0"],["2","21","-3"],["-4","-3","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","8","-8","0"],["0","-8","10","-2"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":2,"multiplier":["1"],"operator":{"coefficients":[{"denominator":["1"],"numerator":["0"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["3"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-1","1"]]},"deriv_order":0,"offset":2,"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":[["-36","0","0"],["32","-12","1"],["-16","8","-1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["96","-192","66","-6"],["0","64","-32","4"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","64","-96","36","-4"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["12"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","-128","384","-256","-256","384","-128"],["0","0","-128","-320","1792","-2176","896","-64"],["0","0","768","-2880","3360","-1056","-288","96"],["0","0","512","0","-2144","2320","-768","80"],["0","0","-1024","2816","-2752","1168","-224","16"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["0","0","0","884736","-5308416","13271040","-17694720","13271040","-5308416","884736"],["0","0","0","5308416","-27869184","59719680","-66355200","39813120","-11943936","1327104"],["0","0","0","10616832","-47775744","85598208","-76972032","35831808","-7962624","663552"],["0","0","0","7077888","-26542080","38486016","-27095040","9621504","-1658880","110592"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","294912","-2064384","6193152","-10321920","10321920","-6193152","2064384","-294912","0"],["0","0","0","1769472","-10764288","27353088","-37158912","28385280","-11354112","1548288","294912","-73728"],["0","0","0","2359296","-10027008","13418496","921600","-20090880","21602304","-10248192","2248704","-184320"],["0","0","0","-4718592","33030144","-93782016","141262848","-122849280","62595072","-18100224","2727936","-165888"],["0","0","0","-14155776","73138176","-156303360","178716672","-118462464","46384128","-10533888","1281024","-64512"],["0","0","0","-9437184","40108032","-69599232","63995904","-34099200","10884096","-2055168","211968","-9216"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","7077888","-51904512","165298176","-298303488","333398016","-236371968","104251392","-26689536","3391488","-147456"],["0","0","0","42467328","-274857984","759398400","-1162469376","1068613632","-595795968","192282624","-31334400","1622016","73728"],["0","0","0","84934656","-467140608","1061683200","-1271365632","835743744","-269070336","12607488","16588800","-4313088","331776"],["0","0","0","56623104","-231211008","327942144","-116195328","-175251456","225810432","-113319936","29233152","-3833856","202752"],["0","0","0","0","37748736","-160432128","278396928","-255983616","136396800","-43536384","8220672","-847872","36864"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","4718592","-35389440","115900416","-216760320","253919232","-191987712","92897280","-27426816","4423680","-294912"],["0","0","0","0","28311552","-191102976","557383680","-917028864","931627008","-601178112","244187136","-59719680","7962624","-442368"],["0","0","0","0","56623104","-339738624","870580224","-1242169344","1079599104","-588570624","200392704","-41140224","4644864","-221184"],["0","0","0","0","37748736","-198180864","438829056","-534380544","392380416","-179933184","51757056","-9068544","884736","-36864"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","18874368","-113246208","290193408","-414056448","359866368","-196190208","66797568","-13713408","1548288","-73728"],["0","0","0","75497472","-410517504","937820160","-1165197312","850894848","-367718400","89358336","-10395648","221184","36864"],["0","0","0","84934656","-410517504","810418176","-835190784","473665536","-139290624","14155776","2543616","-774144","55296"],["0","0","0","37748736","-169869312","318504960","-325582848","200392704","-77635584","19104768","-2903040","248832","-9216"],["0","0","0","37748736","-169869312","318504960","-325582848","200392704","-77635584","19104768","-2903040","248832","-9216"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-56623104","377487360","-1111228416","1903951872","-2105008128","1569521664","-797368320","270729216","-58171392","7077888","-368640"],["0","0","0","-226492416","1358954496","-3538944000","5251792896","-4905861120","3008987136","-1226465280","328237056","-55296000","5308416","-221184"],["0","0","0","-226492416","1132462080","-2335703040","2548039680","-1552711680","491028480","-40642560","-23224320","8294400","-1105920","55296"],["0","0","0","0","-150994944","679477248","-1274019840","1302331392","-801570816","310542336","-76419072","11612160","-995328","36864"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","-37748736","264241152","-806879232","1408499712","-1547845632","1112113152","-525975552","161021952","-30523392","3244032","-147456"],["0","0","0","0","-150994944","943718400","-2548039680","3892838400","-3707043840","2289254400","-926760960","243302400","-39813120","3686400","-147456"],["0","0","0","0","-150994944","830472192","-1953497088","2576351232","-2103902208","1112113152","-386961408","88031232","-12607488","1032192","-36864"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0"],["-2","-2"],["6","1"],["-4","1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["12","-24","12"],["24","-34","-2"],["0","16","-4"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","8","-16","8"],["0","16","-20","4"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","0","-256","384","448","-1088","576","-64"],["0","0","1024","-4480","6432","-3520","544","0"],["0","0","2560","-5632","3360","-16","-320","48"],["0","0","-1024","2816","-2752","1168","-224","16"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","1024","-2560","1088","1920","-2048","640","-64"],["0","0","-1024","6656","-12352","9088","-2624","256","0"],["0","0","-4096","8192","-2560","-3584","2608","-608","48"],["0","0","4096","-12288","13824","-7424","2064","-288","16"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["0","0","0","884736","-5308416","13271040","-17694720","13271040","-5308416","884736"],["0","0","0","5308416","-27869184","59719680","-66355200","39813120","-11943936","1327104"],["0","0","0","10616832","-47775744","85598208","-76972032","35831808","-7962624","663552"],["0","0","0","7077888","-26542080","38486016","-27095040","9621504","-1658880","110592"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","-147456","1105920","-3538944","6266880","-6635520","4202496","-1474560","221184"],["0","0","0","-1327104","8921088","-25325568","39260160","-35758080","19021824","-5419008","626688"],["0","0","0","-4718592","28164096","-70225920","94316544","-73138176","32403456","-7483392","681984"],["0","0","0","-8257536","43352064","-94003200","108251136","-70751232","25906176","-4856832","359424"],["0","0","0","-7077888","32440320","-60604416","59166720","-32200704","9676800","-1492992","92160"],["0","0","0","-2359296","9437184","-15040512","12238848","-5465088","1354752","-175104","9216"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","2654208","-19021824","58834944","-102187008","108380160","-71221248","27869184","-5750784","442368"],["0","0","0","17694720","-112951296","306044928","-455196672","399974400","-206438400","57286656","-6340608","-73728"],["0","0","0","42467328","-235929600","541605888","-654372864","432599040","-139419648","7741440","6377472","-1069056"],["0","0","0","42467328","-194641920","343277568","-268738560","47720448","65249280","-45453312","11059200","-940032"],["0","0","0","14155776","-40108032","8257536","91570176","-139474944","91090944","-30081024","4902912","-313344"],["0","0","0","0","9437184","-37748736","60162048","-48955392","21860352","-5419008","700416","-36864"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","1769472","-13271040","43352064","-80510976","92897280","-68124672","30965760","-7962624","884736"],["0","0","0","0","11796480","-80216064","235192320","-387219456","390021120","-244776960","92749824","-19169280","1622016"],["0","0","0","0","28311552","-173408256","452984832","-655810560","571760640","-304791552","95993856","-16146432","1105920"],["0","0","0","0","28311552","-155713536","360972288","-457408512","343609344","-155271168","40919040","-5750784","331776"],["0","0","0","0","9437184","-47185920","97910784","-109117440","70815744","-27279360","6119424","-737280","36864"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","7962624","-47333376","118996992","-163897344","133816320","-65470464","18579456","-2875392","221184"],["0","0","0","38338560","-208945152","475398144","-581640192","409595904","-163823616","33693696","-2580480","-36864"],["0","0","0","61341696","-304939008","621379584","-663146496","390408192","-120029184","14561280","626688","-202752"],["0","0","0","42467328","-194641920","361857024","-348364800","183582720","-51287040","6552576","-138240","-27648"],["0","0","0","23592960","-103809024","188153856","-182550528","103606272","-35407872","7170048","-792576","36864"],["0","0","0","9437184","-40108032","69599232","-63995904","34099200","-10884096","2055168","-211968","9216"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-21233664","138018816","-393265152","647405568","-683458560","484614144","-233127936","73654272","-13713408","1105920"],["0","0","0","-99090432","586285056","-1499037696","2174607360","-1978122240","1177288704","-462127104","115826688","-16662528","1032192"],["0","0","0","-141557760","736100352","-1606680576","1913683968","-1357074432","588847104","-155271168","23777280","-1880064","55296"],["0","0","0","-56623104","212336640","-261881856","33619968","213000192","-220575744","102297600","-25214976","3207168","-165888"],["0","0","0","0","-37748736","160432128","-278396928","255983616","-136396800","43536384","-8220672","847872","-36864"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","-14155776","99090432","-301694976","522436608","-564461568","392380416","-174292992","47333376","-7077888","442368"],["0","0","0","0","-66060288","417595392","-1137770496","1745141760","-1651359744","993558528","-377782272","87146496","-11059200","589824"],["0","0","0","0","-94371840","537919488","-1309409280","1776549888","-1471979520","768503808","-252149760","50208768","-5529600","258048"],["0","0","0","0","-37748736","198180864","-438829056","534380544","-392380416","179933184","-51757056","9068544","-884736","36864"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["0","0","768","-3072","4608","-3072","768"],["0","0","3072","-9984","11520","-5376","768"],["0","0","3072","-7680","6336","-1920","192"]]},"start_base":2}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["1","-1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-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) D; so the candidate rows satisfy the input rule at every base n >= 2 (the exceptional bases checked exactly), and agreement on the 3 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 [0, 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) D","kind":"preserver_image","operator":{"coefficients":[{"denominator":["1"],"numerator":["0"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["3"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-1","1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"relation":"Q_n = lambda(n) T_n(P_(n+0)) with T = phi(n, D) = (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), 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); degree_step_positive: fails at n = 2: lambda_n = 0 = 0 there (exact); multipliers_vanish_at_zero: [x^0] c_2(n, x) = -1 is not the zero polynomial","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), B_n(x) = (-1) + (1) x: every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0) (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), B_n(x) = (-1) + (1) x","every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0) (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) 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"}