{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"a":"1","b":"0","c":"1","e":"1","schedule":{"first_degree":0,"first_index":0,"step":1},"shape":"mobius"},"parent":{"first_index":0,"initial_polynomials":[["1"],["4","6"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","4"]]},"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 Triangular array: row n gives the coefficients of the polynomial p(n,x) defined in Comments."},"identifying_rows":2,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["0","0","0","0","0","0"],["-4","20","-40","40","-20","4"],["-3","15","-30","30","-15","3"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-3","6","11","-40","35","-2","-11","4"],["6","-18","2","50","-70","34","-2","-2"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-3","3","17","-27","-15","53","-33","3","2"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["0","0","0","0","0","0"],["1","-5","10","-10","5","-1"]]},"deriv_order":0,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0,1],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["1"],["4","10"]],"recurrence":{"denominator":{"coeffs":[["-1","-3","-3","-1"],["1","3","3","1"]]},"terms":[{"coeff":{"coeffs":[["14","122","410","698","644","308","60"],["-26","-206","-656","-1082","-980","-464","-90"],["12","84","246","384","336","156","30"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["21","207","838","1822","2313","1723","700","120"],["-12","-114","-448","-952","-1188","-874","-352","-60"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["3","36","181","500","835","868","551","196","30"]]},"deriv_order":2,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":1,"multiplier":["1"],"operator":{"a":"1","b":"0","c":"1","e":"1","schedule":{"first_degree":0,"first_index":0,"step":1},"shape":"mobius"},"parent":{"first_index":0,"initial_polynomials":[["1"],["4","6"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","4"]]},"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":[["-4","-6"],["-3","-9"],["0","-3"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["3","9","4","-2"],["0","6","12","2"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-3","-12","-13","-2"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0"],["-3","3","17","-27","-15","53","-33","3","2","0"],["0","3","-3","-17","27","15","-53","33","-3","-2"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["-27","-324","-1647","-4590","-7569","-7416","-4105","-1158","-156","-8","0","0","0"],["0","81","972","4941","13770","22707","22248","12315","3474","468","24","0","0"],["0","0","-81","-972","-4941","-13770","-22707","-22248","-12315","-3474","-468","-24","0"],["0","0","0","27","324","1647","4590","7569","7416","4105","1158","156","8"]]},"step_quotients":[[{"coeff":{"coeffs":[["135","2052","13419","49302","111285","158184","139181","71470","19308","2536","128","0","0","0"],["81","972","3645","-1782","-56349","-198072","-350997","-352494","-196572","-55560","-7488","-384","0","0"],["0","-162","-2754","-18306","-61398","-104058","-51246","116202","225870","161364","50856","7248","384","0"],["0","0","0","1080","12528","60696","157248","229320","175536","45544","-19360","-12288","-2176","-128"],["0","0","0","162","1539","5022","2835","-23436","-69039","-86610","-54627","-16434","-2292","-120"],["0","0","0","0","-81","-972","-4941","-13770","-22707","-22248","-12315","-3474","-468","-24"]]},"deriv_order":0},{"coeff":{"coeffs":[["-81","-1377","-10233","-43659","-117909","-209223","-244659","-183705","-83518","-20892","-2616","-128","0","0","0","0"],["0","81","1863","16875","83025","249939","483165","605217","480075","227512","58440","7440","368","0","0","0"],["0","0","243","2673","10773","12879","-42363","-194157","-347697","-337995","-181428","-49968","-6624","-336","0","0"],["0","0","0","-405","-5427","-31239","-100197","-193455","-224289","-141621","-29415","14392","8184","1392","80","0"],["0","0","0","0","162","2268","13824","47952","103788","144504","128760","71040","23042","4236","408","16"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","81","1296","9180","37800","99846","176040","208884","164280","82561","25160","4440","416","16","0","0","0"],["0","0","-243","-3888","-27540","-113400","-299538","-528120","-626652","-492840","-247683","-75480","-13320","-1248","-48","0","0"],["0","0","0","243","3888","27540","113400","299538","528120","626652","492840","247683","75480","13320","1248","48","0"],["0","0","0","0","-81","-1296","-9180","-37800","-99846","-176040","-208884","-164280","-82561","-25160","-4440","-416","-16"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","-135","-1566","-7587","-19656","-28665","-21942","-5693","2420","1536","272","16","0"],["0","0","-81","-351","2457","23463","79569","142659","143115","76109","17956","1248","-128","-16"],["0","0","0","486","5346","23814","52974","53622","-2754","-59598","-53046","-18036","-2664","-144"],["0","0","0","81","567","81","-10935","-46143","-91287","-98925","-58101","-16902","-2316","-120"],["0","0","0","0","-81","-972","-4941","-13770","-22707","-22248","-12315","-3474","-468","-24"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","81","1053","5859","18063","33183","35775","19425","957","-4268","-1824","-288","-16","0","0"],["0","0","81","810","2538","-1566","-32184","-97902","-151674","-132090","-61433","-12388","-384","176","16","0"],["0","0","0","-243","-3159","-17415","-52245","-89667","-79785","-12861","41625","37434","12420","1800","96","0"],["0","0","0","0","162","2268","13824","47952","103788","144504","128760","71040","23042","4236","408","16"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","-81","-1296","-9180","-37800","-99846","-176040","-208884","-164280","-82561","-25160","-4440","-416","-16","0","0"],["0","0","0","162","2592","18360","75600","199692","352080","417768","328560","165122","50320","8880","832","32","0"],["0","0","0","0","-81","-1296","-9180","-37800","-99846","-176040","-208884","-164280","-82561","-25160","-4440","-416","-16"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0"],["0","6"],["0","9"],["0","3"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-3","-9","-4","0"],["3","3","-2","2"],["0","-6","-12","-2"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-3","-12","-13","-2","0"],["0","3","12","13","2"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["-3","3","17","-27","-15","53","-33","3","2","0"],["0","3","-3","-17","27","15","-53","33","-3","-2"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["-27","-324","-1647","-4590","-7569","-7416","-4105","-1158","-156","-8","0","0","0"],["0","81","972","4941","13770","22707","22248","12315","3474","468","24","0","0"],["0","0","-81","-972","-4941","-13770","-22707","-22248","-12315","-3474","-468","-24","0"],["0","0","0","27","324","1647","4590","7569","7416","4105","1158","156","8"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","-486","-5832","-29646","-82620","-136242","-133488","-73890","-20844","-2808","-144","0","0","0"],["0","-891","-9234","-36855","-62532","-1917","163998","264999","183456","57384","8160","432","0","0"],["0","-486","-3159","972","62937","229230","367983","251568","-14913","-109836","-47232","-7632","-432","0"],["0","-81","486","9882","43578","67932","-38286","-278562","-379746","-210843","-32352","5832","2016","144"],["0","0","243","1458","-1782","-36936","-125388","-190512","-113742","33480","74337","29862","4716","264"],["0","0","0","-243","-2430","-8991","-11664","14499","69498","96543","63468","19440","2736","144"],["0","0","0","0","81","972","4941","13770","22707","22248","12315","3474","468","24"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","324","4374","25596","84726","173448","225234","182748","87786","22716","2904","144","0","0","0","0"],["-81","-729","-2295","-3591","-14715","-85671","-259941","-434277","-416728","-223660","-61704","-8192","-416","0","0","0"],["0","405","4455","18765","32481","-5643","-106839","-132105","22467","176738","148500","49224","7168","384","0","0"],["0","0","-729","-8991","-45765","-119637","-150741","-12717","221481","285921","142674","18600","-4608","-1392","-96","0"],["0","0","0","567","7533","42795","134325","249291","265005","125877","-28305","-62390","-26990","-5220","-472","-16"],["0","0","0","0","-162","-2268","-13824","-47952","-103788","-144504","-128760","-71040","-23042","-4236","-408","-16"]]},"deriv_order":1},{"coeff":{"coeffs":[["81","1215","7884","28620","62046","76194","32844","-44604","-81719","-57401","-20720","-4024","-400","-16","0","0","0"],["0","-324","-4941","-32832","-123660","-285984","-404622","-307416","-30468","162596","147043","57720","11656","1184","48","0","0"],["0","0","486","7533","51192","199260","485676","756702","725184","359028","2526","-96723","-48840","-10824","-1152","-48","0"],["0","0","0","-324","-5103","-35424","-142020","-361584","-604314","-659496","-448236","-165964","-18079","7400","2776","352","16"],["0","0","0","0","81","1296","9180","37800","99846","176040","208884","164280","82561","25160","4440","416","16"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["135","1782","10422","35694","79560","120510","123962","82026","29841","3188","-864","-240","-16","0"],["81","810","3294","6615","3294","-23085","-87918","-165039","-176083","-100597","-26020","-2432","64","16"],["0","-162","-1620","-7398","-24030","-68850","-156114","-228246","-176802","-37348","31918","17460","3016","176"],["0","0","162","1161","1431","-8883","-30051","-14355","74481","147463","111029","36054","5228","280"],["0","0","0","-162","-1458","-4050","2106","37206","91746","108858","66942","19908","2760","144"],["0","0","0","0","81","972","4941","13770","22707","22248","12315","3474","468","24"]]},"deriv_order":0},{"coeff":{"coeffs":[["-81","-1215","-8208","-32994","-87642","-160920","-206292","-180630","-101029","-30385","-1996","1120","256","16","0","0"],["0","243","3240","19035","65637","151011","253179","328221","328719","234822","103633","22708","1680","-112","-16","0"],["0","0","-405","-5022","-25974","-71064","-105084","-68256","9714","22296","-25319","-37786","-14676","-2296","-128","0"],["0","0","0","405","5265","28971","86373","145503","120501","-2883","-99345","-85432","-31226","-5628","-488","-16"],["0","0","0","0","-162","-2268","-13824","-47952","-103788","-144504","-128760","-71040","-23042","-4236","-408","-16"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","-81","-1215","-7884","-28620","-62046","-76194","-32844","44604","81719","57401","20720","4024","400","16","0","0"],["0","0","243","3726","24948","95040","223938","328428","274572","75072","-80877","-89642","-37000","-7632","-784","-32","0"],["0","0","0","-243","-3807","-26244","-104220","-261738","-428274","-450612","-283956","-83403","7081","11840","3192","368","16"],["0","0","0","0","81","1296","9180","37800","99846","176040","208884","164280","82561","25160","4440","416","16"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["-3","-12","-13","-2","0"],["0","3","12","13","2"]]},"start_base":1}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-2","-4"]]},"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 = ((1) x + (1))^(d_n) P(((1) x + (0))/((1) x + (1))), d_n = 0 + 1 (n - 0); so the candidate rows satisfy the input rule at every base n >= 1 (the exceptional bases checked exactly), and agreement on the 2 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.splits_fPolynomial"],"lean_route":"fTransform","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":"((1) x + (1))^(d_n) P(((1) x + (0))/((1) x + (1))), d_n = 0 + 1 (n - 0)","kind":"preserver_image","operator":{"a":"1","b":"0","c":"1","e":"1","schedule":{"first_degree":0,"first_index":0,"step":1},"shape":"mobius"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["4","6"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","4"]]},"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 = ((1) x + (1))^(d_n) P(((1) x + (0))/((1) x + (1))), 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 [-1, 0]","input_root_region":{"lower":{"closed":true,"value":"-1"},"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) = (2) + (4) 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) = (2) + (2) x, B_n(x) = (2) + (4) 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) = (2) + (4) 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 = ((1) x + (1))^(d_n) P(((1) x + (0))/((1) x + (1))), 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 [-1, 0]"},"kind":"preserver_image"}