{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"intercept":"0","shape":"affine","slope":"1"},"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":"existing definition"},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"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}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"denominator":{"coeffs":[["0"],["1"]]},"terms":[{"coeff":{"coeffs":[["8","4"],["-7","-2"],["3","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["30","36","8"],["-12","-12","-2"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["12","24","14","2"]]},"deriv_order":2,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["1","1"],"operator":{"intercept":"0","shape":"affine","slope":"1"},"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":[["1"],["1"]]},"deriv_order":0}],"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":[],"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":[["1"]]},"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 = P((1) x + (0)); 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":["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","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 = 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) = (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":"no lean_proved catalog entry equals the parent; 1 with the same first index and seeds differ in the rule or in later initial rows (oeis_catalog:A134239:lean_proved)","route":"attestation","success":false,"variant":"oeis_catalog"}],"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"}