{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"intercept":"0","shape":"affine","slope":"1"},"parent":{"first_index":0,"initial_polynomials":[["1"],["4","3"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","1"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"existing definition"},"identifying_rows":2,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["0"],["-4"],["-3"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-6","-9","-2"],["12","12","1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-12","-24","-13","-1"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["0"],["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","3"]],"recurrence":{"denominator":{"coeffs":[["-1"],["1"]]},"terms":[{"coeff":{"coeffs":[["-1"],["-2"],["3"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["18","21","3"],["-12","-12","-1"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["12","24","13","1"]]},"deriv_order":2,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":1,"multiplier":["1"],"operator":{"intercept":"0","shape":"affine","slope":"1"},"parent":{"first_index":0,"initial_polynomials":[["1"],["4","3"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","1"]]},"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":[["-8","-6"],["-6","-9"],["0","-3"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["12","18","4","-1"],["0","12","12","1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-12","-24","-13","-1"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["2"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","0"],["-24","-48","-26","-2","0"],["0","12","24","13","1"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["-110592","-663552","-1686528","-2350080","-1937664","-949248","-262720","-37056","-2496","-64","0","0","0"],["0","165888","995328","2529792","3525120","2906496","1423872","394080","55584","3744","96","0","0"],["0","0","-82944","-497664","-1264896","-1762560","-1453248","-711936","-197040","-27792","-1872","-48","0"],["0","0","0","13824","82944","210816","293760","242208","118656","32840","4632","312","8"]]},"step_quotients":[[{"coeff":{"coeffs":[["552960","4202496","13741056","25242624","28488960","20247552","8907584","2287040","308928","20288","512","0","0","0"],["331776","1990656","3732480","-912384","-14425344","-25353216","-22463808","-11279808","-3145152","-444480","-29952","-768","0","0"],["0","-331776","-2820096","-9372672","-15717888","-13319424","-3279744","3718464","3613920","1290912","203424","14496","384","0"],["0","0","0","552960","3207168","7769088","10063872","7338240","2808576","364352","-77440","-24576","-2176","-64"],["0","0","0","82944","393984","642816","181440","-749952","-1104624","-692880","-218508","-32868","-2292","-60"],["0","0","0","0","-20736","-124416","-316224","-440640","-363312","-177984","-49260","-6948","-468","-12"]]},"deriv_order":0},{"coeff":{"coeffs":[["-663552","-5640192","-20957184","-44706816","-60369408","-53561088","-31316352","-11757120","-2672576","-334272","-20928","-512","0","0","0","0"],["0","331776","3815424","17280000","42508800","63984384","61845120","38733888","15362400","3640192","467520","29760","736","0","0","0"],["0","0","497664","2737152","5515776","3297024","-5422464","-12426048","-11126304","-5407920","-1451424","-199872","-13248","-336","0","0"],["0","0","0","-414720","-2778624","-7997184","-12825216","-12381120","-7177248","-2265936","-235320","57568","16368","1392","40","0"],["0","0","0","0","82944","580608","1769472","3068928","3321216","2312064","1030080","284160","46084","4236","204","4"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","663552","5308416","18800640","38707200","51121152","45066240","26737152","10513920","2641952","402560","35520","1664","32","0","0","0"],["0","0","-995328","-7962624","-28200960","-58060800","-76681728","-67599360","-40105728","-15770880","-3962928","-603840","-53280","-2496","-48","0","0"],["0","0","0","497664","3981312","14100480","29030400","38340864","33799680","20052864","7885440","1981464","301920","26640","1248","24","0"],["0","0","0","0","-82944","-663552","-2350080","-4838400","-6390144","-5633280","-3342144","-1314240","-330244","-50320","-4440","-208","-4"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","-138240","-801792","-1942272","-2515968","-1834560","-702144","-91088","19360","6144","544","16","0"],["0","0","-82944","-179712","628992","3003264","5092416","4565088","2289840","608872","71824","2496","-128","-8"],["0","0","0","248832","1368576","3048192","3390336","1715904","-44064","-476784","-212184","-36072","-2664","-72"],["0","0","0","41472","145152","10368","-699840","-1476576","-1460592","-791400","-232404","-33804","-2316","-60"],["0","0","0","0","-20736","-124416","-316224","-440640","-363312","-177984","-49260","-6948","-468","-12"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","165888","1078272","2999808","4624128","4247424","2289600","621600","15312","-34144","-7296","-576","-16","0","0"],["0","0","165888","829440","1299456","-400896","-4119552","-6265728","-4853568","-2113440","-491464","-49552","-768","176","8","0"],["0","0","0","-248832","-1617408","-4458240","-6687360","-5738688","-2553120","-205776","333000","149736","24840","1800","48","0"],["0","0","0","0","82944","580608","1769472","3068928","3321216","2312064","1030080","284160","46084","4236","204","4"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","-331776","-2654208","-9400320","-19353600","-25560576","-22533120","-13368576","-5256960","-1320976","-201280","-17760","-832","-16","0","0"],["0","0","0","331776","2654208","9400320","19353600","25560576","22533120","13368576","5256960","1320976","201280","17760","832","16","0"],["0","0","0","0","-82944","-663552","-2350080","-4838400","-6390144","-5633280","-3342144","-1314240","-330244","-50320","-4440","-208","-4"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0"],["0","6"],["0","9"],["0","3"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-12","-18","-4","0"],["12","6","-2","1"],["0","-12","-12","-1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-24","-48","-26","-2","0"],["0","12","24","13","1"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["-24","-48","-26","-2","0"],["0","12","24","13","1"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["-110592","-663552","-1686528","-2350080","-1937664","-949248","-262720","-37056","-2496","-64","0","0","0"],["0","165888","995328","2529792","3525120","2906496","1423872","394080","55584","3744","96","0","0"],["0","0","-82944","-497664","-1264896","-1762560","-1453248","-711936","-197040","-27792","-1872","-48","0"],["0","0","0","13824","82944","210816","293760","242208","118656","32840","4632","312","8"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","-995328","-5971968","-15178752","-21150720","-17438976","-8543232","-2364480","-333504","-22464","-576","0","0","0"],["0","-1824768","-9455616","-18869760","-16008192","-245376","10495872","8479968","2935296","459072","32640","864","0","0"],["0","-995328","-3234816","497664","16111872","29341440","23550912","8050176","-238608","-878688","-188928","-15264","-432","0"],["0","-165888","497664","5059584","11155968","8695296","-2450304","-8913984","-6075936","-1686744","-129408","11664","2016","72"],["0","0","248832","746496","-456192","-4727808","-8024832","-6096384","-1819872","267840","297348","59724","4716","132"],["0","0","0","-124416","-622080","-1150848","-746496","463968","1111968","772344","253872","38880","2736","72"],["0","0","0","0","20736","124416","316224","440640","363312","177984","49260","6948","468","12"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","1327104","8957952","26210304","43379712","44402688","28829952","11695872","2809152","363456","23232","576","0","0","0","0"],["-663552","-2985984","-4700160","-3677184","-7534080","-21931776","-33272448","-27793728","-13335296","-3578560","-493632","-32768","-832","0","0","0"],["0","1658880","9123840","19215360","16630272","-1444608","-13675392","-8454720","718944","2827808","1188000","196896","14336","384","0","0"],["0","0","-1492992","-9206784","-23431680","-30627072","-19294848","-813888","7087392","4574736","1141392","74400","-9216","-1392","-48","0"],["0","0","0","580608","3856896","10955520","17193600","15954624","8480160","2014032","-226440","-249560","-53980","-5220","-236","-4"],["0","0","0","0","-82944","-580608","-1769472","-3068928","-3321216","-2312064","-1030080","-284160","-46084","-4236","-204","-4"]]},"deriv_order":1},{"coeff":{"coeffs":[["1327104","9953280","32292864","58613760","63535104","39011328","8408064","-5709312","-5230016","-1836832","-331520","-32192","-1600","-32","0","0","0"],["0","-2654208","-20238336","-67239936","-126627840","-146423808","-103583232","-39349248","-1949952","5203072","2352688","461760","46624","2368","48","0","0"],["0","0","1990656","15427584","52420608","102021120","124333056","96857856","46411776","11488896","40416","-773784","-195360","-21648","-1152","-24","0"],["0","0","0","-663552","-5225472","-18137088","-36357120","-46282752","-38676096","-21103872","-7171776","-1327712","-72316","14800","2776","176","4"],["0","0","0","0","82944","663552","2350080","4838400","6390144","5633280","3342144","1314240","330244","50320","4440","208","4"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["552960","3649536","10672128","18275328","20367360","15425280","7933568","2624832","477456","25504","-3456","-480","-16","0"],["331776","1658880","3373056","3386880","843264","-2954880","-5626752","-5281248","-2817328","-804776","-104080","-4864","64","8"],["0","-331776","-1658880","-3787776","-6151680","-8812800","-9991296","-7303872","-2828832","-298784","127672","34920","3016","88"],["0","0","165888","594432","366336","-1137024","-1923264","-459360","1191696","1179704","444116","72108","5228","140"],["0","0","0","-82944","-373248","-518400","134784","1190592","1467936","870864","267768","39816","2760","72"],["0","0","0","0","20736","124416","316224","440640","363312","177984","49260","6948","468","12"]]},"deriv_order":0},{"coeff":{"coeffs":[["-663552","-4976640","-16809984","-33785856","-44872704","-41195520","-26405376","-11560320","-3232928","-486160","-15968","4480","512","16","0","0"],["0","995328","6635520","19491840","33606144","38658816","32406912","21006144","10519008","3757152","829064","90832","3360","-112","-8","0"],["0","0","-829440","-5142528","-13298688","-18192384","-13450752","-4368384","310848","356736","-202552","-151144","-29352","-2296","-64","0"],["0","0","0","414720","2695680","7416576","11055744","9312192","3856032","-46128","-794760","-341728","-62452","-5628","-244","-4"],["0","0","0","0","-82944","-580608","-1769472","-3068928","-3321216","-2312064","-1030080","-284160","-46084","-4236","-204","-4"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","-663552","-4976640","-16146432","-29306880","-31767552","-19505664","-4204032","2854656","2615008","918416","165760","16096","800","16","0","0"],["0","0","995328","7630848","25546752","48660480","57328128","42038784","17572608","2402304","-1294032","-717136","-148000","-15264","-784","-16","0"],["0","0","0","-497664","-3898368","-13436928","-26680320","-33502464","-27409536","-14419584","-4543296","-667224","28324","23680","3192","184","4"],["0","0","0","0","82944","663552","2350080","4838400","6390144","5633280","3342144","1314240","330244","50320","4440","208","4"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["-48","-96","-52","-4","0"],["0","24","48","26","2"]]},"start_base":1}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-2","-2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-2","-1"]]},"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 + (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":"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 + (0))","kind":"preserver_image","operator":{"intercept":"0","shape":"affine","slope":"1"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["4","3"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","1"]]},"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 + (0)), for every n >= 0"},"parent_proof":{"statement":"open: no route proved that every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign; the first 10 parent rows pass the exact check (evidence only)","status":"open"},"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":"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":"open"},"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":"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) + (1) 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"}],"conditional_on":[],"rows_checked":10,"statement":"open: no route proved that every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign; the first 10 parent rows pass the exact check (evidence only)","status":"not_proved"},"rows_compared":16,"schema":"polytool.recurrence-preserver-image.v1","statement":"Q_n = lambda(n) T_n(P_(n+0)) with T = P((1) x + (0)) for every n >= 0 is certified; the lift is Open (open: no route proved that every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign; the first 10 parent rows pass the exact check (evidence only))"},"kind":"definition_equality"}