{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"intercept":"1","shape":"affine","slope":"1"},"parent":{"first_index":0,"initial_polynomials":[["1"],["1"]],"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 Square array A(n,r), the number of neighbors at a sharp Manhattan distance r in a finite n-hypercube lattice, read by upwards antidiagonals; A(n,r) = Sum_{k=0..min(n,r)} binomial(r-1,k-1)*binomial(n,k)* 2^k."},"identifying_rows":3,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["1"],["1"],["-2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-6","-15","-6"],["4","8","2"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-2","-8","-9","-2"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["-1"],["1"]]},"deriv_order":0,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0,1,2],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["1"],["1"],["7","4"]],"recurrence":{"denominator":{"coeffs":[["-2"],["1"]]},"terms":[{"coeff":{"coeffs":[["2"],["-5"],["2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["41","39","8"],["-14","-12","-2"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["21","32","15","2"]]},"deriv_order":2,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":2,"multiplier":["1"],"operator":{"intercept":"1","shape":"affine","slope":"1"},"parent":{"first_index":0,"initial_polynomials":[["1"],["1"]],"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":[["-1","0"],["-2","-2"],["0","-2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["2","2","-6","-4"],["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":[["2","10","17","11","2"],["-2","-12","-25","-20","-4"],["0","2","8","9","2"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["-8","-120","-804","-3172","-8178","-14454","-17867","-15471","-9249","-3695","-930","-132","-8"],["0","24","336","2076","7440","17094","26268","27333","19080","8667","2418","372","24"],["0","0","-24","-312","-1764","-5676","-11418","-14850","-12483","-6597","-2070","-348","-24"],["0","0","0","8","96","492","1400","2406","2544","1617","582","108","8"]]},"step_quotients":[[{"coeff":{"coeffs":[["8","136","1044","4780","14522","30810","46775","51205","40191","22193","8320","1992","272","16"],["16","264","1944","8420","23796","46002","62002","58275","37578","16057","4278","636","40","0"],["0","-32","-552","-4200","-18604","-53268","-103422","-138854","-129033","-81753","-34184","-8904","-1296","-80"],["0","0","0","88","1136","6372","20320","40466","52044","43227","22572","7008","1168","80"],["0","0","0","32","384","1968","5600","9624","10176","6468","2328","432","32","0"],["0","0","0","0","-16","-192","-984","-2800","-4812","-5088","-3234","-1164","-216","-16"]]},"deriv_order":0},{"coeff":{"coeffs":[["-16","-288","-2344","-11392","-36756","-82712","-132470","-150696","-118150","-58092","-11586","5264","4722","1548","248","16"],["0","16","272","2024","8600","22612","36244","28126","-13222","-62554","-79382","-57352","-25576","-6896","-1024","-64"],["0","0","48","768","5592","24528","72252","150672","228114","252564","202986","115824","45084","11208","1584","96"],["0","0","0","-80","-1200","-8024","-31512","-80604","-140756","-171058","-144810","-84168","-32552","-7920","-1088","-64"],["0","0","0","0","32","448","2752","9728","21808","32224","31632","20352","8322","2060","280","16"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","16","304","2640","13872","49208","124488","231312","320320","331977","256355","145603","59457","16832","3112","336","16"],["0","0","-48","-864","-7056","-34560","-113064","-260400","-433536","-527424","-468507","-300558","-136251","-42120","-8376","-960","-48"],["0","0","0","48","816","6240","28320","84744","175656","257880","269544","198963","101595","34656","7464","912","48"],["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","-120","-796","-3068","-7590","-12562","-14061","-10521","-5088","-1496","-240","-16"],["0","0","-16","-216","-1272","-4276","-9012","-12306","-10866","-6015","-1962","-340","-24","0"],["0","0","0","48","624","3528","11352","22836","29700","24966","13194","4140","696","48"],["0","0","0","16","176","792","1816","2012","276","-1854","-2070","-948","-200","-16"],["0","0","0","0","-16","-192","-984","-2800","-4812","-5088","-3234","-1164","-216","-16"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-8","-120","-812","-3276","-8766","-16346","-21673","-20421","-13410","-5894","-1620","-248","-16"],["0","0","16","256","1872","8288","24784","52800","82228","94344","79179","47512","19534","5124","760","48"],["0","0","0","-48","-720","-4824","-19032","-49068","-86724","-107202","-92826","-55494","-22170","-5580","-792","-48"],["0","0","0","0","32","448","2752","9728","21808","32224","31632","20352","8322","2060","280","16"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","-16","-288","-2352","-11520","-37688","-86800","-144512","-175808","-156169","-100186","-45417","-14040","-2792","-320","-16"],["0","0","0","32","544","4160","18880","56496","117104","171920","179696","132642","67730","23104","4976","608","32"],["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","-2"],["0","0"],["0","2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-4","-13","-12","-4"],["2","10","16","6"],["0","-4","-8","-2"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-2","-10","-17","-11","-2"],["0","2","8","9","2"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["-2","-10","-17","-11","-2"],["0","2","8","9","2"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["-8","-120","-804","-3172","-8178","-14454","-17867","-15471","-9249","-3695","-930","-132","-8"],["0","24","336","2076","7440","17094","26268","27333","19080","8667","2418","372","24"],["0","0","-24","-312","-1764","-5676","-11418","-14850","-12483","-6597","-2070","-348","-24"],["0","0","0","8","96","492","1400","2406","2544","1617","582","108","8"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","-32","-480","-3216","-12688","-32712","-57816","-71468","-61884","-36996","-14780","-3720","-528","-32"],["0","-48","-624","-3480","-10728","-19308","-18348","-2130","16506","20826","12498","4092","696","48"],["0","-16","-96","312","4864","21228","50952","76202","73656","46050","18224","4368","576","32"],["0","0","48","528","2312","4680","2100","-10372","-24810","-26562","-15780","-5256","-912","-64"],["0","0","0","-48","-576","-2952","-8400","-14436","-15264","-9702","-3492","-648","-48","0"],["0","0","0","0","16","192","984","2800","4812","5088","3234","1164","216","16"]]},"deriv_order":0},{"coeff":{"coeffs":[["16","296","2480","12452","41776","98842","169624","213827","198263","134017","64721","21554","4660","584","32","0"],["-16","-304","-2688","-14568","-53696","-141444","-272940","-389950","-412911","-321848","-182017","-72960","-19994","-3532","-360","-16"],["0","80","1312","9808","44248","134384","290084","457868","535330","464503","296801","137092","44248","9392","1168","64"],["0","0","-144","-2224","-15440","-63656","-173488","-329348","-447212","-439182","-311667","-157728","-55204","-12584","-1664","-96"],["0","0","0","112","1648","10776","41240","102412","172980","202690","165162","92490","34612","8200","1104","64"],["0","0","0","0","-32","-448","-2752","-9728","-21808","-32224","-31632","-20352","-8322","-2060","-280","-16"]]},"deriv_order":1},{"coeff":{"coeffs":[["16","304","2640","13872","49208","124488","231312","320320","331977","256355","145603","59457","16832","3112","336","16","0"],["0","-64","-1168","-9696","-48432","-162272","-384888","-664848","-847744","-800484","-556913","-281854","-101577","-25208","-4072","-384","-16"],["0","0","96","1680","13296","62880","197808","436056","691416","796968","667470","402153","170907","49584","9288","1008","48"],["0","0","0","-64","-1072","-8064","-35936","-105376","-213576","-305920","-311352","-223476","-110947","-36856","-7752","-928","-48"],["0","0","0","0","16","256","1824","7616","20632","37920","48040","41808","24513","9352","2200","288","16"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["8","120","796","3068","7590","12562","14061","10521","5088","1496","240","16","0","0"],["16","232","1512","5900","15564","29838","43558","49361","42804","27160","11812","3240","496","32"],["0","-32","-424","-2472","-8380","-18484","-28374","-32006","-27669","-18369","-8786","-2692","-456","-32"],["0","0","32","360","1648","3740","3456","-2642","-10788","-12699","-7782","-2620","-456","-32"],["0","0","0","-32","-368","-1776","-4616","-6824","-5364","-1380","906","732","184","16"],["0","0","0","0","16","192","984","2800","4812","5088","3234","1164","216","16"]]},"deriv_order":0},{"coeff":{"coeffs":[["-16","-288","-2360","-11640","-38500","-90076","-153278","-192154","-177842","-120607","-58827","-19934","-4412","-568","-32","0"],["0","48","800","6040","27288","82092","173180","262914","290386","233494","135663","56048","15994","2988","328","16"],["0","0","-80","-1232","-8520","-34936","-94484","-177444","-237470","-228978","-159186","-79034","-27314","-6204","-824","-48"],["0","0","0","80","1168","7576","28760","70876","118948","138834","113178","63816","24230","5860","808","48"],["0","0","0","0","-32","-448","-2752","-9728","-21808","-32224","-31632","-20352","-8322","-2060","-280","-16"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","-16","-288","-2352","-11520","-37688","-86800","-144512","-175808","-156169","-100186","-45417","-14040","-2792","-320","-16","0"],["0","0","48","832","6512","30400","94184","203904","316432","355504","288811","167916","68521","19016","3400","352","16"],["0","0","0","-48","-800","-5984","-26496","-77128","-155024","-219960","-221504","-157155","-77082","-25304","-5264","-624","-32"],["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","-10","-17","-11","-2"],["0","2","8","9","2"]]},"start_base":2}},"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 = P((1) x + (1)); 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":["Polynomial.Splits.comp_of_degree_le_one"],"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":"no parent theorem report with an interlacing conclusion","status":"not_proved"},"lean_replay":"not_attempted","operation":{"description":"P((1) x + (1))","kind":"preserver_image","operator":{"intercept":"1","shape":"affine","slope":"1"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["1"]],"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 = P((1) x + (1)), 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, -1]","input_root_region":{"upper":{"closed":true,"value":"-1"}},"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: seed_degree_step: degrees 0 and 0 (exact); seed_strict_interlacing: the Bezout test fails or the degrees do not differ by one (exact); 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 = P((1) x + (1)) 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, -1]"},"kind":"preserver_image"}