{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"intercept":"0","shape":"affine","slope":"1"},"parent":{"first_index":0,"initial_polynomials":[["1"],["3","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"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":[["-6","-2"],["5","2"],["-2","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-20","-23","-4"],["8","8","1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-8","-16","-9","-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":[["13","4"],["-9","-2"],["2","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["28","31","5"],["-8","-8","-1"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["8","16","9","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"],["3","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"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":[["-6","-2","0"],["4","-2","-2"],["0","2","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-8","4","14","3"],["0","-8","-8","-1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","8","16","9","1"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["2"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["32","96","100","40","4"],["16","64","82","38","4"],["0","8","16","9","1"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["32768","294912","1191936","2850816","4474368","4827648","3644992","1921920","693696","164608","24000","1920","64"],["0","49152","393216","1394688","2881536","3830016","3411456","2056032","826848","213696","33216","2784","96"],["0","0","24576","172032","525312","915456","999552","706176","321840","91584","15264","1344","48"],["0","0","0","4096","24576","62976","89600","76992","40704","12936","2328","216","8"]]},"step_quotients":[[{"coeff":{"coeffs":[["32768","294912","1159168","2555904","3282432","1976832","-829376","-2905728","-2951296","-1757312","-669696","-162688","-23936","-1920","-64"],["65536","671744","3039232","7944192","13095936","13714176","8173184","887200","-2920288","-2741344","-1274720","-347680","-55072","-4640","-160"],["0","131072","1155072","4497408","10116096","14364672","13073280","7129216","1542480","-722688","-688688","-241152","-43536","-3968","-144"],["0","0","98304","765952","2617344","5124608","6284288","4921920","2357440","561624","-24408","-53136","-13360","-1416","-56"],["0","0","0","32768","225280","671744","1133056","1180160","774976","311424","68472","5088","-752","-160","-8"],["0","0","0","0","4096","24576","62976","89600","76992","40704","12936","2328","216","8","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["-131072","-1245184","-5259264","-12869632","-19728384","-18514944","-7961344","3979648","9144000","7364928","3577792","1131840","232512","29632","2112","64"],["0","-327680","-2981888","-12181504","-29405184","-46402560","-49900032","-36803200","-18036544","-5213888","-417856","289088","121408","21440","1856","64"],["0","0","-294912","-2506752","-9547776","-21473280","-31624704","-31958784","-22570560","-11129184","-3762720","-840384","-116352","-8928","-288","0"],["0","0","0","-114688","-892928","-3090432","-6255616","-8196352","-7265664","-4424416","-1842864","-514320","-92768","-10240","-624","-16"],["0","0","0","0","-16384","-114688","-352256","-622592","-697856","-515584","-253056","-81408","-16644","-2060","-140","-4"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","131072","1441792","7274496","22282240","46215168","68530176","74761216","60809216","36966432","16679136","5495456","1287264","205920","21152","1248","32"],["0","0","196608","1966080","8945664","24477696","44845056","57950208","54191616","37022208","18427440","6591264","1651920","278976","29904","1824","48"],["0","0","0","98304","884736","3588096","8650752","13771776","15203328","11892480","6618624","2595096","700536","125424","14064","888","24"],["0","0","0","0","16384","131072","466944","974848","1320448","1213440","768640","334464","98052","18704","2200","144","4"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","8192","81920","363520","945152","1598848","1845248","1479824","823152","311232","76768","11536","944","32"],["0","0","-16384","-102400","-231424","-118272","491776","1249600","1471264","1041432","464736","128848","20992","1816","64"],["0","0","-32768","-262144","-909312","-1777664","-2115584","-1511424","-537728","37248","125736","54176","10864","1056","40"],["0","0","0","-24576","-167936","-496640","-827904","-846976","-539584","-204144","-37944","0","1200","176","8"],["0","0","0","0","-4096","-24576","-62976","-89600","-76992","-40704","-12936","-2328","-216","-8","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","-32768","-319488","-1404928","-3679232","-6380032","-7703168","-6627392","-4087088","-1792464","-547072","-111840","-14384","-1040","-32"],["0","0","98304","819200","3039232","6598656","9261056","8743424","5581440","2338112","582312","55824","-10448","-3712","-408","-16"],["0","0","0","81920","630784","2156544","4305920","5555456","4838784","2887136","1173936","318216","55360","5840","336","8"],["0","0","0","0","16384","114688","352256","622592","697856","515584","253056","81408","16644","2060","140","4"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","-65536","-655360","-2981888","-8159232","-14948352","-19316736","-18063872","-12340736","-6142480","-2197088","-550640","-92992","-9968","-608","-16"],["0","0","0","-65536","-589824","-2392064","-5767168","-9181184","-10135552","-7928320","-4412416","-1730064","-467024","-83616","-9376","-592","-16"],["0","0","0","0","-16384","-131072","-466944","-974848","-1320448","-1213440","-768640","-334464","-98052","-18704","-2200","-144","-4"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["-8","-10","-4"],["8","2","-2"],["0","2","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["24","54","36","6"],["-24","-28","-4","1"],["0","-8","-8","-1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["16","48","50","20","2"],["0","8","16","9","1"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["-16","-48","-50","-20","-2"],["0","-8","-16","-9","-1"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["32768","294912","1191936","2850816","4474368","4827648","3644992","1921920","693696","164608","24000","1920","64"],["0","49152","393216","1394688","2881536","3830016","3411456","2056032","826848","213696","33216","2784","96"],["0","0","24576","172032","525312","915456","999552","706176","321840","91584","15264","1344","48"],["0","0","0","4096","24576","62976","89600","76992","40704","12936","2328","216","8"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","-98304","-983040","-4460544","-12128256","-21975552","-27906048","-25417920","-16700736","-7846848","-2574912","-565824","-77760","-5952","-192"],["131072","1179648","4489216","8896512","7766016","-4921344","-23452160","-33347328","-28207648","-15677888","-5800416","-1391488","-203744","-16320","-544"],["131072","1507328","7487488","21184512","37472256","42006528","27213568","4599040","-8638144","-8942096","-4354064","-1225120","-198368","-16976","-592"],["0","229376","2162688","8982528","21553152","32813568","32546304","20390080","6831360","-11616","-1061816","-452448","-88272","-8384","-312"],["0","0","147456","1196032","4257792","8708096","11224832","9374976","4972960","1518144","165744","-42816","-16192","-1920","-80"],["0","0","0","40960","286720","871424","1501184","1602944","1087360","459408","111936","12504","-88","-136","-8"],["0","0","0","0","4096","24576","62976","89600","76992","40704","12936","2328","216","8","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","294912","3047424","14364672","40845312","78054912","105693696","104159808","75520128","40241280","15571584","4272384","799104","95616","6528","192"],["-393216","-4259840","-20676608","-59269120","-111058944","-141622272","-122884608","-68458624","-18538528","4070080","6206240","2799872","699424","101312","7904","256"],["0","-720896","-7110656","-31621120","-83693568","-146528256","-178285056","-154035712","-94769344","-40936688","-11985712","-2213920","-217376","-4144","1040","64"],["0","0","-491520","-4374528","-17473536","-41306112","-64143360","-68652288","-51679104","-27419232","-10123848","-2531472","-410736","-40608","-2184","-48"],["0","0","0","-147456","-1171456","-4139008","-8557568","-11459840","-10390400","-6477280","-2764848","-791832","-146820","-16700","-1052","-28"],["0","0","0","0","-16384","-114688","-352256","-622592","-697856","-515584","-253056","-81408","-16644","-2060","-140","-4"]]},"deriv_order":1},{"coeff":{"coeffs":[["262144","3276800","18874368","66387968","159277056","275705856","355112960","345902080","256360512","144257568","61028320","19060896","4273632","660064","65952","3808","96"],["0","524288","5963776","31064064","98074624","209338368","318965760","356995072","297428480","184887936","85143984","28573088","6800976","1102656","114512","6816","176"],["0","0","393216","4030464","18776064","52543488","98340864","129672192","123586560","85936896","43473504","15777624","4004376","683376","73872","4536","120"],["0","0","0","131072","1196032","4915200","12001280","19337216","21591552","17070080","9593472","3794592","1032100","185936","20952","1328","36"],["0","0","0","0","16384","131072","466944","974848","1320448","1213440","768640","334464","98052","18704","2200","144","4"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["32768","327680","1527808","4419584","8880640","13097984","14545856","12239808","7740432","3603376","1193536","267296","37520","2928","96"],["65536","606208","2564096","6670336","12192768","16980224","18828160","16710752","11561408","5971064","2186816","534064","80224","6584","224"],["0","0","-90112","-655360","-2003968","-3222528","-2566784","-79616","1945360","2049360","1086168","330880","56992","5104","184"],["0","0","-65536","-552960","-2027520","-4225536","-5474304","-4494144","-2232512","-536376","37344","60016","15072","1608","64"],["0","0","0","-32768","-229376","-696320","-1196032","-1269760","-851968","-352128","-81408","-7416","536","152","8"],["0","0","0","0","-4096","-24576","-62976","-89600","-76992","-40704","-12936","-2328","-216","-8","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["-131072","-1376256","-6701056","-20086784","-41469952","-62431232","-70674176","-61045760","-40341312","-20240368","-7572816","-2050880","-384224","-46448","-3216","-96"],["0","65536","720896","3432448","9375744","16276480","18618880","13833344","5968320","631744","-867928","-567728","-169360","-27520","-2328","-80"],["0","0","229376","2064384","8310784","19730432","30648832","32660480","24334784","12678464","4544448","1083784","162912","14192","608","8"],["0","0","0","114688","909312","3205120","6607872","8818944","7963520","4940000","2095920","595728","109412","12300","764","20"],["0","0","0","0","16384","114688","352256","622592","697856","515584","253056","81408","16644","2060","140","4"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","-131072","-1507328","-7929856","-25264128","-54374400","-83478528","-94077952","-78873088","-49307168","-22821616","-7692544","-1837904","-298912","-31120","-1856","-48"],["0","0","-196608","-2031616","-9535488","-26869760","-50612224","-67131392","-64327168","-44950528","-22839856","-8321328","-2118944","-362592","-39280","-2416","-64"],["0","0","0","-98304","-901120","-3719168","-9117696","-14746624","-16523776","-13105920","-7387264","-2929560","-798588","-144128","-16264","-1032","-28"],["0","0","0","0","-16384","-131072","-466944","-974848","-1320448","-1213440","-768640","-334464","-98052","-18704","-2200","-144","-4"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["32","96","100","40","4"],["0","16","32","18","2"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-1","-1"]]},"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"],["3","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"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) = (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; 12 with the same first index and seeds differ in the rule or in later initial rows (oeis_catalog:A039692:lean_proved, oeis_catalog:A079638:lean_proved, oeis_catalog:A093560:lean_proved, oeis_catalog:A103327:lean_proved, oeis_catalog:A110441:lean_proved, oeis_catalog:A116412:lean_proved, oeis_catalog:A125662:lean_proved, oeis_catalog:A127893:lean_proved, oeis_catalog:A216182:lean_proved, oeis_catalog:A249139:lean_proved, oeis_catalog:A249253:lean_proved, oeis_catalog:A327997: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"}