{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"intercept":"0","shape":"affine","slope":"1"},"parent":{"first_index":0,"initial_polynomials":[["1"],["2","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["6","6"]]},"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":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["-2","-1"],["6","1"],["-7","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-42","-45","-3"],["28","28","1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-28","-56","-29","-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":[["15","2"],["-20","-1"],["7","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["70","73","4"],["-28","-28","-1"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["28","56","29","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"],["2","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["6","6"]]},"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":[["-2","-1"],["6","1"],["-7","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-42","-45","-3"],["28","28","1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-28","-56","-29","-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":[["0","0","0","21952","131712","331632","450800","352884","155568","34217","2691","87","1"],["0","0","0","65856","395136","994896","1352400","1058652","466704","102651","8073","261","3"],["0","0","0","65856","395136","994896","1352400","1058652","466704","102651","8073","261","3"],["0","0","0","21952","131712","331632","450800","352884","155568","34217","2691","87","1"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","21952","175616","595056","1114064","1254484","861336","345353","71125","5469","175","2"],["0","0","0","-87808","-395136","-536256","186592","1293264","1495032","796540","194538","15798","518","6"],["0","0","0","-395136","-2239104","-5179104","-6124608","-3647112","-682920","317502","156864","14580","504","6"],["0","0","0","-439040","-2590336","-6369216","-8352736","-6156080","-2405592","-373204","14614","3642","154","2"],["0","0","0","-153664","-921984","-2321424","-3155600","-2470188","-1088976","-239519","-18837","-609","-7","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-307328","-2217152","-6925856","-12212368","-13267240","-9078580","-3829462","-930499","-115399","-6875","-191","-2"],["0","0","0","0","-131712","-856128","-2384928","-3699696","-3469704","-1992060","-672006","-118797","-8595","-267","-3"],["0","0","0","921984","6388032","19065312","31867248","32402328","20296332","7504266","1447485","108603","3435","39","0"],["0","0","0","614656","4302592","12995584","22039808","22834784","14687456","5666864","1188992","112001","5155","115","1"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","-614656","-4917248","-17298176","-35035392","-44874592","-37522240","-20354320","-6855856","-1300993","-117156","-5270","-116","-1"],["0","0","0","-1229312","-9834496","-34596352","-70070784","-89749184","-75044480","-40708640","-13711712","-2601986","-234312","-10540","-232","-2"],["0","0","0","-614656","-4917248","-17298176","-35035392","-44874592","-37522240","-20354320","-6855856","-1300993","-117156","-5270","-116","-1"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","-307328","-2151296","-6464864","-10822336","-10919944","-6667528","-2304106","-361144","-4675","1459","73","1"],["0","-921984","-6607552","-20316576","-34788432","-35915432","-22472772","-8001294","-1322951","-32862","3768","212","3"],["0","-921984","-6914880","-22160544","-39431280","-42226632","-27413148","-10179246","-1801989","-70536","2550","198","3"],["0","-307328","-2612288","-9230816","-17786608","-20386744","-14078092","-5571034","-1079701","-61186","-368","52","1"],["0","0","-153664","-921984","-2321424","-3155600","-2470188","-1088976","-239519","-18837","-609","-7","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","614656","4609920","15081024","28109536","32662224","24255000","11275740","3026394","370494","1757","-1605","-75","-1"],["0","1229312","9834496","34464640","69214656","87364256","71344784","37238936","11719652","1929980","115515","1945","-35","-1"],["0","614656","5839232","23686208","54100704","76741840","69924568","40650652","14360122","2748478","225759","8705","155","1"],["0","0","614656","4302592","12995584","22039808","22834784","14687456","5666864","1188992","112001","5155","115","1"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","-614656","-4917248","-17298176","-35035392","-44874592","-37522240","-20354320","-6855856","-1300993","-117156","-5270","-116","-1"],["0","0","-1229312","-9834496","-34596352","-70070784","-89749184","-75044480","-40708640","-13711712","-2601986","-234312","-10540","-232","-2"],["0","0","-614656","-4917248","-17298176","-35035392","-44874592","-37522240","-20354320","-6855856","-1300993","-117156","-5270","-116","-1"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["14","7","-1"],["0","7","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-28","-14","16","2"],["0","-28","-28","-1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","28","56","29","1"]]},"deriv_order":2,"shift":0}]},"quotient":[],"step_multiplier":{"coeffs":[["0","0","0","21952","131712","331632","450800","352884","155568","34217","2691","87","1"],["0","0","0","65856","395136","994896","1352400","1058652","466704","102651","8073","261","3"],["0","0","0","65856","395136","994896","1352400","1058652","466704","102651","8073","261","3"],["0","0","0","21952","131712","331632","450800","352884","155568","34217","2691","87","1"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","307328","2151296","6464864","10822336","10919944","6667528","2304106","361144","4675","-1459","-73","-1"],["0","0","0","921984","6607552","20316576","34788432","35915432","22472772","8001294","1322951","32862","-3768","-212","-3"],["0","0","0","921984","6914880","22160544","39431280","42226632","27413148","10179246","1801989","70536","-2550","-198","-3"],["0","0","0","307328","2612288","9230816","17786608","20386744","14078092","5571034","1079701","61186","368","-52","-1"],["0","0","0","0","153664","921984","2321424","3155600","2470188","1088976","239519","18837","609","7","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-614656","-4609920","-15081024","-28109536","-32662224","-24255000","-11275740","-3026394","-370494","-1757","1605","75","1"],["0","0","0","-1229312","-9834496","-34464640","-69214656","-87364256","-71344784","-37238936","-11719652","-1929980","-115515","-1945","35","1"],["0","0","0","-614656","-5839232","-23686208","-54100704","-76741840","-69924568","-40650652","-14360122","-2748478","-225759","-8705","-155","-1"],["0","0","0","0","-614656","-4302592","-12995584","-22039808","-22834784","-14687456","-5666864","-1188992","-112001","-5155","-115","-1"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","614656","4917248","17298176","35035392","44874592","37522240","20354320","6855856","1300993","117156","5270","116","1"],["0","0","0","0","1229312","9834496","34596352","70070784","89749184","75044480","40708640","13711712","2601986","234312","10540","232","2"],["0","0","0","0","614656","4917248","17298176","35035392","44874592","37522240","20354320","6855856","1300993","117156","5270","116","1"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","614656","4324544","13105344","22239728","22953952","14589540","5469548","1067641","80475","2551","29"],["0","0","1843968","13127296","40238016","69040608","72017456","46238808","17497620","3442442","260262","8262","94"],["0","0","1843968","13434624","42081984","73683456","78328656","51179184","19675572","3921480","297936","9480","108"],["0","0","614656","4785536","15871296","29204000","32420752","22000104","8736476","1786198","136986","4378","50"],["0","0","0","153664","921984","2321424","3155600","2470188","1088976","239519","18837","609","7"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","-1229312","-9527168","-32379200","-63144928","-77536816","-61777240","-31630060","-9882250","-1671487","-118913","-3665","-41","0"],["0","0","-2458624","-19668992","-69060992","-139285440","-177113440","-146389264","-77947576","-25431364","-4531966","-349827","-12485","-197","-1"],["0","0","-1229312","-10756480","-40984384","-89136096","-121616432","-107446808","-61004972","-21215978","-4049471","-342915","-13975","-271","-2"],["0","0","0","-614656","-4302592","-12995584","-22039808","-22834784","-14687456","-5666864","-1188992","-112001","-5155","-115","-1"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","614656","4917248","17298176","35035392","44874592","37522240","20354320","6855856","1300993","117156","5270","116","1"],["0","0","0","1229312","9834496","34596352","70070784","89749184","75044480","40708640","13711712","2601986","234312","10540","232","2"],["0","0","0","614656","4917248","17298176","35035392","44874592","37522240","20354320","6855856","1300993","117156","5270","116","1"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["1"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-6","-6"]]},"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 >= 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"],["2","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["6","6"]]},"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) = (6) + (6) x; open hypotheses: multipliers_vanish_at_zero: [x^0] c_2(n, x) = 6 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 = 6 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 = 6 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; 25 with the same first index and seeds differ in the rule or in later initial rows (oeis_catalog:A029653:lean_proved, oeis_catalog:A060920:lean_proved, oeis_catalog:A084950:lean_proved, oeis_catalog:A093375:lean_proved, oeis_catalog:A104029:lean_proved, oeis_catalog:A106246:lean_proved, oeis_catalog:A113214:lean_proved, oeis_catalog:A113413:lean_proved, oeis_catalog:A117317:lean_proved, oeis_catalog:A119308:lean_proved, oeis_catalog:A119808:lean_proved, oeis_catalog:A121574:lean_proved, oeis_catalog:A126216:lean_proved, oeis_catalog:A133087:lean_proved, oeis_catalog:A134082:lean_proved, oeis_catalog:A154929:lean_proved, oeis_catalog:A156319:lean_proved, oeis_catalog:A167194:lean_proved, oeis_catalog:A193727:lean_proved, oeis_catalog:A193728:lean_proved, oeis_catalog:A193730:lean_proved, oeis_catalog:A193735:lean_proved, oeis_catalog:A202241:lean_proved, oeis_catalog:A318397:lean_proved, oeis_catalog:A394813: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"}