{"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":[["7","7"]]},"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"],["7","1"],["-8","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-48","-51","-3"],["32","32","1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-32","-64","-33","-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":[["17","2"],["-23","-1"],["8","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["80","83","4"],["-32","-32","-1"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["32","64","33","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":[["7","7"]]},"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"],["7","1"],["-8","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-48","-51","-3"],["32","32","1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-32","-64","-33","-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","32768","196608","494592","670720","522336","227712","48705","3459","99","1"],["0","0","0","98304","589824","1483776","2012160","1567008","683136","146115","10377","297","3"],["0","0","0","98304","589824","1483776","2012160","1567008","683136","146115","10377","297","3"],["0","0","0","32768","196608","494592","670720","522336","227712","48705","3459","99","1"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","32768","262144","887808","1659904","1863776","1272384","504129","100869","7017","199","2"],["0","0","0","-163840","-786432","-1293312","-386048","1412640","1995456","1122747","274935","20259","589","6"],["0","0","0","-688128","-3932160","-9206784","-11117568","-6944736","-1647936","343467","219591","18675","573","6"],["0","0","0","-753664","-4456448","-10982400","-14437376","-10672288","-4192704","-664791","17853","4641","175","2"],["0","0","0","-262144","-1572864","-3956736","-5365760","-4178688","-1821696","-389640","-27672","-792","-8","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-524288","-3768320","-11714560","-20521984","-22090240","-14909216","-6150480","-1436163","-164715","-8815","-217","-2"],["0","0","0","0","-196608","-1277952","-3557376","-5508096","-5146176","-2933280","-975366","-166869","-10971","-303","-3"],["0","0","0","1572864","10911744","32587776","54451200","55254528","34435296","12584880","2357757","160407","4503","45","0"],["0","0","0","1048576","7340032","22151168","37486592","38672384","24672256","9367680","1896960","162561","6659","131","1"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","-1048576","-8388608","-29491200","-59637760","-76158976","-63344640","-34039936","-11264640","-2059521","-169220","-6790","-132","-1"],["0","0","0","-2097152","-16777216","-58982400","-119275520","-152317952","-126689280","-68079872","-22529280","-4119042","-338440","-13580","-264","-2"],["0","0","0","-1048576","-8388608","-29491200","-59637760","-76158976","-63344640","-34039936","-11264640","-2059521","-169220","-6790","-132","-1"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","-524288","-3670016","-11026432","-18448384","-18594304","-11330048","-3900336","-606912","-8223","1859","83","1"],["0","-1572864","-11272192","-34652160","-59301888","-61148672","-38168832","-13522704","-2210376","-52341","4785","241","3"],["0","-1572864","-11796480","-37797888","-67215360","-71880192","-46526208","-17166096","-2989656","-107685","3201","225","3"],["0","-524288","-4456448","-15745024","-30318592","-34691584","-23866112","-9365424","-1775832","-91239","-517","59","1"],["0","0","-262144","-1572864","-3956736","-5365760","-4178688","-1821696","-389640","-27672","-792","-8","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","1048576","7864320","25722880","47923200","55636992","41254400","19130720","5114160","623358","4505","-2025","-85","-1"],["0","2097152","16777216","58785792","117997568","148760576","121181184","62933696","19596000","3143676","171571","2609","-39","-1"],["0","1048576","9961472","40402944","92225536","130610176","118599168","68475232","23849520","4417278","329627","11293","177","1"],["0","0","1048576","7340032","22151168","37486592","38672384","24672256","9367680","1896960","162561","6659","131","1"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","-1048576","-8388608","-29491200","-59637760","-76158976","-63344640","-34039936","-11264640","-2059521","-169220","-6790","-132","-1"],["0","0","-2097152","-16777216","-58982400","-119275520","-152317952","-126689280","-68079872","-22529280","-4119042","-338440","-13580","-264","-2"],["0","0","-1048576","-8388608","-29491200","-59637760","-76158976","-63344640","-34039936","-11264640","-2059521","-169220","-6790","-132","-1"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["16","8","-1"],["0","8","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-32","-16","18","2"],["0","-32","-32","-1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","32","64","33","1"]]},"deriv_order":2,"shift":0}]},"quotient":[],"step_multiplier":{"coeffs":[["0","0","0","32768","196608","494592","670720","522336","227712","48705","3459","99","1"],["0","0","0","98304","589824","1483776","2012160","1567008","683136","146115","10377","297","3"],["0","0","0","98304","589824","1483776","2012160","1567008","683136","146115","10377","297","3"],["0","0","0","32768","196608","494592","670720","522336","227712","48705","3459","99","1"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","524288","3670016","11026432","18448384","18594304","11330048","3900336","606912","8223","-1859","-83","-1"],["0","0","0","1572864","11272192","34652160","59301888","61148672","38168832","13522704","2210376","52341","-4785","-241","-3"],["0","0","0","1572864","11796480","37797888","67215360","71880192","46526208","17166096","2989656","107685","-3201","-225","-3"],["0","0","0","524288","4456448","15745024","30318592","34691584","23866112","9365424","1775832","91239","517","-59","-1"],["0","0","0","0","262144","1572864","3956736","5365760","4178688","1821696","389640","27672","792","8","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-1048576","-7864320","-25722880","-47923200","-55636992","-41254400","-19130720","-5114160","-623358","-4505","2025","85","1"],["0","0","0","-2097152","-16777216","-58785792","-117997568","-148760576","-121181184","-62933696","-19596000","-3143676","-171571","-2609","39","1"],["0","0","0","-1048576","-9961472","-40402944","-92225536","-130610176","-118599168","-68475232","-23849520","-4417278","-329627","-11293","-177","-1"],["0","0","0","0","-1048576","-7340032","-22151168","-37486592","-38672384","-24672256","-9367680","-1896960","-162561","-6659","-131","-1"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","1048576","8388608","29491200","59637760","76158976","63344640","34039936","11264640","2059521","169220","6790","132","1"],["0","0","0","0","2097152","16777216","58982400","119275520","152317952","126689280","68079872","22529280","4119042","338440","13580","264","2"],["0","0","0","0","1048576","8388608","29491200","59637760","76158976","63344640","34039936","11264640","2059521","169220","6790","132","1"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","1048576","7372800","22315008","37784576","38848512","24523872","9073056","1717953","117315","3299","33"],["0","0","3145728","22380544","68517888","117310464","121911296","77750304","29040864","5543499","379617","10689","107"],["0","0","3145728","22904832","71663616","125223936","132642816","86107680","32684256","6322779","434961","12273","123"],["0","0","1048576","8159232","27033600","49654784","54945792","37059936","14538144","2886873","200331","5675","57"],["0","0","0","262144","1572864","3956736","5365760","4178688","1821696","389640","27672","792","8"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","-2097152","-16252928","-55214080","-107560960","-131795968","-104599040","-53170656","-16378800","-2682879","-173725","-4765","-47","0"],["0","0","-4194304","-33554432","-117768192","-237273088","-301078528","-247870464","-131013568","-42125280","-7262718","-510011","-16189","-225","-1"],["0","0","-2097152","-18350080","-69894144","-151863296","-206769152","-181943808","-102515168","-35114160","-6476799","-498847","-18083","-309","-2"],["0","0","0","-1048576","-7340032","-22151168","-37486592","-38672384","-24672256","-9367680","-1896960","-162561","-6659","-131","-1"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","1048576","8388608","29491200","59637760","76158976","63344640","34039936","11264640","2059521","169220","6790","132","1"],["0","0","0","2097152","16777216","58982400","119275520","152317952","126689280","68079872","22529280","4119042","338440","13580","264","2"],["0","0","0","1048576","8388608","29491200","59637760","76158976","63344640","34039936","11264640","2059521","169220","6790","132","1"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["1"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-7","-7"]]},"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":[["7","7"]]},"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) = (7) + (7) x; open hypotheses: multipliers_vanish_at_zero: [x^0] c_2(n, x) = 7 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 = 7 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 = 7 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"}