{"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":[["4","4"]]},"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"],["4","1"],["-5","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-30","-33","-3"],["20","20","1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-20","-40","-21","-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":[["11","2"],["-14","-1"],["5","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["50","53","4"],["-20","-20","-1"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["20","40","21","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":[["4","4"]]},"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"],["4","1"],["-5","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-30","-33","-3"],["20","20","1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-20","-40","-21","-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","8000","48000","121200","166000","132060","60240","14361","1443","63","1"],["0","0","0","24000","144000","363600","498000","396180","180720","43083","4329","189","3"],["0","0","0","24000","144000","363600","498000","396180","180720","43083","4329","189","3"],["0","0","0","8000","48000","121200","166000","132060","60240","14361","1443","63","1"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","8000","64000","217200","408400","464060","324360","134841","30165","2949","127","2"],["0","0","0","-16000","-48000","45600","395200","731880","671880","332718","83280","8532","376","6"],["0","0","0","-96000","-528000","-1166400","-1264800","-588720","69480","189108","68850","7902","366","6"],["0","0","0","-112000","-656000","-1600800","-2081600","-1516840","-579240","-80574","8520","2004","112","2"],["0","0","0","-40000","-240000","-606000","-830000","-660300","-301200","-71805","-7215","-315","-5","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-80000","-584000","-1852000","-3331600","-3721000","-2651180","-1190850","-321603","-48111","-3715","-139","-2"],["0","0","0","0","-48000","-312000","-871200","-1359600","-1290360","-757620","-266886","-51741","-4707","-195","-3"],["0","0","0","240000","1656000","4932000","8252400","8443800","5372820","2057310","431037","40851","1731","27","0"],["0","0","0","160000","1120000","3392000","5792000","6082400","4012000","1624080","376320","44481","2723","83","1"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","-160000","-1280000","-4512000","-9184000","-11874400","-10094400","-5636080","-2000400","-420801","-47204","-2806","-84","-1"],["0","0","0","-320000","-2560000","-9024000","-18368000","-23748800","-20188800","-11272160","-4000800","-841602","-94408","-5612","-168","-2"],["0","0","0","-160000","-1280000","-4512000","-9184000","-11874400","-10094400","-5636080","-2000400","-420801","-47204","-2806","-84","-1"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","-80000","-560000","-1684000","-2824000","-2859400","-1757000","-613950","-97800","-699","803","53","1"],["0","-240000","-1720000","-5292000","-9078000","-9408200","-5931300","-2143050","-365205","-9312","2094","154","3"],["0","-240000","-1800000","-5772000","-10290000","-11068200","-7251900","-2745450","-508815","-23742","1464","144","3"],["0","-80000","-680000","-2404000","-4642000","-5349400","-3737900","-1517550","-313215","-22344","-142","38","1"],["0","0","-40000","-240000","-606000","-830000","-660300","-301200","-71805","-7215","-315","-5","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","160000","1200000","3928000","7332000","8542800","6373400","2984900","809550","99198","-907","-909","-55","-1"],["0","320000","2560000","8976000","18056000","22877600","18829200","9981800","3243180","574716","42667","905","-27","-1"],["0","160000","1520000","6168000","14116000","20126800","18538200","11008900","4057710","851838","88055","4537","111","1"],["0","0","160000","1120000","3392000","5792000","6082400","4012000","1624080","376320","44481","2723","83","1"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","-160000","-1280000","-4512000","-9184000","-11874400","-10094400","-5636080","-2000400","-420801","-47204","-2806","-84","-1"],["0","0","-320000","-2560000","-9024000","-18368000","-23748800","-20188800","-11272160","-4000800","-841602","-94408","-5612","-168","-2"],["0","0","-160000","-1280000","-4512000","-9184000","-11874400","-10094400","-5636080","-2000400","-420801","-47204","-2806","-84","-1"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["10","5","-1"],["0","5","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-20","-10","12","2"],["0","-20","-20","-1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","20","40","21","1"]]},"deriv_order":2,"shift":0}]},"quotient":[],"step_multiplier":{"coeffs":[["0","0","0","8000","48000","121200","166000","132060","60240","14361","1443","63","1"],["0","0","0","24000","144000","363600","498000","396180","180720","43083","4329","189","3"],["0","0","0","24000","144000","363600","498000","396180","180720","43083","4329","189","3"],["0","0","0","8000","48000","121200","166000","132060","60240","14361","1443","63","1"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","80000","560000","1684000","2824000","2859400","1757000","613950","97800","699","-803","-53","-1"],["0","0","0","240000","1720000","5292000","9078000","9408200","5931300","2143050","365205","9312","-2094","-154","-3"],["0","0","0","240000","1800000","5772000","10290000","11068200","7251900","2745450","508815","23742","-1464","-144","-3"],["0","0","0","80000","680000","2404000","4642000","5349400","3737900","1517550","313215","22344","142","-38","-1"],["0","0","0","0","40000","240000","606000","830000","660300","301200","71805","7215","315","5","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-160000","-1200000","-3928000","-7332000","-8542800","-6373400","-2984900","-809550","-99198","907","909","55","1"],["0","0","0","-320000","-2560000","-8976000","-18056000","-22877600","-18829200","-9981800","-3243180","-574716","-42667","-905","27","1"],["0","0","0","-160000","-1520000","-6168000","-14116000","-20126800","-18538200","-11008900","-4057710","-851838","-88055","-4537","-111","-1"],["0","0","0","0","-160000","-1120000","-3392000","-5792000","-6082400","-4012000","-1624080","-376320","-44481","-2723","-83","-1"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","160000","1280000","4512000","9184000","11874400","10094400","5636080","2000400","420801","47204","2806","84","1"],["0","0","0","0","320000","2560000","9024000","18368000","23748800","20188800","11272160","4000800","841602","94408","5612","168","2"],["0","0","0","0","160000","1280000","4512000","9184000","11874400","10094400","5636080","2000400","420801","47204","2806","84","1"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","160000","1128000","3432000","5865200","6127200","3978060","1552260","330441","31563","1343","21"],["0","0","480000","3424000","10536000","18201600","19211600","12594480","4957980","1063128","101904","4344","68"],["0","0","480000","3504000","11016000","19413600","20871600","13915080","5560380","1206738","116334","4974","78"],["0","0","160000","1248000","4152000","7683200","8617200","5958960","2455860","545856","53208","2288","36"],["0","0","0","40000","240000","606000","830000","660300","301200","71805","7215","315","5"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","-320000","-2480000","-8440000","-16516000","-20417200","-16467800","-8620980","-2809950","-519999","-46297","-1897","-29","0"],["0","0","-640000","-5120000","-18000000","-36424000","-46626400","-39018000","-21253960","-7243980","-1416318","-137075","-6517","-141","-1"],["0","0","-320000","-2800000","-10680000","-23300000","-32001200","-28632600","-16644980","-6058110","-1272639","-135259","-7343","-195","-2"],["0","0","0","-160000","-1120000","-3392000","-5792000","-6082400","-4012000","-1624080","-376320","-44481","-2723","-83","-1"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","160000","1280000","4512000","9184000","11874400","10094400","5636080","2000400","420801","47204","2806","84","1"],["0","0","0","320000","2560000","9024000","18368000","23748800","20188800","11272160","4000800","841602","94408","5612","168","2"],["0","0","0","160000","1280000","4512000","9184000","11874400","10094400","5636080","2000400","420801","47204","2806","84","1"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["1"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-4","-4"]]},"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":[["4","4"]]},"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) = (4) + (4) x; open hypotheses: multipliers_vanish_at_zero: [x^0] c_2(n, x) = 4 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 = 4 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 = 4 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"}