{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"intercept":"0","shape":"affine","slope":"1"},"parent":{"first_index":0,"initial_polynomials":[["0"],["2"],["15","6"]],"recurrence":{"denominator":{"coeffs":[["0"],["4"],["-10"],["2"],["4"]]},"terms":[{"coeff":{"coeffs":[["0","0","0","0"],["0","0","-12","10"],["0","0","12","-10"],["0","0","48","-4"],["0","0","-48","4"]]},"deriv_order":0,"offset":3,"sign":"none"},{"coeff":{"coeffs":[["0","0","0","0","0"],["0","0","0","-4","3"],["0","0","0","4","-3"],["0","0","0","16","0"],["0","0","0","-16","0"]]},"deriv_order":1,"offset":3,"sign":"none"},{"coeff":{"coeffs":[["0","0","0"],["-8","8","-6"],["16","-16","12"],["32","-8","6"],["-64","16","-12"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["0","0","0","0"],["0","8","-2","-3"],["0","-16","4","6"],["0","-32","-16","0"],["0","64","32","0"]]},"deriv_order":1,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["8","0"],["0","0"],["-40","-12"],["0","0"],["32","12"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","-4","3"],["0","0","0"],["0","20","-3"],["0","0","0"],["0","-16","0"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"existing definition"},"identifying_rows":2,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["-12","0"],["-26","-10"],["-18","-11"],["-4","-3"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","6","6"],["0","7","7"],["0","2","2"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0"],["3"],["4"],["1"]]},"deriv_order":0,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0,1],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["0"],["2"]],"recurrence":{"denominator":{"coeffs":[["0"],["-2"],["1"],["1"]]},"terms":[{"coeff":{"coeffs":[["0","-2"],["2","-3"],["6","2"],["4","3"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","-1","-1"],["0","-3","-3"],["0","-2","-2"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":1,"multiplier":["0","3","4","1"],"operator":{"intercept":"0","shape":"affine","slope":"1"},"parent":{"first_index":0,"initial_polynomials":[["0"],["2"],["15","6"]],"recurrence":{"denominator":{"coeffs":[["0"],["4"],["-10"],["2"],["4"]]},"terms":[{"coeff":{"coeffs":[["0","0","0","0"],["0","0","-12","10"],["0","0","12","-10"],["0","0","48","-4"],["0","0","-48","4"]]},"deriv_order":0,"offset":3,"sign":"none"},{"coeff":{"coeffs":[["0","0","0","0","0"],["0","0","0","-4","3"],["0","0","0","4","-3"],["0","0","0","16","0"],["0","0","0","-16","0"]]},"deriv_order":1,"offset":3,"sign":"none"},{"coeff":{"coeffs":[["0","0","0"],["-8","8","-6"],["16","-16","12"],["32","-8","6"],["-64","16","-12"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["0","0","0","0"],["0","8","-2","-3"],["0","-16","4","6"],["0","-32","-16","0"],["0","64","32","0"]]},"deriv_order":1,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["8","0"],["0","0"],["-40","-12"],["0","0"],["32","12"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","-4","3"],["0","0","0"],["0","20","-3"],["0","0","0"],["0","-16","0"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_leader_shift":3,"parent_valid_from_base":0,"quotients":[],"row_annihilation":{"kind":"system","system":{"generators":[{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","16","10"],["0","24","19"],["0","8","7"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","0","-8","-8"],["0","0","-4","-4"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-30","-12"],["-22","-16"],["-4","-4"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["4"],["5"],["1"]]},"deriv_order":0,"shift":2}]},"quotient":[],"step_multiplier":{"coeffs":[["0","0","0"],["0","0","0"],["0","144","144"],["0","744","744"],["0","1609","1609"],["0","1890","1890"],["0","1311","1311"],["0","548","548"],["0","135","135"],["0","18","18"],["0","1","1"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","0"],["0","0","0","0"],["0","201600","167040","-34560"],["0","1320960","1089408","-231552"],["0","3835928","3146600","-689328"],["0","6520580","5316180","-1204400"],["0","7223004","5848320","-1374684"],["0","5494196","4414460","-1079736"],["0","2945276","2346612","-598664"],["0","1122684","886404","-236280"],["0","302500","236548","-65952"],["0","56284","43572","-12712"],["0","6876","5268","-1608"],["0","496","376","-120"],["0","16","12","-4"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0"],["0","0","0","0","0"],["0","0","-403200","-411840","-8640"],["0","0","-2440320","-2486688","-46368"],["0","0","-6552496","-6660124","-107628"],["0","0","-10324592","-10466732","-142140"],["0","0","-10641996","-10760271","-118275"],["0","0","-7569400","-7634254","-64854"],["0","0","-3815348","-3839117","-23769"],["0","0","-1375296","-1381056","-5760"],["0","0","-352388","-353273","-885"],["0","0","-62680","-62758","-78"],["0","0","-7356","-7359","-3"],["0","0","-512","-512","0"],["0","0","-16","-16","0"]]},"deriv_order":1}],[{"coeff":{"coeffs":[["0","0","0","0","0"],["0","0","0","0","0"],["0","0","403200","417600","14400"],["0","0","2238720","2314560","75840"],["0","0","5433136","5605508","172372"],["0","0","7608024","7830490","222466"],["0","0","6837984","7018636","180652"],["0","0","4150408","4247022","96614"],["0","0","1740144","1774688","34544"],["0","0","505224","513398","8174"],["0","0","99776","101004","1228"],["0","0","12792","12898","106"],["0","0","960","964","4"],["0","0","32","32","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0"],["0","0","-2016000","-2836800","-1006560","-185760"],["0","0","-9984000","-14897280","-5952672","-1039392"],["0","0","-21659120","-34752164","-15636822","-2543778"],["0","0","-27247272","-47786126","-24132795","-3593941"],["0","0","-22158696","-43288738","-24389852","-3259810"],["0","0","-12269312","-27297372","-17024531","-1996471"],["0","0","-4732224","-12314976","-8426996","-844244"],["0","0","-1274184","-4011806","-2984665","-247043"],["0","0","-235144","-937770","-751756","-49130"],["0","0","-28368","-153528","-131497","-6337"],["0","0","-2016","-16720","-15182","-478"],["0","0","-64","-1088","-1040","-16"],["0","0","0","-32","-32","0"]]},"deriv_order":1}],[{"coeff":{"coeffs":[["0","0","0","0","0","0"],["0","0","12096000","17020800","6039360","1114560"],["0","0","74016000","106015680","39467232","7467552"],["0","0","203874720","297332184","115961892","22504428"],["0","0","335065472","497595216","202932124","40402380"],["0","0","367001320","554932918","236167969","48236371"],["0","0","283221288","435943314","193192644","40470618"],["0","0","158595920","248425752","114398281","24568449"],["0","0","65309296","104070028","49696072","10935340"],["0","0","19794600","32075454","15852267","3571413"],["0","0","4364584","7188882","3670196","845898"],["0","0","680960","1139564","599927","141323"],["0","0","71232","121056","65604","15780"],["0","0","4480","7728","4304","1056"],["0","0","128","224","128","32"]]},"deriv_order":0}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["-12","0"],["-26","-10"],["-18","-11"],["-4","-3"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","6","6"],["0","7","7"],["0","2","2"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0"],["3"],["4"],["1"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0"],["3"],["4"],["1"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["0","0","0"],["0","0","0"],["0","36","36"],["0","141","141"],["0","217","217"],["0","166","166"],["0","66","66"],["0","13","13"],["0","1","1"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0"],["0","0","0"],["0","21600","21600"],["0","126360","126360"],["0","325368","325368"],["0","486782","486782"],["0","470458","470458"],["0","308738","308738"],["0","140562","140562"],["0","44454","44454"],["0","9582","9582"],["0","1342","1342"],["0","110","110"],["0","4","4"]]},"deriv_order":0}],[{"coeff":{"coeffs":[["0","0","0","0"],["0","0","0","0"],["0","0","10800","10800"],["0","0","57780","57780"],["0","0","133794","133794"],["0","0","176494","176494"],["0","0","146982","146982"],["0","0","80878","80878"],["0","0","29842","29842"],["0","0","7306","7306"],["0","0","1138","1138"],["0","0","102","102"],["0","0","4","4"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0"],["0","0","54000","108000","54000"],["0","0","256500","513000","256500"],["0","0","528030","1056060","528030"],["0","0","622028","1244056","622028"],["0","0","465870","931740","465870"],["0","0","232484","464968","232484"],["0","0","78482","156964","78482"],["0","0","17732","35464","17732"],["0","0","2570","5140","2570"],["0","0","216","432","216"],["0","0","8","16","8"]]},"deriv_order":1}],[{"coeff":{"coeffs":[["0","0","0","0","0"],["0","0","-324000","-648000","-324000"],["0","0","-1917000","-3834000","-1917000"],["0","0","-5071680","-10143360","-5071680"],["0","0","-7941378","-15882756","-7941378"],["0","0","-8205476","-16410952","-8205476"],["0","0","-5900050","-11800100","-5900050"],["0","0","-3030020","-6060040","-3030020"],["0","0","-1120734","-2241468","-1120734"],["0","0","-296508","-593016","-296508"],["0","0","-54750","-109500","-54750"],["0","0","-6700","-13400","-6700"],["0","0","-488","-976","-488"],["0","0","-16","-32","-16"]]},"deriv_order":0}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0"],["-1"],["1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-1","2"],["-2","-2"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","1","1"]]},"deriv_order":2,"shift":0}]},"quotient":[],"step_multiplier":{"coeffs":[["0","0","0","0","0"],["0","0","0","0","0"],["0","0","0","0","0"],["0","0","27","54","27"],["0","0","108","216","108"],["0","0","171","342","171"],["0","0","136","272","136"],["0","0","57","114","57"],["0","0","12","24","12"],["0","0","1","2","1"]]},"step_quotients":[[],[{"coeff":{"coeffs":[["0","0","0","0","0"],["0","0","0","0","0"],["0","0","0","0","0"],["0","0","2700","5400","2700"],["0","0","13770","27540","13770"],["0","0","30006","60012","30006"],["0","0","36622","73244","36622"],["0","0","27590","55180","27590"],["0","0","13322","26644","13322"],["0","0","4130","8260","4130"],["0","0","794","1588","794"],["0","0","86","172","86"],["0","0","4","8","4"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0"],["0","0","0","0","0","0"],["0","0","-8100","-16200","-8100","0"],["0","0","-38610","-82620","-49410","-5400"],["0","0","-78948","-180036","-123228","-22140"],["0","0","-90930","-219732","-166674","-37872"],["0","0","-65084","-165540","-135828","-35372"],["0","0","-30062","-79932","-69678","-19808"],["0","0","-8972","-24780","-22644","-6836"],["0","0","-1670","-4764","-4518","-1424"],["0","0","-176","-516","-504","-164"],["0","0","-8","-24","-24","-8"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","0"],["0","0","0","0","0","0","0"],["0","0","0","2700","8100","8100","2700"],["0","0","0","11070","33210","33210","11070"],["0","0","0","18936","56808","56808","18936"],["0","0","0","17686","53058","53058","17686"],["0","0","0","9904","29712","29712","9904"],["0","0","0","3418","10254","10254","3418"],["0","0","0","712","2136","2136","712"],["0","0","0","82","246","246","82"],["0","0","0","4","12","12","4"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","0","0","0"],["0","0","0","0","0","0"],["0","0","48600","97200","48600","0"],["0","0","288360","603720","342360","27000"],["0","0","760158","1660716","1040958","140400"],["0","0","1175436","2670102","1813896","319230"],["0","0","1184910","2788186","2021642","418366"],["0","0","817820","1986034","1518608","350394"],["0","0","394434","985050","786798","196182"],["0","0","132948","340326","281808","74430"],["0","0","30690","80286","68502","18906"],["0","0","4620","12318","10776","3078"],["0","0","408","1106","988","290"],["0","0","16","44","40","12"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0"],["0","0","0","0","0","0","0"],["0","0","0","-16200","-48600","-48600","-16200"],["0","0","0","-85320","-255960","-255960","-85320"],["0","0","0","-196506","-589518","-589518","-196506"],["0","0","0","-260808","-782424","-782424","-260808"],["0","0","0","-221098","-663294","-663294","-221098"],["0","0","0","-125208","-375624","-375624","-125208"],["0","0","0","-48006","-144018","-144018","-48006"],["0","0","0","-12312","-36936","-36936","-12312"],["0","0","0","-2022","-6066","-6066","-2022"],["0","0","0","-192","-576","-576","-192"],["0","0","0","-8","-24","-24","-8"]]},"deriv_order":1}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["1"]]},"start_base":1}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["0","0","2520","-156"],["0","0","3828","-274"],["0","0","2148","-170"],["0","0","528","-44"],["0","0","48","-4"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","0","0","840","18"],["0","0","0","1276","15"],["0","0","0","716","3"],["0","0","0","176","0"],["0","0","0","16","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["4200","-960","720"],["5960","-1424","1068"],["3152","-776","582"],["736","-184","138"],["64","-16","12"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-4200","-2190","-45"],["0","-5960","-3046","-33"],["0","-3152","-1588","-6"],["0","-736","-368","0"],["0","-64","-32","0"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["-2240","-864"],["-3216","-1224"],["-1688","-636"],["-384","-144"],["-32","-12"]]},"deriv_order":0,"shift":2},{"coeff":{"coeffs":[["0","1120","24"],["0","1608","18"],["0","844","3"],["0","192","0"],["0","16","0"]]},"deriv_order":1,"shift":2},{"coeff":{"coeffs":[["300"],["430"],["224"],["50"],["4"]]},"deriv_order":0,"shift":3}]},"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 >= 1 (the exceptional bases checked exactly), and agreement on the 2 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":[["0"],["2"],["15","6"]],"recurrence":{"denominator":{"coeffs":[["0"],["4"],["-10"],["2"],["4"]]},"terms":[{"coeff":{"coeffs":[["0","0","0","0"],["0","0","-12","10"],["0","0","12","-10"],["0","0","48","-4"],["0","0","-48","4"]]},"deriv_order":0,"offset":3,"sign":"none"},{"coeff":{"coeffs":[["0","0","0","0","0"],["0","0","0","-4","3"],["0","0","0","4","-3"],["0","0","0","16","0"],["0","0","0","-16","0"]]},"deriv_order":1,"offset":3,"sign":"none"},{"coeff":{"coeffs":[["0","0","0"],["-8","8","-6"],["16","-16","12"],["32","-8","6"],["-64","16","-12"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["0","0","0","0"],["0","8","-2","-3"],["0","-16","4","6"],["0","-32","-16","0"],["0","64","32","0"]]},"deriv_order":1,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["8","0"],["0","0"],["-40","-12"],["0","0"],["32","12"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","-4","3"],["0","0","0"],["0","20","-3"],["0","0","0"],["0","-16","0"]]},"deriv_order":1,"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 leader is not a nonzero constant","route":"periodic_product","success":false,"variant":"P_(n+k) = c(x) P_n"},{"detail":"not applicable: expected one nonzero lag term","route":"product_recurrence","success":false,"variant":"product_recurrence"},{"detail":"no theorem matched (weighted_renewal_window: LHS must be a nonzero constant; fixed_delay_predecessor_window: LHS must be a nonzero constant)","route":"paper_theorem","success":false,"variant":"match_recurrence_theorems"},{"detail":"not applicable: the rule is not f(n) P_n = c_1(n, x) P_(n-1) + c_2(n, x) P_(n-2) with both terms nonzero","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":"not applicable: the rule is not f(n) P_n = c_0(n, x) P_(n-1) + c_1(n, x) P'_(n-1) + c_2(n, x) P_(n-2) with a derivative or a lag term","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":"not applicable: the rule is not f(n) P_n = c_1(n, x) P_(n-1) + c_d(n, x) P'_(n-1) + c_2(n, x) P_(n-2) with a nonzero lag term and a nonzero P_(n-1) or P'_(n-1) term","route":"liu_wang_three_term","success":false,"variant":"liu_wang_three_term"}],"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"}