{"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"],["5","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","2"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"basis_map_A007318 of Triangular array:  row n gives the coefficients of the polynomial p(n,x) defined in Comments."},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["72","302","408","200","32"],["200","471","450","180","24"],["151","226","116","24","0"],["28","24","0","0","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-761","-2582","-3575","-2612","-1040","-208","-16"],["-293","-942","-1054","-564","-152","-16","0"],["83","78","20","8","0","0","0"],["28","24","0","0","0","0","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-833","-2884","-3983","-2812","-1072","-208","-16"],["-493","-1413","-1504","-744","-176","-16","0"],["-68","-148","-96","-16","0","0","0"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["-8","-30","-32","-8","0"],["12","73","86","44","8"],["29","78","44","8","0"],["4","8","0","0","0"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["-8","-30","-32","-8","0"],["12","73","86","44","8"],["29","78","44","8","0"],["4","8","0","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":[["5","-33","-74","-44","-8"],["-34","-59","-2","28","8"],["17","54","44","8","0"],["4","8","0","0","0"]]},"terms":[{"coeff":{"coeffs":[["5","-33","-74","-44","-8"],["18","-91","-218","-132","-24"],["-67","-154","-116","-24","0"],["-28","-24","0","0","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["408","1619","2575","2084","896","192","16"],["357","1117","1312","712","176","16","0"],["68","148","96","16","0","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"],["5","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","2"]]},"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":[["-20","-16"],["-20","-24"],["-4","-8"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["21","26","-4","-8"],["17","54","44","8"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-17","-71","-98","-52","-8"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["4"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["-36992","-299744","-1031488","-1974624","-2309120","-1701760","-785408","-217600","-32768","-2048","0","0","0"],["92480","952816","3917504","8891248","12588192","11705536","7241856","2929920","736768","103424","6144","0","0"],["69360","142392","-1252032","-6714920","-15130464","-19951296","-16925568","-9522176","-3527168","-822272","-108544","-6144","0"],["-101728","-894812","-3168976","-5630156","-4540216","870592","5792384","6247808","3692288","1345536","301056","37888","2048"],["15028","215696","1239428","3862056","7341824","9002496","7296128","3922176","1377280","303104","37888","2048","0"],["4624","47872","211216","518880","778048","733568","430848","150016","27648","2048","0","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["-36992","-299744","-1031488","-1974624","-2309120","-1701760","-785408","-217600","-32768","-2048","0","0","0"],["92480","952816","3917504","8891248","12588192","11705536","7241856","2929920","736768","103424","6144","0","0"],["69360","142392","-1252032","-6714920","-15130464","-19951296","-16925568","-9522176","-3527168","-822272","-108544","-6144","0"],["-101728","-894812","-3168976","-5630156","-4540216","870592","5792384","6247808","3692288","1345536","301056","37888","2048"],["15028","215696","1239428","3862056","7341824","9002496","7296128","3922176","1377280","303104","37888","2048","0"],["4624","47872","211216","518880","778048","733568","430848","150016","27648","2048","0","0","0"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["-2515456","-16424448","-46401024","-74084864","-73236480","-46159872","-18407424","-4448256","-589824","-32768","0","0","0"],["3773184","32183040","118874880","250330368","332109312","288949248","166090752","61894656","14229504","1818624","98304","0","0"],["-1886592","-19864704","-91620480","-244040064","-416385024","-476583936","-371994624","-197038080","-69009408","-15138816","-1867776","-98304","0"],["314432","3939648","21891648","71213504","150744192","218225664","220860416","156837888","77180928","25526272","5357568","638976","32768"]]},"step_quotients":[[{"coeff":{"coeffs":[["20123648","156550144","535452672","1056689152","1326740480","1101643776","608858112","219660288","49201152","6160384","327680","0","0","0"],["-12577280","-155070464","-783777792","-2208787456","-3906674176","-4577203200","-3627767808","-1940852736","-684171264","-150716416","-18644992","-983040","0","0"],["-8804096","-63774208","-143093760","94350848","1164818176","2825416704","3800395776","3243343872","1813389312","657391616","147521536","18481152","983040","0"],["6917504","83527936","442219776","1347780608","2604237184","3293522688","2676672512","1241829376","129601536","-210231296","-137396224","-39518208","-5668864","-327680"],["-314432","-7083968","-61288128","-290129984","-862879232","-1725667584","-2403117056","-2365442048","-1645559808","-797335552","-260620288","-54214656","-6422528","-327680"],["-314432","-4568512","-29770944","-114996800","-293171200","-519714048","-657311744","-598558720","-390856704","-179888128","-56410112","-11354112","-1310720","-65536"]]},"deriv_order":0},{"coeff":{"coeffs":[["-23896832","-206341376","-794453248","-1796071168","-2641454080","-2644097024","-1830432768","-872005632","-278642688","-56590336","-6553600","-327680","0","0","0","0"],["25154560","277440000","1364099584","3950492160","7495733760","9797900288","9022779392","5877669888","2676621312","826966016","163774464","18612224","917504","0","0","0"],["-1886592","-38730624","-305360256","-1319162496","-3589749504","-6592754688","-8468914176","-7729655808","-5015347200","-2281537536","-705331200","-139886592","-15925248","-786432","0","0"],["-5030912","-66178688","-388405120","-1342573952","-3036475520","-4714198528","-5113046528","-3845107712","-1919832064","-552878080","-32260096","38305792","14516224","2228224","131072","0"],["1336336","20988336","149683504","642159632","1850732544","3789637504","5685316352","6350147328","5311246336","3317366784","1530040320","510193664","118751232","18186240","1638400","65536"]]},"deriv_order":1},{"coeff":{"coeffs":[["10690688","114453248","550366976","1573578752","2981635200","3947268352","3747768320","2576797696","1278996480","451207168","109674496","17367040","1605632","65536","0","0","0"],["-16036032","-203751936","-1168910208","-4011469056","-9193189056","-14865808128","-17463457536","-15108501504","-9648887808","-4513800192","-1518133248","-355074048","-54509568","-4915200","-196608","0","0"],["8018016","117912000","788207040","3174644736","8608063584","16626093120","23597536896","25017708288","19932945408","11905787904","5272866816","1695670272","382328832","56967168","5013504","196608","0"],["-1336336","-22324672","-170671840","-791843136","-2492892176","-5640370048","-9474953856","-12035463680","-11661393664","-8628613120","-4847407104","-2040233984","-628944896","-136937472","-19824640","-1703936","-65536"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["-1257728","-11985408","-47837184","-101613056","-114896640","-40132608","69726208","116637696","85352448","35913728","8847360","1179648","65536","0"],["3144320","41283072","237523456","790512384","1690401664","2435948288","2407598080","1622650880","720850944","192913408","22708224","-1835008","-819200","-65536"],["1886592","19864704","84074112","164581248","49903104","-499576320","-1293545472","-1709297664","-1418969088","-773013504","-274169856","-60456960","-7471104","-393216"],["-943296","-14963264","-105071424","-432556992","-1164367616","-2162118912","-2844837888","-2679117824","-1799921664","-848388096","-271335424","-55492608","-6488064","-327680"],["-314432","-4568512","-29770944","-114996800","-293171200","-519714048","-657311744","-598558720","-390856704","-179888128","-56410112","-11354112","-1310720","-65536"]]},"deriv_order":0},{"coeff":{"coeffs":[["1257728","12614272","53201024","118910080","135163008","16234240","-188454912","-310362112","-267669504","-144269312","-49807360","-10649600","-1277952","-65536","0","0"],["-1257728","-20475072","-141001536","-552376896","-1383074752","-2340865024","-2744978176","-2232915968","-1227585536","-420708352","-65937408","8503296","5980160","1048576","65536","0"],["-2358240","-29547360","-162300768","-510463392","-999231552","-1209411456","-751987968","133069824","746305536","749580288","422903808","148365312","31899648","3833856","196608","0"],["1336336","20988336","149683504","642159632","1850732544","3789637504","5685316352","6350147328","5311246336","3317366784","1530040320","510193664","118751232","18186240","1638400","65536"]]},"deriv_order":1},{"coeff":{"coeffs":[["-5345344","-67917312","-389636736","-1337156352","-3064396352","-4955269376","-5821152512","-5036167168","-3216295936","-1504600064","-506044416","-118358016","-18169856","-1638400","-65536","0","0"],["5345344","78608000","525471360","2116429824","5738709056","11084062080","15731691264","16678472192","13288630272","7937191936","3515244544","1130446848","254885888","37978112","3342336","131072","0"],["-1336336","-22324672","-170671840","-791843136","-2492892176","-5640370048","-9474953856","-12035463680","-11661393664","-8628613120","-4847407104","-2040233984","-628944896","-136937472","-19824640","-1703936","-65536"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0"],["8","16"],["12","24"],["4","8"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-26","-44","-16","0"],["13","14","12","8"],["-17","-54","-44","-8"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-34","-74","-48","-8","0"],["17","71","98","52","8"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["471648","2742032","7036640","10585936","10469856","7211840","3532672","1210112","272896","35840","2048","0","0"],["4624","-835312","-5112912","-13709200","-21526848","-22117376","-15640832","-7726592","-2620416","-577536","-73728","-4096","0"],["-150280","-1189388","-3639416","-5268524","-2437496","3859776","8019072","7218048","3941120","1380352","303104","37888","2048"],["5780","175440","1206500","3961896","7593600","9241088","7407232","3946752","1379328","303104","37888","2048","0"],["4624","47872","211216","518880","778048","733568","430848","150016","27648","2048","0","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["18496","186864","815488","2018800","3129184","3160000","2094464","894208","233984","33792","2048","0","0"],["-36992","-456960","-2316960","-6538240","-11601952","-13731776","-11119232","-6165248","-2287104","-537600","-71680","-4096","0"],["-53176","-406028","-1131816","-976588","1940936","6638272","9122688","7484800","3976960","1382400","303104","37888","2048"],["24276","292944","1507364","4363944","7894144","9364992","7432832","3948800","1379328","303104","37888","2048","0"],["4624","47872","211216","518880","778048","733568","430848","150016","27648","2048","0","0","0"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["-2515456","-16424448","-46401024","-74084864","-73236480","-46159872","-18407424","-4448256","-589824","-32768","0","0","0"],["3773184","32183040","118874880","250330368","332109312","288949248","166090752","61894656","14229504","1818624","98304","0","0"],["-1886592","-19864704","-91620480","-244040064","-416385024","-476583936","-371994624","-197038080","-69009408","-15138816","-1867776","-98304","0"],["314432","3939648","21891648","71213504","150744192","218225664","220860416","156837888","77180928","25526272","5357568","638976","32768"]]},"step_quotients":[[{"coeff":{"coeffs":[["-15092736","-128732160","-475499520","-1001321472","-1328437248","-1155796992","-664363008","-247578624","-56918016","-7274496","-393216","0","0","0"],["-5030912","2367488","227696640","1092724736","2561152000","3600046080","3245936640","1910562816","723763200","168329216","21692416","1179648","0","0"],["15092736","166464000","752051712","1803873792","2405242368","1472925696","-431456256","-1558904832","-1317224448","-593166336","-152174592","-20840448","-1179648","0"],["1257728","-15684608","-246027264","-1248516608","-3414875392","-5758235136","-6279708672","-4436754432","-1930174464","-424951808","7208960","27131904","5701632","393216"],["-4087616","-51844288","-277377984","-810641216","-1369137664","-1186101504","23443456","1332058112","1658929152","1090101248","431374336","102088704","13238272","720896"],["0","3773184","47275776","262699776","854562048","1808930304","2618707968","2650324992","1882054656","926171136","306315264","64290816","7667712","393216"],["314432","4568512","29770944","114996800","293171200","519714048","657311744","598558720","390856704","179888128","56410112","11354112","1310720","65536"]]},"deriv_order":0},{"coeff":{"coeffs":[["18865920","176007936","723106560","1727151360","2661868032","2773183488","1986250752","973836288","318726144","66011136","7766016","393216","0","0","0","0"],["-15092736","-175268096","-935310080","-2963581696","-6134301952","-8681568256","-8577867776","-5940068352","-2849906688","-919830528","-188809216","-22085632","-1114112","0","0","0"],["5030912","34735488","121470848","392863104","1252509312","3023974144","4976982016","5547982848","4213813248","2168922112","738459648","157843456","19038208","983040","0","0"],["-8489664","-75241728","-248214144","-255882240","649802304","2747339520","4743403776","4883189760","3190032384","1281761280","263135232","-3342336","-14598144","-2949120","-196608","0"],["6367248","81821680","464825968","1532524880","3222986944","4429348096","3788788736","1473137920","-725276672","-1462030336","-1042616320","-438439936","-115884032","-18808832","-1703936","-65536"],["-1336336","-20988336","-149683504","-642159632","-1850732544","-3789637504","-5685316352","-6350147328","-5311246336","-3317366784","-1530040320","-510193664","-118751232","-18186240","-1638400","-65536"]]},"deriv_order":1},{"coeff":{"coeffs":[["10690688","71690496","178079488","116685824","-398893952","-1218214144","-1710340096","-1498058752","-878481408","-349822976","-93093888","-15794176","-1540096","-65536","0","0","0"],["-26726720","-254061056","-1032557696","-2282845952","-2733351744","-923265280","2472384256","4801310720","4532901888","2708971520","1079435264","285605888","48087040","4653056","196608","0","0"],["24054048","289591872","1549613376","4848293376","9778314528","13105523136","11329378176","5199294720","-635169792","-2878187520","-2236600320","-985522176","-273309696","-47136768","-4620288","-196608","0"],["-9354352","-134891328","-880270880","-3441016512","-8984525936","-16527754112","-21988428672","-21321480704","-14915866880","-7245770752","-2183081984","-220659712","119173120","60981248","13139968","1441792","65536"],["1336336","22324672","170671840","791843136","2492892176","5640370048","9474953856","12035463680","11661393664","8628613120","4847407104","2040233984","628944896","136937472","19824640","1703936","65536"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["16350464","130655744","467700736","983028224","1332598528","1199323136","702943232","241950720","27402240","-13205504","-6225920","-1048576","-65536","0"],["-628864","-32404992","-255488512","-974300928","-2249221504","-3425215232","-3559768064","-2536275968","-1213329408","-368599040","-61931520","-3080192","557056","65536"],["-9432960","-101838976","-494650496","-1408058752","-2552668672","-2971648000","-2045947904","-480464896","490389504","553058304","262635520","68059136","9306112","524288"],["314432","6455104","63470656","352291776","1209094784","2725726208","4187385856","4465502208","3315855360","1693843456","577617920","124239872","15106048","786432"],["628864","11652480","91059072","405126784","1156050432","2245381632","3060428800","2964000768","2036416512","977223680","317030400","65568768","7733248","393216"],["314432","4568512","29770944","114996800","293171200","519714048","657311744","598558720","390856704","179888128","56410112","11354112","1310720","65536"]]},"deriv_order":0},{"coeff":{"coeffs":[["-20123648","-178560384","-715640704","-1703368064","-2659191424","-2830245632","-2055968768","-975110144","-254717952","-1908736","23199744","7831552","1146880","65536","0","0"],["18865920","200848064","978369856","2896199744","5813881792","8332038144","8713272064","6662436864","3666950144","1398571008","340860928","42352640","-475136","-786432","-65536","0"],["-6445856","-67556640","-311612448","-844686816","-1539811648","-2108372608","-2421402880","-2475748352","-2163550208","-1477242880","-729661440","-245194752","-52314112","-6324224","-327680","0"],["3694576","45190352","238721616","700414320","1185742976","924561024","-572269824","-2505039616","-3391414272","-2764488704","-1497780224","-548499456","-133267456","-20414464","-1769472","-65536"],["-1336336","-20988336","-149683504","-642159632","-1850732544","-3789637504","-5685316352","-6350147328","-5311246336","-3317366784","-1530040320","-510193664","-118751232","-18186240","-1638400","-65536"]]},"deriv_order":1},{"coeff":{"coeffs":[["-5345344","-46535936","-160730240","-236422400","82761152","1008001024","2073384192","2459369472","1937299456","1053392896","396369920","100990976","16564224","1572864","65536","0","0"],["10690688","125143936","643438848","1895039232","3454480000","3781746048","1731766272","-1569970688","-3639742464","-3423391744","-1997111296","-775372800","-200376320","-33062912","-3145728","-131072","0"],["-6681680","-95587328","-617535200","-2382801600","-6115171408","-10985723072","-14122583040","-12982244608","-8271551744","-3277174784","-425459712","344563712","246616064","79970304","14811136","1507328","65536"],["1336336","22324672","170671840","791843136","2492892176","5640370048","9474953856","12035463680","11661393664","8628613120","4847407104","2040233984","628944896","136937472","19824640","1703936","65536"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["18496","80512","139840","122368","55808","12288","1024","0","0"],["-18496","-117504","-300864","-402048","-300544","-123904","-25600","-2048","0"],["4624","38624","133968","250944","276160","181248","68352","13312","1024"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-2","-2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-3","-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":{"reason":"no parent theorem report with an interlacing conclusion","status":"none"},"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":{"reason":"no parent theorem report with an interlacing conclusion","status":"not_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"],["5","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","2"]]},"deriv_order":0,"offset":1,"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_three_term","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_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: 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) + (2) x, V_n(x) = 0, W_n(x) = (2) + (2) x; open hypotheses: multipliers_vanish_at_zero: [x^0] c_2(n, x) = 2 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 = 2 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 = 2 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":"P_n = A_n(x) P_(n-1) + B_n(x) P_(n-2) for n >= 2, with A_n(x) = (3) + (2) x, B_n(x) = (2) + (2) x: every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, -1] (so its coefficients have one sign); for n >= 1, P_(n-1) interlaces P_n (weakly, in the sense of Liu and Wang), and deg P_n - deg P_(n-1) is 0 or 1 for n >= 2","route":"liu_wang_three_term","success":true,"variant":"liu_wang_three_term"}],"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) + B_n(x) P_(n-2) for n >= 2, with A_n(x) = (3) + (2) x, B_n(x) = (2) + (2) x","every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, -1] (so its coefficients have one sign); for n >= 1, P_(n-1) interlaces P_n (weakly, in the sense of Liu and Wang), and deg P_n - deg P_(n-1) is 0 or 1 for n >= 2"],"theorem":"liu_wang_three_term: L. L. Liu and Y. Wang, Adv. Appl. Math. 38 (2007) 542-560, Theorem 2.1 and Corollary 2.4 (A unified approach to polynomial sequences with only real zeros; the lag row as the interlacer, b_n = 0), weak interlacing of consecutive rows, with nonnegativity of the coefficients replaced, where a root region is certified, by an exact root-location induction"},"kind":"weak","orientation":"previous_interlaces_next"},"route":"liu_wang_three_term","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"}