{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"intercept":"0","shape":"affine","slope":"1"},"parent":{"first_index":0,"initial_polynomials":[["1"],["4","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","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":[["-8","-2"],["5","2"],["-3","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-28","-28","-4"],["13","10","1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-13","-23","-11","-1"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["2"],["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":[["1"],["1"]]},"terms":[{"coeff":{"coeffs":[["16","4"],["-11","-2"],["3","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["41","38","5"],["-13","-10","-1"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["13","23","11","1"]]},"deriv_order":2,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["1"],"operator":{"intercept":"0","shape":"affine","slope":"1"},"parent":{"first_index":0,"initial_polynomials":[["1"],["4","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","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":[["-16","-4","0"],["13","1","-2"],["-3","3","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-41","-23","13","3"],["13","-3","-9","-1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-13","-10","12","10","1"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["4"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["52","144","136","48","4"],["0","52","92","44","4"],["-13","-10","12","10","1"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["1124864","9345024","34704384","75884544","108277248","105541632","71469056","33509376","10642944","2193408","273408","18432","512"],["-1687296","-10642944","-27396096","-34374144","-14214912","18318336","32790528","24148992","10150656","2523648","356352","26112","768"],["843648","3634176","4742400","-1253376","-8826240","-7440384","204288","4116480","2882688","930816","152832","12288","384"],["-140608","-324480","139776","859520","402624","-633600","-640512","-11520","217152","108160","21504","1920","64"]]},"step_quotients":[[{"coeff":{"coeffs":[["1687296","15142400","60839168","143858688","220948224","228647424","158606592","68962304","13739264","-2821632","-2717952","-795648","-117504","-8704","-256"],["-562432","670592","25630592","115222272","262932480","366690432","330241664","190796288","64511744","7570560","-3021696","-1452288","-254464","-20608","-640"],["-2530944","-21448128","-74418240","-132616320","-112491264","7059648","119381568","129053952","69117312","18663360","1123392","-695424","-181248","-17088","-576"],["2530944","13925600","26757536","11113536","-33736384","-53217376","-20899872","17421696","23279616","10720800","2112352","41536","-43968","-5792","-224"],["-878800","-2906800","-1084096","6407840","7818512","-1873360","-8164512","-3758400","1605456","2038960","701824","92320","1648","-560","-32"],["105456","137904","-348192","-539808","342672","777168","5184","-471744","-171504","81744","64992","14688","1392","48","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["-7874048","-72726784","-302548480","-746862848","-1211813376","-1349356800","-1040084480","-539434240","-168071680","-15289088","11226624","5608704","1246720","151808","9728","256"],["15466880","114995712","362514048","606496000","504785280","-1517568","-489481600","-580204800","-363806592","-137217536","-29753472","-2641152","267392","89088","8064","256"],["-11389248","-64247040","-133233984","-84796416","120374208","264957696","170887104","-25767936","-113932224","-82978560","-31790016","-7105536","-914112","-62208","-1728","0"],["3726112","14363648","11779040","-23338048","-47751904","-13179520","35850976","35984448","5279328","-10950400","-8358752","-2826176","-521888","-53888","-2912","-64"],["-456976","-949104","1014000","3453840","430512","-4330032","-2727248","1767888","2313936","374704","-496944","-307536","-76656","-9744","-624","-16"]]},"deriv_order":1},{"coeff":{"coeffs":[["-3655808","-33183488","-132777216","-302538496","-413855488","-296952576","27090688","318711040","386967552","271850240","127197440","40821504","8916736","1285888","115968","5888","128"],["5483712","38807808","110582784","144059136","22916352","-198270720","-287794176","-149636352","47251584","125424384","91554816","38009088","9848064","1598208","156672","8448","192"],["-2741856","-13920192","-21967296","5229120","55342272","55251264","-10489536","-58589376","-39854592","768192","16166592","10606272","3474240","650688","70080","4032","96"],["456976","1406080","-64896","-4467840","-3884352","3899520","7057280","959360","-4081824","-2688640","122240","804480","384192","86400","10368","640","16"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","281216","1492608","2792192","1163008","-3359872","-5422208","-2412032","1440256","2333056","1271168","361216","55040","4224","128"],["-843648","-4196608","-6602752","514560","12823424","12488960","-1128192","-9212928","-5490816","-108288","1148416","506368","93312","7936","256"],["-492128","-3666624","-9077536","-6449024","9422496","19999424","9843936","-5875968","-9143328","-4112704","-594528","100480","40928","4416","160"],["667888","2209168","807040","-4908896","-5925296","1526896","6253344","2780352","-1297008","-1550992","-507328","-57184","1328","656","32"],["-105456","-137904","348192","539808","-342672","-777168","-5184","471744","171504","-81744","-64992","-14688","-1392","-48","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["-281216","-2617472","-9043840","-13824384","-4084352","17698688","27460736","13630080","-5682048","-12043648","-7778944","-2771072","-585600","-72064","-4736","-128"],["3937024","22443200","46596992","28470080","-45199360","-94136128","-56026496","14568768","41654016","27163712","8960128","1501120","79360","-10688","-1664","-64"],["-2812160","-10637536","-8182720","17998688","34643840","7870496","-27045440","-25260192","-2718720","8133728","5786560","1862944","327040","31840","1600","32"],["456976","949104","-1014000","-3453840","-430512","4330032","2727248","-1767888","-2313936","-374704","496944","307536","76656","9744","624","16"]]},"deriv_order":1},{"coeff":{"coeffs":[["-1827904","-12935936","-36860928","-48019712","-7638784","66090240","95931392","49878784","-15750528","-41808128","-30518272","-12669696","-3282688","-532736","-52224","-2816","-64"],["1827904","9280128","14644864","-3486080","-36894848","-36834176","6993024","39059584","26569728","-512128","-10777728","-7070848","-2316160","-433792","-46720","-2688","-64"],["-456976","-1406080","64896","4467840","3884352","-3899520","-7057280","-959360","4081824","2688640","-122240","-804480","-384192","-86400","-10368","-640","-16"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["-10","-10","-4"],["19","7","-2"],["-3","3","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["30","66","42","6"],["-67","-69","-9","1"],["13","-3","-9","-1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["26","72","68","24","2"],["-13","-10","12","10","1"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["-26","-72","-68","-24","-2"],["13","10","-12","-10","-1"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["1124864","9345024","34704384","75884544","108277248","105541632","71469056","33509376","10642944","2193408","273408","18432","512"],["-1687296","-10642944","-27396096","-34374144","-14214912","18318336","32790528","24148992","10150656","2523648","356352","26112","768"],["843648","3634176","4742400","-1253376","-8826240","-7440384","204288","4116480","2882688","930816","152832","12288","384"],["-140608","-324480","139776","859520","402624","-633600","-640512","-11520","217152","108160","21504","1920","64"]]},"step_quotients":[[{"coeff":{"coeffs":[["1687296","14017536","50369280","99809280","110359296","44485632","-55212288","-108048384","-91239168","-46973952","-15554304","-3262464","-409344","-27648","-768"],["2812160","32080256","154404224","418953984","711304704","780493440","536441984","189106688","-17438464","-54448512","-27550080","-7156992","-1017856","-74368","-2176"],["-3937024","-22724416","-31919680","85496448","412081536","759302208","803965760","518854400","190046720","23201088","-10365888","-5099904","-914560","-75328","-2368"],["-1265472","-20004192","-96167136","-217116480","-238718976","-55585056","180788448","246876288","150676416","46911072","5042400","-1045824","-354432","-35808","-1248"],["2706704","17178512","38426336","24438560","-40143376","-81099280","-41598720","20440512","36344304","18762352","4308832","287008","-43760","-7664","-320"],["-984256","-3466528","-1709344","7366976","10054400","-1442656","-10070496","-5208192","1742400","2608672","961312","142144","6016","-416","-32"],["105456","137904","-348192","-539808","342672","777168","5184","-471744","-171504","81744","64992","14688","1392","48","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["-6749184","-57757440","-215494656","-449606400","-541246464","-288301824","176363520","487405824","473005056","279134976","109191168","28604160","4899840","519936","30720","768"],["-1406080","-50489088","-368314752","-1310933504","-2812758144","-3968823552","-3822377344","-2528483328","-1119099264","-302381312","-32942208","6895104","3135104","487680","35712","1024"],["15888704","147184128","566160192","1161039616","1281112128","457502208","-729406912","-1274565888","-993892416","-466416128","-137448000","-24656640","-2416960","-87552","3264","256"],["-13287456","-84235008","-200899296","-175139520","121581024","411981696","339209760","20465856","-175809888","-155377152","-68123040","-17462592","-2660448","-233088","-10656","-192"],["4183088","17140656","16389360","-25223568","-60429456","-22818576","41929264","48476592","10153872","-13392368","-11427888","-4096944","-793392","-85680","-4848","-112"],["-456976","-949104","1014000","3453840","430512","-4330032","-2727248","1767888","2313936","374704","-496944","-307536","-76656","-9744","-624","-16"]]},"deriv_order":1},{"coeff":{"coeffs":[["3655808","47806720","280134400","981004544","2302475520","3840994560","4704761600","4304778496","2961677824","1528924928","586176768","163762944","32381696","4345600","371968","18176","384"],["-9139520","-93926144","-420526080","-1066094848","-1632505600","-1386081024","-179431424","1125207808","1595121792","1212825344","600344576","201295104","45515008","6741760","620544","32000","704"],["8225568","63695424","199198272","293347392","101174976","-341290176","-586077888","-357862080","54648576","251616960","199276224","86624448","23170368","3847104","383424","20928","480"],["-3198832","-17154176","-29354624","2504320","69905344","77567872","-6928768","-77159808","-57221280","-1664384","21677696","14946176","5016512","953984","103808","6016","144"],["456976","1406080","-64896","-4467840","-3884352","3899520","7057280","959360","-4081824","-2688640","122240","804480","384192","86400","10368","640","16"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["1687296","14298752","54111616","121291520","180931072","192894848","155920000","100622848","53139200","22377856","7002752","1485568","192512","13440","384"],["1968512","20572032","88746112","212407040","315815808","308944000","209310336","109165056","53122176","25745536","10125696","2614016","387712","29568","896"],["-2741856","-14904448","-27121120","-6349824","42370592","54141824","9700512","-28388352","-24070944","-5705088","1615456","1183744","246624","22144","736"],["-456976","-5378256","-16835104","-16530592","12682896","39401552","25013568","-7712448","-18399984","-9759536","-2054688","-27296","50032","6576","256"],["773344","2768896","1432288","-5868032","-8161184","1096192","8159328","4230144","-1433952","-2120704","-766816","-107008","-3040","512","32"],["-105456","-137904","348192","539808","-342672","-777168","-5184","471744","171504","-81744","-64992","-14688","-1392","-48","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["-7030400","-62624640","-252227456","-609849472","-993425024","-1163642752","-1025246080","-702789760","-382531456","-165207680","-55136896","-13546880","-2296704","-247424","-14976","-384"],["3093376","10934976","-6406400","-90380736","-179363712","-133695296","36624896","154666560","134634624","58739264","12033792","-142144","-606336","-122304","-10240","-320"],["4921280","35049248","92105728","91207008","-44886208","-195006944","-171074432","-15531168","84932160","76097632","32850688","8095520","1147584","88672","3200","32"],["-3269136","-13414544","-12793040","19884208","47321392","17509552","-33123728","-37752336","-7593264","10575696","8855696","3133712","598544","63632","3536","80"],["456976","949104","-1014000","-3453840","-430512","4330032","2727248","-1767888","-2313936","-374704","496944","307536","76656","9744","624","16"]]},"deriv_order":1},{"coeff":{"coeffs":[["1827904","20247552","95916288","254518784","406216704","363042816","68840704","-268832256","-402718080","-313658368","-157715712","-53491200","-12199424","-1818624","-168192","-8704","-192"],["-3655808","-29527680","-95937920","-147545216","-59811200","161436544","294787200","188695936","-20681856","-125936512","-102332544","-45079936","-12164224","-2032000","-203392","-11136","-256"],["2284880","12514112","22032192","-761280","-51457920","-59150784","3432256","57630016","43936416","1920448","-16288832","-11410752","-3858432","-737088","-80448","-4672","-112"],["-456976","-1406080","64896","4467840","3884352","-3899520","-7057280","-959360","4081824","2688640","-122240","-804480","-384192","-86400","-10368","-640","-16"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["104","288","272","96","8"],["-52","-40","48","40","4"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-1","-1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-3","-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"],["4","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","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) = (3) + (1) x, V_n(x) = 0, W_n(x) = (1) + (1) x; open hypotheses: multipliers_vanish_at_zero: [x^0] c_2(n, x) = 1 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 = 1 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 = 1 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; 5 with the same first index and seeds differ in the rule or in later initial rows (oeis_catalog:A060923:lean_proved, oeis_catalog:A093561:lean_proved, oeis_catalog:A116414:lean_proved, oeis_catalog:A156308:lean_proved, oeis_catalog:A207823: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"}