{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"euler_polynomial"},"parent":{"first_index":1,"initial_polynomials":[["1"],["1","1"]],"recurrence":{"denominator":{"coeffs":[["0"],["1"],["2"]]},"terms":[{"coeff":{"coeffs":[["0","4"],["1","-23"],["2","13"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","-1","3"],["0","4","-27/2"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","0","2"],["0","0","-6"],["0","0","5/2"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"Triangle read by rows: T(n,k) = binomial(n+1,k+1)*binomial(2*n-k+1,k)/(n+1), 0<=k<=n."},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["0","-4"],["0","4"],["-2","24"],["-4","-36"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","4","-44"],["0","4","-56"],["0","-18","128"],["0","-4","-36"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0","8","-44"],["0","0","17","-90"],["0","0","-8","52"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["0","0","0","2","-8"],["0","0","0","5","-20"]]},"deriv_order":3,"shift":0},{"coeff":{"coeffs":[["0"],["0"],["2"],["4"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","0"],["0","0"],["0","2"],["0","4"]]},"deriv_order":1,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[1],"index_shift":0,"input":{"first_index":1,"initial_polynomials":[["1"]],"recurrence":{"denominator":{"coeffs":[["-2"],["8"],["-10"],["4"]]},"terms":[{"coeff":{"coeffs":[["-2","-52"],["8","152"],["-10","-132"],["4","36"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","8","-62"],["0","-18","134"],["0","8","-52"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","0","3","-12"],["0","0","-5","20"]]},"deriv_order":2,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":1,"multiplier":["0","0","9/4","15/2","37/4","5","1"],"operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"euler_polynomial"},"parent":{"first_index":1,"initial_polynomials":[["1"],["1","1"]],"recurrence":{"denominator":{"coeffs":[["0"],["1"],["2"]]},"terms":[{"coeff":{"coeffs":[["0","4"],["1","-23"],["2","13"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","-1","3"],["0","4","-27/2"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","0","2"],["0","0","-6"],["0","0","5/2"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_leader_shift":2,"parent_valid_from_base":1,"quotients":[],"row_annihilation":{"kind":"system","system":{"generators":[{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","-6"],["-6","14"],["-10","8"],["-4","-36"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","6","-30"],["0","4","-14"],["0","-8","52"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0","3","-12"],["0","0","5","-20"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["0"],["6"],["10"],["4"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0"],["0","0","0","0"],["0","0","0","0"],["0","0","-12","48"],["0","0","-44","176"],["0","0","-48","192"],["0","0","-16","64"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0"],["0","0","0","0","0"],["0","0","0","0","0"],["0","0","0","-12","48"],["0","0","0","-44","176"],["0","0","0","-48","192"],["0","0","0","-16","64"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["0","0","0","0","0","0","0"],["0","0","0","0","0","0","0"],["0","0","0","0","0","0","0"],["0","0","0","0","216","-1728","3456"],["0","0","0","0","1080","-8640","17280"],["0","0","0","0","2232","-17856","35712"],["0","0","0","0","2440","-19520","39040"],["0","0","0","0","1488","-11904","23808"],["0","0","0","0","480","-3840","7680"],["0","0","0","0","64","-512","1024"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0"],["0","0","0","0","0","-5760","46080","-92160"],["0","0","0","0","0","-27984","223872","-447744"],["0","0","0","0","0","-57352","458816","-917632"],["0","0","0","0","0","-64272","514176","-1028352"],["0","0","0","0","0","-42536","340288","-680576"],["0","0","0","0","0","-16624","132992","-265984"],["0","0","0","0","0","-3552","28416","-56832"],["0","0","0","0","0","-320","2560","-5120"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","5760","-60480","207360","-230400"],["0","0","0","0","0","27984","-279432","892224","-888960"],["0","0","0","0","0","57352","-532236","1504992","-1174720"],["0","0","0","0","0","64272","-531476","1166752","-276800"],["0","0","0","0","0","42536","-285948","245856","869440"],["0","0","0","0","0","16624","-68212","-252256","1036480"],["0","0","0","0","0","3552","4264","-204608","522880"],["0","0","0","0","0","320","5520","-59520","129280"],["0","0","0","0","0","0","800","-6400","12800"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","2880","-34560","138240","-184320"],["0","0","0","0","0","0","13992","-167904","671616","-895488"],["0","0","0","0","0","0","28676","-344112","1376448","-1835264"],["0","0","0","0","0","0","32136","-385632","1542528","-2056704"],["0","0","0","0","0","0","21268","-255216","1020864","-1361152"],["0","0","0","0","0","0","8312","-99744","398976","-531968"],["0","0","0","0","0","0","1776","-21312","85248","-113664"],["0","0","0","0","0","0","160","-1920","7680","-10240"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","17280","-181440","622080","-691200"],["0","0","0","0","0","112752","-1140696","3713472","-3818880"],["0","0","0","0","0","317736","-3062988","9252576","-8337600"],["0","0","0","0","0","507560","-4591416","12368448","-8494976"],["0","0","0","0","0","506320","-4203448","9324224","-2446208"],["0","0","0","0","0","326824","-2405640","3557568","3343232"],["0","0","0","0","0","136312","-838700","166624","4028736"],["0","0","0","0","0","35344","-161608","-403648","1938304"],["0","0","0","0","0","5152","-12624","-146304","457472"],["0","0","0","0","0","320","160","-16640","43520"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","8640","-103680","414720","-552960"],["0","0","0","0","0","0","56376","-676512","2706048","-3608064"],["0","0","0","0","0","0","155988","-1871856","7487424","-9983232"],["0","0","0","0","0","0","239788","-2877456","11509824","-15346432"],["0","0","0","0","0","0","224484","-2693808","10775232","-14366976"],["0","0","0","0","0","0","131276","-1575312","6301248","-8401664"],["0","0","0","0","0","0","46888","-562656","2250624","-3000832"],["0","0","0","0","0","0","9360","-112320","449280","-599040"],["0","0","0","0","0","0","800","-9600","38400","-51200"]]},"deriv_order":1}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["2"],["-8"],["10"],["-4"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-2","22"],["4","-32"],["0","12"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-4","22"],["0","2","-12"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["0","0","-1","4"]]},"deriv_order":3,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","0"],["0","0","0","0","0"],["0","0","0","72","-288"],["0","0","0","384","-1536"],["0","0","0","704","-2816"],["0","0","0","536","-2144"],["0","0","0","144","-576"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","-1296","15552","-62208","82944"],["0","0","0","0","0","0","-8640","103680","-414720","552960"],["0","0","0","0","0","0","-25056","300672","-1202688","1603584"],["0","0","0","0","0","0","-41280","495360","-1981440","2641920"],["0","0","0","0","0","0","-42256","507072","-2028288","2704384"],["0","0","0","0","0","0","-27520","330240","-1320960","1761280"],["0","0","0","0","0","0","-11136","133632","-534528","712704"],["0","0","0","0","0","0","-2560","30720","-122880","163840"],["0","0","0","0","0","0","-256","3072","-12288","16384"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","4320","-51840","207360","-276480"],["0","0","0","0","0","0","34128","-409536","1638144","-2184192"],["0","0","0","0","0","0","115920","-1391040","5564160","-7418880"],["0","0","0","0","0","0","223184","-2678208","10712832","-14283776"],["0","0","0","0","0","0","269200","-3230400","12921600","-17228800"],["0","0","0","0","0","0","211360","-2536320","10145280","-13527040"],["0","0","0","0","0","0","108160","-1297920","5191680","-6922240"],["0","0","0","0","0","0","34816","-417792","1671168","-2228224"],["0","0","0","0","0","0","6400","-76800","307200","-409600"],["0","0","0","0","0","0","512","-6144","24576","-32768"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","-4320","47520","-155520","69120","276480"],["0","0","0","0","0","0","-34128","401328","-1539648","1790208","525312"],["0","0","0","0","0","0","-115920","1402128","-5697216","7951104","-709632"],["0","0","0","0","0","0","-223184","2691760","-10875456","14934272","-867328"],["0","0","0","0","0","0","-269200","3131312","-11732544","12472576","6341632"],["0","0","0","0","0","0","-211360","2260832","-6839424","303616","17631232"],["0","0","0","0","0","0","-108160","970976","-1268352","-8771072","20924416"],["0","0","0","0","0","0","-34816","201344","926208","-8161280","13852672"],["0","0","0","0","0","0","-6400","-6400","691200","-3584000","5324800"],["0","0","0","0","0","0","-512","-11264","184320","-802816","1114112"],["0","0","0","0","0","0","0","-1536","18432","-73728","98304"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","4320","-73440","466560","-1313280","1382400"],["0","0","0","0","0","0","0","21168","-355536","2234304","-6227712","6497280"],["0","0","0","0","0","0","0","39456","-645264","3955392","-10771200","10994688"],["0","0","0","0","0","0","0","28352","-417040","2282688","-5501696","4916224"],["0","0","0","0","0","0","0","-10688","274992","-2273856","7727360","-9391104"],["0","0","0","0","0","0","0","-36464","702496","-4929408","15050240","-16955392"],["0","0","0","0","0","0","0","-30272","560768","-3823104","11417600","-12640256"],["0","0","0","0","0","0","0","-12800","233472","-1572864","4653056","-5111808"],["0","0","0","0","0","0","0","-2816","50944","-340992","1003520","-1097728"],["0","0","0","0","0","0","0","-256","4608","-30720","90112","-98304"]]},"deriv_order":2},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","2160","-34560","207360","-552960","552960"],["0","0","0","0","0","0","0","0","12744","-203904","1223424","-3262464","3262464"],["0","0","0","0","0","0","0","0","32472","-519552","3117312","-8312832","8312832"],["0","0","0","0","0","0","0","0","46648","-746368","4478208","-11941888","11941888"],["0","0","0","0","0","0","0","0","41304","-660864","3965184","-10573824","10573824"],["0","0","0","0","0","0","0","0","23072","-369152","2214912","-5906432","5906432"],["0","0","0","0","0","0","0","0","7936","-126976","761856","-2031616","2031616"],["0","0","0","0","0","0","0","0","1536","-24576","147456","-393216","393216"],["0","0","0","0","0","0","0","0","128","-2048","12288","-32768","32768"]]},"deriv_order":3}],[{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","-12960","142560","-466560","207360","829440"],["0","0","0","0","0","0","-123984","1441584","-5396544","5716224","2958336"],["0","0","0","0","0","0","-522720","6273504","-25100928","33495552","-55296"],["0","0","0","0","0","0","-1283280","15598272","-63984384","91677696","-12730368"],["0","0","0","0","0","0","-2039440","24679520","-100368000","140423680","-13199360"],["0","0","0","0","0","0","-2203264","26083184","-101484864","123921664","22782976"],["0","0","0","0","0","0","-1650480","18732256","-66340992","54102528","68704256"],["0","0","0","0","0","0","-856608","9078816","-26711424","-2800128","76830720"],["0","0","0","0","0","0","-301440","2870912","-5512704","-16533504","47767552"],["0","0","0","0","0","0","-68352","548608","-21504","-8663040","17383424"],["0","0","0","0","0","0","-8960","53248","221184","-2031616","3473408"],["0","0","0","0","0","0","-512","1536","30720","-188416","294912"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","12960","-220320","1399680","-3939840","4147200"],["0","0","0","0","0","0","0","85104","-1433808","9035712","-25249536","26403840"],["0","0","0","0","0","0","0","228528","-3782592","23452416","-64558080","66576384"],["0","0","0","0","0","0","0","307824","-4885248","29071872","-76886016","76247040"],["0","0","0","0","0","0","0","174640","-2299328","10826496","-20952064","13033472"],["0","0","0","0","0","0","0","-69536","1989712","-17201088","59903744","-73937920"],["0","0","0","0","0","0","0","-190528","3873056","-28185984","88356352","-101550080"],["0","0","0","0","0","0","0","-143616","2765952","-19404288","59234304","-66723840"],["0","0","0","0","0","0","0","-56576","1066240","-7363584","22212608","-24788992"],["0","0","0","0","0","0","0","-11776","219392","-1502208","4501504","-4997120"],["0","0","0","0","0","0","0","-1024","18944","-129024","385024","-425984"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","6480","-103680","622080","-1658880","1658880"],["0","0","0","0","0","0","0","0","49032","-784512","4707072","-12552192","12552192"],["0","0","0","0","0","0","0","0","161136","-2578176","15469056","-41250816","41250816"],["0","0","0","0","0","0","0","0","302304","-4836864","29021184","-77389824","77389824"],["0","0","0","0","0","0","0","0","357152","-5714432","34286592","-91430912","91430912"],["0","0","0","0","0","0","0","0","275736","-4411776","26470656","-70588416","70588416"],["0","0","0","0","0","0","0","0","139168","-2226688","13360128","-35627008","35627008"],["0","0","0","0","0","0","0","0","44288","-708608","4251648","-11337728","11337728"],["0","0","0","0","0","0","0","0","8064","-129024","774144","-2064384","2064384"],["0","0","0","0","0","0","0","0","640","-10240","61440","-163840","163840"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["0","0","-16","64"]]},"start_base":1}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["0","0","-4"],["0","0","-5/2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-10","-10"],["-9","-29"],["-2","-13"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-7","24"],["0","-4","27/2"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["10"],["9"],["2"]]},"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 1) and E the input rule gauged by lambda(n)/delta(n) and composed with (or conjugated through) T = f(n, theta) = 1 + (1) theta; so the candidate rows satisfy the input rule at every base n >= 1 (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 >= 1"},"method":"operator_division"},"status":"certified"},"input_first_index":1,"interlacing":{"reason":"no parent theorem report with an interlacing conclusion","status":"none"},"lean_declarations":["RealRooted.isMultiplierSequence_eval_of_roots_nonpos","RealRooted.isPFMultiplierSequence_eval_of_roots_nonpos","RealRooted.isMultiplierSequence_iff_preserves"],"lift_summary":{"hypotheses":[{"evidence":"the polynomial with ascending coefficients [1, 1] is fixed; exact check: real-rooted = true, coefficients of one sign = true","name":"euler_polynomial_roots_nonpositive","statement":"the polynomial in theta is real-rooted with every root <= 0 for every n >= n0","status":{"kind":"verified"}},{"evidence":"lambda(n) = 1","name":"gauge_finite_nonzero","statement":"lambda(n) is finite and nonzero for every n >= n0","status":{"kind":"verified"}},{"evidence":"delta(n) != 0 for every integer n in [1, +inf) (exact; Taylor shift: the coefficients of delta(n) at n = 1 + u have one sign)","name":"operator_coefficients_defined","sign_decision":{"certificate":{"condition":"nonzero","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1"]},"numerator":["1"],"range":{"first":"1","last":null}},"decision":"holds"},"statement":"the operator coefficients are finite at every n >= n0 (their denominators do not vanish)","status":{"kind":"verified"}}],"identity":{"method":"forward_division","status":"certified"},"input_first_index":1,"input_interlacing":{"reason":"no parent theorem report with an interlacing conclusion","status":"not_proved"},"lean_replay":"not_attempted","operation":{"description":"f(n, theta) = 1 + (1) theta","kind":"preserver_image","operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"euler_polynomial"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":1,"initial_polynomials":[["1"],["1","1"]],"recurrence":{"denominator":{"coeffs":[["0"],["1"],["2"]]},"terms":[{"coeff":{"coeffs":[["0","4"],["1","-23"],["2","13"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","-1","3"],["0","4","-27/2"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","0","2"],["0","0","-6"],["0","0","5/2"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"relation":"Q_n = lambda(n) T_n(P_(n+0)) with T = f(n, theta) = 1 + (1) theta, for every n >= 1"},"parent_proof":{"statement":"open: no route proved that every parent row P_n, n >= 1, 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 >= 1, 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":"Laguerre's theorem on multiplier sequences: if f is a real polynomial whose roots are all real and <= 0, then (f(k))_(k >= 0) is a multiplier sequence, so x^k -> f(k) x^k maps every real-rooted polynomial to a real-rooted polynomial or zero (Laguerre; see T. Craven and G. Csordas, Multiplier sequences for fields, Illinois J. Math. 21 (1977); Polya--Schur, Theorem 40 of P. Branden, arXiv:1410.6601: sum_k f(k) x^k / k! = f(theta) e^x = C e^x x^m prod (1 + x/a_j), a_j > 0); f(k) has one sign for k >= 0, so coefficients of one sign stay of one sign; applied to f(n, .) for each n"},"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":"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":"HypothesisFailed: P_n = A_n(x) P_(n-1) + V_n(x) P'_(n-1) + W_n(x) P_(n-2) for n >= 3, with A_n(x) = ((n^2 + 1/2 n)/(n^2 + 1/2 n)) + ((13/2 n^2 - 23/2 n + 2)/(n^2 + 1/2 n)) x, V_n(x) = ((2 n - 1/2)/(n^2 + 1/2 n)) x + ((-27/4 n + 3/2)/(n^2 + 1/2 n)) x^2, W_n(x) = ((5/4 n^2 - 3 n + 1)/(n^2 + 1/2 n)) x^2; open hypotheses: derivative_degree_step_nonnegative: fails at n = 14: lambda_n = (-1/4 n^2 + 7/2 n - 1)/(n^2 + 1/2 n) = -1/203 there (exact); lag_coefficient_nonpositive: W_n(x) = gamma(n) w(x) / f(n) with w(x) = 2 x^2, which is positive on (-inf, 0) (no root there, exact): fails at n = 3: gamma(n)/f(n) = (5/8 n^2 - 3/2 n + 1/2)/(n^2 + 1/2 n) = 13/84 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; 7 with the same first index and seeds differ in the rule or in later initial rows (oeis_catalog:A008288:lean_proved, oeis_catalog:A046716:lean_proved, oeis_catalog:A063967:lean_proved, oeis_catalog:A085478:lean_proved, oeis_catalog:A086645:lean_proved, oeis_catalog:A123160:lean_proved, oeis_catalog:A158909: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 >= 1, 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 = f(n, theta) = 1 + (1) theta for every n >= 1 is certified; the lift is Open (open: no route proved that every parent row P_n, n >= 1, is zero or real-rooted with coefficients of one sign; the first 10 parent rows pass the exact check (evidence only))"},"kind":"preserver_image"}