{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"intercept":"0","shape":"affine","slope":"1"},"parent":{"first_index":0,"initial_polynomials":[["1"],["3","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","1"]]},"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":[["-3","-1"],["0","1"],["-3","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-15","-18","-3"],["13","10","1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-13","-23","-11","-1"]]},"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":[["6","2"],["-6","-1"],["3","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["28","28","4"],["-13","-10","-1"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["13","23","11","1"]]},"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"],["3","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","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":[["-3","-1"],["0","1"],["-3","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-15","-18","-3"],["13","10","1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-13","-23","-11","-1"]]},"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":[["-2197","-5070","2184","13430","6291","-9900","-10008","-180","3393","1690","336","30","1"],["-6591","-15210","6552","40290","18873","-29700","-30024","-540","10179","5070","1008","90","3"],["-6591","-15210","6552","40290","18873","-29700","-30024","-540","10179","5070","1008","90","3"],["-2197","-5070","2184","13430","6291","-9900","-10008","-180","3393","1690","336","30","1"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","-4394","-10140","4368","26860","12582","-19800","-20016","-360","6786","3380","672","60","2"],["6591","2028","-36972","-27186","61707","67446","-29376","-59508","-11259","15288","9132","1926","177","6"],["19773","32448","-50076","-107766","23961","126846","30672","-58428","-31617","5148","7116","1746","171","6"],["19773","41236","-29796","-116502","-29759","101682","70272","-18396","-30897","-8424","356","402","51","2"],["6591","15210","-6552","-40290","-18873","29700","30024","540","-10179","-5070","-1008","-90","-3","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["4394","27716","40586","-34192","-124390","-57388","86634","100224","14670","-30164","-20978","-6128","-914","-68","-2"],["-19773","-32448","56667","122976","-30513","-167136","-49545","88128","61641","-4608","-17295","-6816","-1179","-96","-3"],["-52728","-148044","-8424","348528","312144","-162108","-358992","-124416","79272","81276","28344","4752","384","12","0"],["-28561","-87880","-24505","191360","218267","-52360","-222813","-112320","32301","55720","24661","5440","649","40","1"]]},"deriv_order":1},{"coeff":{"coeffs":[["28561","116441","112385","-166855","-409627","-165907","275173","335133","80019","-88021","-80381","-30101","-6089","-689","-41","-1"],["57122","232882","224770","-333710","-819254","-331814","550346","670266","160038","-176042","-160762","-60202","-12178","-1378","-82","-2"],["28561","116441","112385","-166855","-409627","-165907","275173","335133","80019","-88021","-80381","-30101","-6089","-689","-41","-1"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["10985","64896","146250","137912","-7137","-139584","-136500","-62352","-13737","-896","138","24","1"],["26364","172887","423501","438777","22503","-404538","-425310","-203406","-47382","-3789","321","69","3"],["13182","129285","393003","488859","110331","-376110","-456930","-236106","-59724","-5991","135","63","3"],["-8788","-507","100503","213035","124605","-96942","-183930","-111402","-32250","-4199","-141","15","1"],["-6591","-21801","-15249","25041","43914","14214","-15810","-16350","-6171","-1101","-93","-3","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["-32955","-205673","-503646","-559986","-116501","425889","549084","323556","103563","16425","482","-210","-27","-1"],["-37349","-294905","-866346","-1170386","-501683","635457","1104660","765924","293637","63641","7094","270","-13","-1"],["24167","27209","-221754","-660814","-653863","-6753","562068","561180","276585","78007","12742","1170","55","1"],["28561","116441","140946","-50414","-268681","-216321","6492","118812","86511","30791","6130","690","41","1"]]},"deriv_order":1},{"coeff":{"coeffs":[["-28561","-145002","-257387","-90532","319095","485002","209829","-125304","-205323","-117302","-36921","-6820","-731","-42","-1"],["-57122","-290004","-514774","-181064","638190","970004","419658","-250608","-410646","-234604","-73842","-13640","-1462","-84","-2"],["-28561","-145002","-257387","-90532","319095","485002","209829","-125304","-205323","-117302","-36921","-6820","-731","-42","-1"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["8","5","-1"],["-3","3","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-28","-26","4","2"],["13","-3","-9","-1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-13","-10","12","10","1"]]},"deriv_order":2,"shift":0}]},"quotient":[],"step_multiplier":{"coeffs":[["-2197","-5070","2184","13430","6291","-9900","-10008","-180","3393","1690","336","30","1"],["-6591","-15210","6552","40290","18873","-29700","-30024","-540","10179","5070","1008","90","3"],["-6591","-15210","6552","40290","18873","-29700","-30024","-540","10179","5070","1008","90","3"],["-2197","-5070","2184","13430","6291","-9900","-10008","-180","3393","1690","336","30","1"]]},"step_quotients":[[{"coeff":{"coeffs":[["-10985","-42926","-27443","89692","136711","-12602","-135531","-71064","25533","35774","11807","1148","-91","-22","-1"],["-26364","-120159","-104091","235338","431550","10767","-406269","-242676","65880","112431","39483","4362","-186","-63","-3"],["-13182","-102921","-147615","167862","474384","107913","-405621","-301644","44442","122649","47607","6198","-12","-57","-3"],["8788","-17069","-92729","-11522","200962","133117","-134559","-159516","-6624","51101","23993","3902","170","-13","-1"],["6591","8619","-21762","-33738","21417","48573","324","-29484","-10719","5109","4062","918","87","3","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["32955","139763","125255","-241633","-499825","-98905","419195","348723","-5535","-132855","-71195","-15251","-875","157","25","1"],["37349","220207","313885","-267401","-972743","-468437","667937","807939","133551","-242291","-173449","-49723","-6541","-295","11","1"],["-24167","21125","252005","190097","-446011","-640159","78289","569709","283707","-86017","-133313","-53693","-10457","-1061","-53","-1"],["-28561","-59319","63375","215865","26907","-270627","-170453","110493","144621","23419","-31059","-19221","-4791","-609","-39","-1"]]},"deriv_order":1},{"coeff":{"coeffs":[["28561","87880","-4056","-279240","-242772","243720","441080","59960","-255114","-168040","7640","50280","24012","5400","648","40","1"],["57122","175760","-8112","-558480","-485544","487440","882160","119920","-510228","-336080","15280","100560","48024","10800","1296","80","2"],["28561","87880","-4056","-279240","-242772","243720","441080","59960","-255114","-168040","7640","50280","24012","5400","648","40","1"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["21970","103428","152568","-12308","-263238","-252312","-13632","128280","96870","32468","5448","444","14"],["59319","295074","464256","3366","-770841","-786636","-70920","384300","300789","102474","17352","1422","45"],["46137","264654","477360","83946","-733095","-846036","-130968","383220","321147","112614","19368","1602","51"],["2197","57798","172224","108562","-206619","-341412","-103704","126660","127407","47678","8472","714","23"],["-6591","-15210","6552","40290","18873","-29700","-30024","-540","10179","5070","1008","90","3"]]},"deriv_order":0},{"coeff":{"coeffs":[["-61516","-317720","-555360","-146872","762580","1027392","333024","-350832","-425316","-204440","-52864","-7512","-548","-16","0"],["-94471","-547560","-1086215","-485104","1306893","2107144","888861","-589344","-882933","-464600","-130389","-20464","-1745","-72","-1"],["-4394","-141960","-506350","-529592","326046","1132112","778650","-126192","-489918","-315880","-102186","-18392","-1846","-96","-2"],["28561","87880","24505","-191360","-218267","52360","222813","112320","-32301","-55720","-24661","-5440","-649","-40","-1"]]},"deriv_order":1},{"coeff":{"coeffs":[["-28561","-116441","-112385","166855","409627","165907","-275173","-335133","-80019","88021","80381","30101","6089","689","41","1"],["-57122","-232882","-224770","333710","819254","331814","-550346","-670266","-160038","176042","160762","60202","12178","1378","82","2"],["-28561","-116441","-112385","166855","409627","165907","-275173","-335133","-80019","88021","80381","30101","6089","689","41","1"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["1"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-1","-1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-3","-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 >= 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"],["3","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","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) = (3) + (1) x, V_n(x) = 0, W_n(x) = (1) + (1) x; open hypotheses: 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":"no lean_proved catalog entry equals the parent; 12 with the same first index and seeds differ in the rule or in later initial rows (oeis_catalog:A039692:lean_proved, oeis_catalog:A079638:lean_proved, oeis_catalog:A093560:lean_proved, oeis_catalog:A103327:lean_proved, oeis_catalog:A110441:lean_proved, oeis_catalog:A116412:lean_proved, oeis_catalog:A125662:lean_proved, oeis_catalog:A127893:lean_proved, oeis_catalog:A216182:lean_proved, oeis_catalog:A249139:lean_proved, oeis_catalog:A249253:lean_proved, oeis_catalog:A327997: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"}