{"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":[["9","9"]]},"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"],["9","1"],["-10","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-60","-63","-3"],["40","40","1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-40","-80","-41","-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":[["21","2"],["-29","-1"],["10","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["100","103","4"],["-40","-40","-1"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["40","80","41","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":[["9","9"]]},"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"],["9","1"],["-10","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-60","-63","-3"],["40","40","1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-40","-80","-41","-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","64000","384000","964800","1304000","1008120","432480","88721","5283","123","1"],["0","0","0","192000","1152000","2894400","3912000","3024360","1297440","266163","15849","369","3"],["0","0","0","192000","1152000","2894400","3912000","3024360","1297440","266163","15849","369","3"],["0","0","0","64000","384000","964800","1304000","1008120","432480","88721","5283","123","1"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","64000","512000","1732800","3233600","3616120","2448720","953681","182725","10689","247","2"],["0","0","0","-448000","-2304000","-4449600","-3339200","767160","3021360","1973833","495345","30837","731","6"],["0","0","0","-1728000","-9984000","-23745600","-29419200","-19395240","-5628240","199413","389685","28377","711","6"],["0","0","0","-1856000","-11008000","-27211200","-35886400","-26627480","-10525680","-1707949","24235","6999","217","2"],["0","0","0","-640000","-3840000","-9648000","-13040000","-10081200","-4324800","-887210","-52830","-1230","-10","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-1280000","-9152000","-28256000","-49038400","-52084000","-34444360","-13737700","-3011203","-301411","-13415","-269","-2"],["0","0","0","0","-384000","-2496000","-6940800","-10718400","-9960720","-5619240","-1829766","-297861","-16587","-375","-3"],["0","0","0","3840000","26688000","79776000","133233600","134815200","83411640","29974620","5374077","308511","7071","57","0"],["0","0","0","2560000","17920000","54016000","91136000","93449600","58928000","21856160","4192640","304961","10243","163","1"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","-2560000","-20480000","-71936000","-145152000","-184585600","-152377600","-80784160","-26048800","-4497601","-315204","-10406","-164","-1"],["0","0","0","-5120000","-40960000","-143872000","-290304000","-369171200","-304755200","-161568320","-52097600","-8995202","-630408","-20812","-328","-2"],["0","0","0","-2560000","-20480000","-71936000","-145152000","-184585600","-152377600","-80784160","-26048800","-4497601","-315204","-10406","-164","-1"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","-1280000","-8960000","-26912000","-44992000","-45277600","-27508000","-9415900","-1447600","-19399","2803","103","1"],["0","-3840000","-27520000","-84576000","-144624000","-148872800","-92605200","-32572500","-5230010","-111027","7179","299","3"],["0","-3840000","-28800000","-92256000","-163920000","-174952800","-112767600","-41222100","-7004430","-216687","4719","279","3"],["0","-1280000","-10880000","-38432000","-73936000","-84397600","-57751600","-22390300","-4109230","-177889","-887","73","1"],["0","0","-640000","-3840000","-9648000","-13040000","-10081200","-4324800","-887210","-52830","-1230","-10","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","2560000","19200000","62784000","116896000","135547200","100293600","46339800","12311100","1486398","13793","-3009","-105","-1"],["0","5120000","40960000","143488000","287808000","362230400","294036800","151607600","46478360","7165436","332547","4225","-47","-1"],["0","2560000","24320000","98624000","224928000","317819200","287192800","164195800","56023420","9871678","623715","17477","221","1"],["0","0","2560000","17920000","54016000","91136000","93449600","58928000","21856160","4192640","304961","10243","163","1"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","-2560000","-20480000","-71936000","-145152000","-184585600","-152377600","-80784160","-26048800","-4497601","-315204","-10406","-164","-1"],["0","0","-5120000","-40960000","-143872000","-290304000","-369171200","-304755200","-161568320","-52097600","-8995202","-630408","-20812","-328","-2"],["0","0","-2560000","-20480000","-71936000","-145152000","-184585600","-152377600","-80784160","-26048800","-4497601","-315204","-10406","-164","-1"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["20","10","-1"],["0","10","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-40","-20","22","2"],["0","-40","-40","-1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","40","80","41","1"]]},"deriv_order":2,"shift":0}]},"quotient":[],"step_multiplier":{"coeffs":[["0","0","0","64000","384000","964800","1304000","1008120","432480","88721","5283","123","1"],["0","0","0","192000","1152000","2894400","3912000","3024360","1297440","266163","15849","369","3"],["0","0","0","192000","1152000","2894400","3912000","3024360","1297440","266163","15849","369","3"],["0","0","0","64000","384000","964800","1304000","1008120","432480","88721","5283","123","1"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","1280000","8960000","26912000","44992000","45277600","27508000","9415900","1447600","19399","-2803","-103","-1"],["0","0","0","3840000","27520000","84576000","144624000","148872800","92605200","32572500","5230010","111027","-7179","-299","-3"],["0","0","0","3840000","28800000","92256000","163920000","174952800","112767600","41222100","7004430","216687","-4719","-279","-3"],["0","0","0","1280000","10880000","38432000","73936000","84397600","57751600","22390300","4109230","177889","887","-73","-1"],["0","0","0","0","640000","3840000","9648000","13040000","10081200","4324800","887210","52830","1230","10","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-2560000","-19200000","-62784000","-116896000","-135547200","-100293600","-46339800","-12311100","-1486398","-13793","3009","105","1"],["0","0","0","-5120000","-40960000","-143488000","-287808000","-362230400","-294036800","-151607600","-46478360","-7165436","-332547","-4225","47","1"],["0","0","0","-2560000","-24320000","-98624000","-224928000","-317819200","-287192800","-164195800","-56023420","-9871678","-623715","-17477","-221","-1"],["0","0","0","0","-2560000","-17920000","-54016000","-91136000","-93449600","-58928000","-21856160","-4192640","-304961","-10243","-163","-1"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","2560000","20480000","71936000","145152000","184585600","152377600","80784160","26048800","4497601","315204","10406","164","1"],["0","0","0","0","5120000","40960000","143872000","290304000","369171200","304755200","161568320","52097600","8995202","630408","20812","328","2"],["0","0","0","0","2560000","20480000","71936000","145152000","184585600","152377600","80784160","26048800","4497601","315204","10406","164","1"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","2560000","17984000","54336000","91716800","93788800","58632120","21280520","3848881","221523","5083","41"],["0","0","7680000","54592000","166848000","284798400","294406400","185977560","68166360","12433853","717399","16479","133"],["0","0","7680000","55872000","174528000","304094400","320486400","206139960","76815960","14208273","823059","18939","153"],["0","0","2560000","19904000","65856000","120660800","132908800","88875720","34254920","6510511","380013","8773","71"],["0","0","0","640000","3840000","9648000","13040000","10081200","4324800","887210","52830","1230","10"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","-5120000","-39680000","-134720000","-262048000","-320132800","-252671200","-127123960","-38359900","-5983999","-328997","-7397","-59","0"],["0","0","-10240000","-81920000","-287360000","-578112000","-731401600","-598792000","-313175920","-98575960","-16160638","-962955","-25037","-281","-1"],["0","0","-5120000","-44800000","-170560000","-370080000","-502404800","-439570400","-244979960","-82072220","-14369279","-938919","-27883","-385","-2"],["0","0","0","-2560000","-17920000","-54016000","-91136000","-93449600","-58928000","-21856160","-4192640","-304961","-10243","-163","-1"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","2560000","20480000","71936000","145152000","184585600","152377600","80784160","26048800","4497601","315204","10406","164","1"],["0","0","0","5120000","40960000","143872000","290304000","369171200","304755200","161568320","52097600","8995202","630408","20812","328","2"],["0","0","0","2560000","20480000","71936000","145152000","184585600","152377600","80784160","26048800","4497601","315204","10406","164","1"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["1"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-9","-9"]]},"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":[["9","9"]]},"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) = (9) + (9) x; open hypotheses: multipliers_vanish_at_zero: [x^0] c_2(n, x) = 9 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 = 9 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 = 9 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"}