{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["1","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","1","-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"Triangle of coefficients of polynomials u(n,x) jointly generated with A112351; see the Formula section."},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["0","22","-49","24","11","-8"],["-2","42","-51","92","132","-96"],["-5","22","23","80","-192","0"],["-3","2","52","-96","0","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","24","-32","32","0","-88","64"],["-2","47","-18","22","36","32","0"],["-5","25","36","0","-128","0","0"],["-3","2","52","-96","0","0","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","2","17","8","-11","-80","64"],["0","5","33","-70","-96","128","0"],["0","3","13","-80","64","0","0"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["0","-11","30","-27","8"],["-1","0","13","-68","32"],["2","-9","-48","64","0"],["3","-20","32","0","0"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-11","30","-27","8"],["-1","0","13","-68","32"],["2","-9","-48","64","0"],["3","-20","32","0","0"]]},"deriv_order":1,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"denominator":{"coeffs":[["0","0","-63","105","-24"],["4","-42","205","-196","32"],["-7","51","-144","64","0"],["3","-20","32","0","0"]]},"terms":[{"coeff":{"coeffs":[["0","0","27","-108","313","-88"],["1","-4","-59","356","-516","96"],["-4","-16","133","-368","192","0"],["3","-2","-52","96","0","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","0","3","2","-149","208","-64"],["0","1","-7","-90","224","-128","0"],["0","-3","-13","80","-64","0","0"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["1"],"operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["1","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","1","-1"]]},"deriv_order":0,"offset":2,"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":[["-3","-3","0"],["-2","0","-16"],["3","-20","32"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","15","-36","48"],["-1","-2","40","-64"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","1","3","-36","32"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["3"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","-33","-306","801","5004","-25551","50238","-53649","32904","-10944","1536"],["0","0","-3","-102","-393","4392","4155","-89646","267345","-378804","289056","-114432","18432"],["0","0","0","-42","-264","1476","-3912","-40314","291168","-681648","737664","-377856","73728"],["0","0","18","84","-1512","-3276","39222","-21816","-132336","62784","290304","-331776","98304"],["0","0","24","51","-2166","1827","57048","-191184","66816","411648","-540672","196608","0"],["0","0","9","-6","-831","2988","16464","-124608","290304","-282624","98304","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-33","-306","801","5004","-25551","50238","-53649","32904","-10944","1536"],["0","0","-3","-102","-393","4392","4155","-89646","267345","-378804","289056","-114432","18432"],["0","0","0","-42","-264","1476","-3912","-40314","291168","-681648","737664","-377856","73728"],["0","0","18","84","-1512","-3276","39222","-21816","-132336","62784","290304","-331776","98304"],["0","0","24","51","-2166","1827","57048","-191184","66816","411648","-540672","196608","0"],["0","0","9","-6","-831","2988","16464","-124608","290304","-282624","98304","0","0"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["0","0","0","27","486","1701","-8100","-17739","113238","-202581","176904","-77760","13824"],["0","0","0","81","1215","486","-44226","-243","552339","-1414260","1547424","-808704","165888"],["0","0","0","81","972","-3402","-49572","127089","680400","-2943216","4261248","-2737152","663552"],["0","0","0","27","243","-2187","-14175","94284","151632","-1736640","3608064","-2985984","884736"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","9","9","-2043","-9747","49059","95067","-803817","1810863","-2108808","1388736","-493056","73728"],["0","0","0","63","234","-10071","-36720","364689","207522","-5666409","16224516","-22284720","16776576","-6681600","1105920"],["0","0","0","162","711","-21717","-52326","956664","-580581","-14559669","54220212","-88513344","76640256","-34430976","6340608"],["0","0","0","198","819","-24912","-30726","1175850","-2057589","-16997256","84530736","-164471040","164081664","-83312640","17104896"],["0","0","0","117","396","-14742","-2376","701001","-1977372","-8952336","61532352","-142414848","163086336","-93192192","21233664"],["0","0","0","27","63","-3519","2997","165456","-628128","-1741824","16803072","-45563904","59277312","-37748736","9437184"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-9","-45","1575","10575","-29511","-134487","577773","-691227","-81540","974736","-987264","433152","-73728"],["0","0","0","-36","-234","4680","25506","-173772","-416934","3028752","-3942162","-3065256","12773952","-13432320","6377472","-1179648"],["0","0","0","-54","-432","5562","31536","-256770","-508032","5406750","-6148224","-19577376","60583680","-67405824","34947072","-7077888"],["0","0","0","-36","-342","3384","25452","-172476","-549126","4716792","-2126304","-42180480","122047488","-147234816","84344832","-18874368"],["0","0","0","-9","-99","927","8847","-56322","-255744","2037312","-34560","-27800064","86851584","-117374976","75497472","-18874368"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","9","189","729","-6543","-29241","135351","172179","-1691685","3789828","-4356864","2833920","-995328","147456"],["0","0","0","0","27","486","405","-27972","-37179","719766","-387909","-7529112","24140592","-34407936","26376192","-10616832","1769472"],["0","0","0","0","27","405","-1134","-30726","43983","912465","-2354508","-8331984","45925056","-85045248","78962688","-37158912","7077888"],["0","0","0","0","9","108","-810","-9540","46089","291600","-1709856","-1347840","25069824","-64512000","75202560","-42467328","9437184"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","-9","-63","882","3186","-40149","17037","648540","-2410992","3979584","-3488256","1585152","-294912"],["0","0","0","-54","-279","6300","12798","-293922","367713","4440420","-19575216","35626176","-33744384","16404480","-3244032"],["0","0","0","-108","-405","13716","10530","-651240","1416123","9036360","-50757840","105463296","-110536704","58392576","-12386304"],["0","0","0","-90","-252","11736","-3132","-560574","1745496","6911136","-51152256","121568256","-141631488","81985536","-18874368"],["0","0","0","-27","-63","3519","-2997","-165456","628128","1741824","-16803072","45563904","-59277312","37748736","-9437184"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","9","45","-1116","-2610","52353","-35775","-850014","2970324","-3970080","1841472","769536","-1069056","294912"],["0","0","0","27","162","-3132","-9936","148959","-12474","-2690982","7531056","-3843936","-12842496","23224320","-15040512","3538944"],["0","0","0","27","216","-2862","-15444","147339","249156","-3623616","4427136","23618304","-81644544","104620032","-61931520","14155776"],["0","0","0","9","99","-927","-8847","56322","255744","-2037312","34560","27800064","-86851584","117374976","-75497472","18874368"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","-9","-162","-135","9324","12393","-239922","129303","2509704","-8046864","11469312","-8792064","3538944","-589824"],["0","0","0","0","-18","-270","756","20484","-29322","-608310","1569672","5554656","-30616704","56696832","-52641792","24772608","-4718592"],["0","0","0","0","-9","-108","810","9540","-46089","-291600","1709856","1347840","-25069824","64512000","-75202560","42467328","-9437184"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["-2","9","-4"],["1","-11","-8"],["3","-20","32"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","12","-24","12"],["-1","10","-14","32"],["-1","-2","40","-64"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","1","6","-15","8"],["0","1","3","-36","32"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","0","18","294","927","-3636","-4788","40266","-97029","129708","-98784","39168","-6144"],["0","0","66","834","330","-16902","15492","75372","-291096","536160","-535296","264192","-49152"],["0","0","69","702","-1425","-16236","37002","-14880","-15408","196032","-468480","380928","-98304"],["0","0","12","168","84","-5904","-8760","73920","72576","-500736","565248","-196608","0"],["0","0","-9","6","831","-2988","-16464","124608","-290304","282624","-98304","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","33","207","-1818","-3618","41949","-110493","144108","-103392","39168","-6144"],["0","0","3","60","-30","-3348","6411","56256","-291384","570720","-553728","264192","-49152"],["0","0","-3","-9","357","1053","-8934","-14880","49104","159168","-468480","380928","-98304"],["0","0","-15","-30","1425","-972","-40152","117696","54144","-500736","565248","-196608","0"],["0","0","-9","6","831","-2988","-16464","124608","-290304","282624","-98304","0","0"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["0","0","0","27","486","1701","-8100","-17739","113238","-202581","176904","-77760","13824"],["0","0","0","81","1215","486","-44226","-243","552339","-1414260","1547424","-808704","165888"],["0","0","0","81","972","-3402","-49572","127089","680400","-2943216","4261248","-2737152","663552"],["0","0","0","27","243","-2187","-14175","94284","151632","-1736640","3608064","-2985984","884736"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","18","126","-2250","-14634","58914","151578","-1083726","2358450","-2699676","1758816","-619776","92160"],["0","0","0","135","1017","-14085","-78327","514377","641331","-8807535","23413995","-30985308","22772448","-8914176","1456128"],["0","0","0","387","2709","-39951","-168345","1695789","293355","-27669249","90714681","-138991680","115376256","-50245632","9031680"],["0","0","0","558","3348","-60876","-170640","2768094","-2297268","-42747696","175356576","-310711680","290589696","-140451840","27721728"],["0","0","0","432","2070","-50508","-73872","2369196","-4310118","-33795792","177609888","-363267072","380768256","-202899456","43646976"],["0","0","0","171","603","-21267","-4887","1006884","-2837376","-12735360","88715520","-208825344","243818496","-142147584","33030144"],["0","0","0","27","63","-3519","2997","165456","-628128","-1741824","16803072","-45563904","59277312","-37748736","9437184"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-18","-144","2124","16884","-44280","-210492","932148","-1274724","341226","940860","-1139040","527616","-92160"],["0","0","0","-81","-702","7695","54324","-279045","-783918","5217777","-7613352","-1418634","15163200","-17093376","8294400","-1548288"],["0","0","0","-144","-1341","11997","87282","-516726","-1328265","10770489","-13108284","-26358912","88016256","-97606656","50061312","-10027008"],["0","0","0","-126","-1251","10332","85302","-482490","-1659339","12055716","-5959440","-82790208","226566144","-259301376","142147584","-30670848"],["0","0","0","-54","-567","4833","44307","-253935","-1104840","7847280","139968","-88542720","249302016","-307224576","182255616","-42467328"],["0","0","0","-9","-99","927","8847","-56322","-255744","2037312","-34560","-27800064","86851584","-117374976","75497472","-18874368"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","18","405","2133","-8199","-58563","182655","398223","-2651373","5432589","-5932512","3722112","-1271808","184320"],["0","0","0","0","63","1242","3321","-54144","-154143","1261170","300807","-14295852","39299904","-51835392","37711872","-14598144","2359296"],["0","0","0","0","81","1377","-324","-86670","-30375","2351997","-3130326","-23390208","94206240","-153861120","131715072","-58392576","10616832"],["0","0","0","0","45","648","-2322","-50508","104733","1508220","-4849200","-12457152","86303232","-177905664","180486144","-92012544","18874368"],["0","0","0","0","9","108","-810","-9540","46089","291600","-1709856","-1347840","25069824","-64512000","75202560","-42467328","9437184"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","-18","-234","9","2727","-40608","28404","772929","-3006369","5026968","-4410432","1995264","-368640"],["0","0","0","-117","-1053","7623","33966","-416907","303075","6991569","-28522044","50305968","-46664064","22311936","-4349952"],["0","0","0","-270","-1710","27009","67068","-1272888","1743822","19289421","-91548900","177201216","-177389568","90611712","-18726912"],["0","0","0","-288","-1287","34056","36666","-1604232","3464181","22093992","-127834416","274675968","-298414080","163528704","-35979264"],["0","0","0","-144","-459","18261","-621","-866457","2605500","10694160","-78335424","187978752","-222363648","130940928","-30670848"],["0","0","0","-27","-63","3519","-2997","-165456","628128","1741824","-16803072","45563904","-59277312","37748736","-9437184"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","18","144","-1287","-2007","92880","-66366","-1485135","5068197","-6776028","3541680","540288","-1281024","368640"],["0","0","0","63","504","-5328","-21834","268947","-67608","-4985874","15479154","-13800888","-10188864","28251648","-19648512","4718592"],["0","0","0","81","702","-7344","-44064","352917","577530","-7898958","12242016","30339360","-121326336","157870080","-93339648","21233664"],["0","0","0","45","441","-4311","-34299","228798","804870","-6754104","2160864","69980544","-208899072","264609792","-159842304","37748736"],["0","0","0","9","99","-927","-8847","56322","255744","-2037312","34560","27800064","-86851584","117374976","-75497472","18874368"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","-18","-351","-864","15867","41634","-375273","-42876","4201389","-11836692","15826176","-11625984","4534272","-737280"],["0","0","0","0","-45","-756","351","48456","7857","-1328076","1957581","13083768","-54757296","91104768","-79017984","35389440","-6488064"],["0","0","0","0","-36","-513","1944","40266","-90072","-1204065","4064364","9679824","-70994880","149557248","-154165248","79626240","-16515072"],["0","0","0","0","-9","-108","810","9540","-46089","-291600","1709856","1347840","-25069824","64512000","-75202560","42467328","-9437184"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["0","0","9","108","54","-1476","2889","-2160","576"],["0","0","18","162","-594","-3978","13608","-13824","4608"],["0","0","9","54","-567","-1368","13392","-20736","9216"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["0","-1","1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-1","-2"]]},"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 = phi(n, D) = 1 + (1) D; 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":{"from_index":1,"justification":"the parent theorem (LiuWangDerivativeLag) proves P_(m-1) strictly interlacing P_m for every m >= 1; T = phi(n, D) = 1 + (1) D is independent of n and maps every real-rooted polynomial to a real-rooted polynomial or zero, so by the Hermite--Kakeya--Obreschkoff theorem (both directions) T(P_(m-1)) and T(P_m) have weakly interlacing zeros; the nonzero gauge does not move zeros, so Q_(n-1) and Q_n interlace weakly (orientation not determined) for every n >= 1","kind":"weak","orientation":"unordered","status":"claimed"},"lean_declarations":["RealRooted.splits_add_C_mul_derivative_all","RealRooted.splits_C_mul_add_derivative","Polynomial.Splits.derivative"],"lift_summary":{"hypotheses":[{"evidence":"the polynomial with ascending coefficients [1, 1] is fixed; exact check: real-rooted = true, coefficients of one sign = true","name":"derivative_polynomial_real_rooted","statement":"the polynomial in D is real-rooted 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 [0, +inf) (exact; Taylor shift: the coefficients of delta(n) at n = 0 + 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":"0","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":0,"input_interlacing":{"interlacing":{"from_index":1,"justification":{"premises":["the parent theorem (LiuWangDerivativeLag) proves P_(m-1) strictly interlacing P_m for every m >= 1; T = phi(n, D) = 1 + (1) D is independent of n and maps every real-rooted polynomial to a real-rooted polynomial or zero, so by the Hermite--Kakeya--Obreschkoff theorem (both directions) T(P_(m-1)) and T(P_m) have weakly interlacing zeros; the nonzero gauge does not move zeros, so Q_(n-1) and Q_n interlace weakly (orientation not determined) for every n >= 1"],"theorem":"Hermite--Kakeya--Obreschkoff theorem (N. Obreschkoff, Verteilung und Berechnung der Nullstellen reeller Polynome, 1963; see S. Fisk, Polynomials, Roots, and Interlacing, arXiv:math/0612833): real polynomials f, g have weakly interlacing zeros iff alpha f + beta g is real-rooted or zero for all real alpha, beta; a linear T independent of n that maps every real-rooted polynomial to a real-rooted polynomial or zero therefore maps interlacing pairs to pairs with weakly interlacing zeros (orientation not determined)"},"kind":"weak","orientation":"unordered"},"status":"proved"},"lean_replay":"not_attempted","operation":{"description":"phi(n, D) = 1 + (1) D","kind":"preserver_image","operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["1","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","1","-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"relation":"Q_n = lambda(n) T_n(P_(n+0)) with T = phi(n, D) = 1 + (1) D, for every n >= 0"},"parent_proof":{"route":"liu_wang_derivative_lag","statement":"every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign","status":"proved"},"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":"Laguerre's theorem on differential operators: if phi is a real polynomial with only real roots, then phi(D) maps every real-rooted polynomial to a real-rooted polynomial or zero (write phi(D) = C D^j prod (1 + c_i D); D preserves real-rootedness by Rolle's theorem and p + c p' is real-rooted for every real c by Rolle's theorem applied to e^(x/c) p; Polya--Schur 1914); when the coefficients of phi have one sign, coefficients of one sign stay of one sign; applied to phi(n, .) for each n"},"verdict":"proved"},"notes":["the division remainder is removed by row annihilators of the shifted parent"],"parent_interlacing_report":{"conclusion":{"first_index":0,"interlacing":"strict","interlacing_from":1,"root_region":{"upper":{"closed":false,"value":"0"}},"simple_roots":true,"statement":"every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0) (so its coefficients have one sign); for n >= 1, P_n has simple roots and P_(n-1) strictly interlaces P_n (no common root), and deg P_n = deg P_(n-1) + 1 for n >= 2"},"hypotheses":[{"evidence":"checked exactly","name":"seed_roots_negative","statement":"P_0 and P_1 are nonzero and real-rooted with every root < 0","status":{"kind":"verified"}},{"evidence":"degrees 0 and 1, leading coefficients of one sign","name":"seed_degree_step","statement":"deg P_1 = deg P_0 + 1, with leading coefficients of one sign","status":{"kind":"verified"}},{"evidence":"Bezout test, exact","name":"seed_strict_interlacing","statement":"P_0 strictly interlaces P_1 (simple real roots, no common root)","status":{"kind":"verified"}},{"evidence":"shared degree-law certificate, route recurrence (RealRooted RealRooted.LinRec.natDegree_eq_and_leadingCoeff_pos_of_ratio, RealRooted.ScalarRec.pos_of_ratio): the degree law deg P_n = 0 + 1 (n - 0) with positive leading coefficient for n >= 0 (route recurrence, induction from n = 2); every row is nonzero; lead P_n = 1 for every n >= 0; degree steps {1} from n = 1; the certificate is recomputed when the report is replayed","name":"degree_law","statement":"deg P_n = deg P_(n-1) + 1 with leading coefficients of one sign for every n >= 1","status":{"kind":"verified"}},{"evidence":"[x^0] c_1 and [x^0] c_2 are zero polynomials","name":"multipliers_vanish_at_zero","statement":"V_n(0) = 0 and W_n(0) = 0 for every n >= 2","status":{"kind":"verified"}},{"evidence":"A_n(0) = 1 > 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of A_n(0) = 1 at n = 2 + u have one sign)","name":"constant_term_positive","sign_decision":{"certificate":{"condition":"positive","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1"]},"numerator":["1"],"range":{"first":"2","last":null}},"decision":"holds"},"statement":"A_n(0) > 0 for every n >= 2","status":{"kind":"verified"}},{"evidence":"V_n = 0","name":"derivative_coefficient_nonpositive","statement":"V_n(x) <= 0 for every x < 0 and every n >= 2","status":{"kind":"verified"}},{"evidence":"W_n(x) = gamma(n) w(x) / f(n) with w(x) = -x^2 + x, which is negative on (-inf, 0) (no root there, exact): gamma(n)/f(n) = 1 >= 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of gamma(n)/f(n) = 1 at n = 2 + u have one sign)","name":"lag_coefficient_nonpositive","sign_decision":{"certificate":{"condition":"nonnegative","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1"]},"numerator":["1"],"range":{"first":"2","last":null}},"decision":"holds"},"statement":"W_n(x) <= 0 for every x < 0 and every n >= 2","status":{"kind":"verified"}},{"evidence":"W_n(x) = gamma(n) w(x) / f(n) with w(x) = -x^2 + x, which is negative on (-inf, 0) (no root there, exact): gamma(n)/f(n) = 1 > 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of gamma(n)/f(n) = 1 at n = 2 + u have one sign)","name":"derivative_or_lag_coefficient_negative","sign_decision":{"certificate":{"condition":"positive","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1"]},"numerator":["1"],"range":{"first":"2","last":null}},"decision":"holds"},"statement":"for every n >= 2 and x < 0, V_n(x) < 0 or W_n(x) < 0 (V_n < 0 on (-inf, 0) for every n, or W_n < 0 there for every n)","status":{"kind":"verified"}}],"lean_declarations":["RealRooted.threeTerm_interlaces_of_nonnegCoeffs","RealRooted.LiuWang.strictInterl_nonpos_lag_sequence"],"lean_replay":"not_attempted","lean_route":"sign","normal_form":"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) = (1) + (2) x, V_n(x) = 0, W_n(x) = (1) x + (-1) x^2","recurrence":{"first_index":0,"initial_polynomials":[["1"],["1","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","1","-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"reference":"L. L. Liu and Y. Wang, A unified approach to polynomial sequences with only real zeros, Adv. in Appl. Math. 38 (2007) 542-560, Theorem 2.1 with the interlacers f' and the lag row (strict form, as in the derivative-lag theorems of the RealRooted library, https://github.com/PerAlexandersson/RealRooted), with nonnegativity of the coefficients replaced by an exact induction keeping every root in (-inf, 0)","schema":"polytool.recurrence-real-rootedness-theorem.v1","status":"proved","theorem":"liu_wang_derivative_lag"},"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":"not applicable: expected one nonzero lag term","route":"product_recurrence","success":false,"variant":"product_recurrence"},{"detail":"no theorem matched (weighted_renewal_window: support must satisfy offset = 1 + ell * t_degree; fixed_delay_predecessor_window: more than one weighted lag)","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":"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) = (1) + (2) x, V_n(x) = 0, W_n(x) = (1) x + (-1) x^2: every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0) (so its coefficients have one sign); for n >= 1, P_n has simple roots and P_(n-1) strictly interlaces P_n (no common root), and deg P_n = deg P_(n-1) + 1 for n >= 2","route":"liu_wang_derivative_lag","success":true,"variant":"liu_wang_derivative_lag"}],"conditional_on":[],"interlacing":{"from_index":1,"justification":{"premises":["every hypothesis of the theorem is verified exactly for every index: 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) = (1) + (2) x, V_n(x) = 0, W_n(x) = (1) x + (-1) x^2","every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0) (so its coefficients have one sign); for n >= 1, P_n has simple roots and P_(n-1) strictly interlaces P_n (no common root), and deg P_n = deg P_(n-1) + 1 for n >= 2"],"theorem":"liu_wang_derivative_lag: L. L. Liu and Y. Wang, A unified approach to polynomial sequences with only real zeros, Adv. in Appl. Math. 38 (2007) 542-560, Theorem 2.1 with the interlacers f' and the lag row (strict form, as in the derivative-lag theorems of the RealRooted library, https://github.com/PerAlexandersson/RealRooted), with nonnegativity of the coefficients replaced by an exact induction keeping every root in (-inf, 0)"},"kind":"strict","orientation":"previous_interlaces_next"},"route":"liu_wang_derivative_lag","rows_checked":10,"statement":"every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign","status":"proved"},"rows_compared":16,"schema":"polytool.recurrence-preserver-image.v1","statement":"proved: Q_n = lambda(n) T_n(P_(n+0)) with T = phi(n, D) = 1 + (1) D for every n >= 0, the side conditions hold for every n, and every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign; so every Q_n, n >= 0, is zero or real-rooted with roots in (-inf, 0]"},"kind":"preserver_image"}