{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["2"]},{"denominator":["1"],"numerator":["1"]}],"shape":"euler_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1","1"],["1","3"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","2"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"Irregular triangle read by rows: T(n,i) = 2^(i-1)*(binomial(n-i+1,i)+binomial(n-i,i)), n >= 1, 0 <= i <= (n+1)/2."},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["18","240","16","-4736","-12800"],["21","488","1408","-3968","-17920"],["8","298","1534","-368","-9632"],["1","72","576","468","-2512"],["0","6","86","144","-320"],["0","0","4","12","-16"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","18","-208","-6224","-17024","12800"],["0","39","600","-3096","-21696","-7680"],["0","20","638","1786","-7360","-13408"],["0","3","192","1320","-36","-5232"],["0","0","18","242","320","-832"],["0","0","0","12","36","-48"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0","-27","-920","-7824","-8256","51200"],["0","0","-9","-592","-7742","-16208","39680"],["0","0","3","-22","-1986","-8188","9728"],["0","0","1","42","66","-1332","368"],["0","0","0","6","66","4","-160"],["0","0","0","0","4","12","-16"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["0","0","0","-9","-232","-1568","-704","12800"],["0","0","0","-6","-216","-1830","-2448","11520"],["0","0","0","-1","-64","-704","-1564","3872"],["0","0","0","0","-6","-102","-360","576"],["0","0","0","0","0","-4","-28","32"]]},"deriv_order":3,"shift":0},{"coeff":{"coeffs":[["-18","-60","672","2880"],["-21","-224","446","3936"],["-8","-182","-130","2132"],["-1","-56","-170","572"],["0","-6","-46","76"],["0","0","-4","4"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-54","-180","2016","8640"],["0","-63","-672","1338","11808"],["0","-24","-546","-390","6396"],["0","-3","-168","-510","1716"],["0","0","-18","-138","228"],["0","0","0","-12","12"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["0","0","-18","-60","672","2880"],["0","0","-21","-224","446","3936"],["0","0","-8","-182","-130","2132"],["0","0","-1","-56","-170","572"],["0","0","0","-6","-46","76"],["0","0","0","0","-4","4"]]},"deriv_order":2,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["1","4"]],"recurrence":{"denominator":{"coeffs":[["-4","32","224","576"],["-8","-4","360","1104"],["-5","-50","144","832"],["-1","-32","-26","308"],["0","-6","-26","56"],["0","0","-4","4"]]},"terms":[{"coeff":{"coeffs":[["-4","16","352","1472","2304"],["-8","-84","256","2344","4992"],["-5","-118","-282","1028","3856"],["-1","-48","-272","-12","1392"],["0","-6","-66","-84","240"],["0","0","-4","-12","16"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","4","74","344","-512","-4608"],["0","4","106","712","288","-5376"],["0","1","46","422","652","-2336"],["0","0","6","86","248","-448"],["0","0","0","4","28","-32"]]},"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":["2"]},{"denominator":["1"],"numerator":["1"]}],"shape":"euler_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1","1"],["1","3"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","2"]]},"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":[["-4","2","-4"],["-3","9","-6"],["-2","4","-2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["1","-7","2","4"],["1","6","-15","8"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-1","-6","15","-8"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["3"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","1296","25704","62748","-1512594","-7838748","23404032","150258240","-226368000","-981504000","1658880000"],["0","0","0","3456","82548","439740","-3028563","-28955952","18057942","471419568","-188035200","-2799590400","3262464000"],["0","0","0","3816","109818","879327","-1368657","-39242736","-43776648","549919044","296016480","-3228929280","2787379200"],["0","0","0","2232","78579","839088","1193598","-25640244","-74497338","307671192","516306240","-2016456192","1351618560"],["0","0","0","729","32661","443178","1593792","-8231148","-47313504","81455580","325323936","-756013824","406960128"],["0","0","0","126","7875","134352","740349","-889632","-15299118","4756032","108350208","-175730688","77930496"],["0","0","0","9","1017","22455","169875","167904","-2579400","-2471940","20290464","-24871680","9271296"],["0","0","0","0","54","1764","18648","52164","-199278","-555912","2023488","-1967616","626688"],["0","0","0","0","0","36","720","3672","-4176","-35676","83808","-66816","18432"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","3888","77112","188244","-4537782","-23516244","70212096","450774720","-679104000","-2944512000","4976640000"],["0","0","0","0","10368","247644","1319220","-9085689","-86867856","54173826","1414258704","-564105600","-8398771200","9787392000"],["0","0","0","0","11448","329454","2637981","-4105971","-117728208","-131329944","1649757132","888049440","-9686787840","8362137600"],["0","0","0","0","6696","235737","2517264","3580794","-76920732","-223492014","923013576","1548918720","-6049368576","4054855680"],["0","0","0","0","2187","97983","1329534","4781376","-24693444","-141940512","244366740","975971808","-2268041472","1220880384"],["0","0","0","0","378","23625","403056","2221047","-2668896","-45897354","14268096","325050624","-527192064","233791488"],["0","0","0","0","27","3051","67365","509625","503712","-7738200","-7415820","60871392","-74615040","27813888"],["0","0","0","0","0","162","5292","55944","156492","-597834","-1667736","6070464","-5902848","1880064"],["0","0","0","0","0","0","108","2160","11016","-12528","-107028","251424","-200448","55296"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","1296","25704","62748","-1512594","-7838748","23404032","150258240","-226368000","-981504000","1658880000"],["0","0","0","0","0","3456","82548","439740","-3028563","-28955952","18057942","471419568","-188035200","-2799590400","3262464000"],["0","0","0","0","0","3816","109818","879327","-1368657","-39242736","-43776648","549919044","296016480","-3228929280","2787379200"],["0","0","0","0","0","2232","78579","839088","1193598","-25640244","-74497338","307671192","516306240","-2016456192","1351618560"],["0","0","0","0","0","729","32661","443178","1593792","-8231148","-47313504","81455580","325323936","-756013824","406960128"],["0","0","0","0","0","126","7875","134352","740349","-889632","-15299118","4756032","108350208","-175730688","77930496"],["0","0","0","0","0","9","1017","22455","169875","167904","-2579400","-2471940","20290464","-24871680","9271296"],["0","0","0","0","0","0","54","1764","18648","52164","-199278","-555912","2023488","-1967616","626688"],["0","0","0","0","0","0","0","36","720","3672","-4176","-35676","83808","-66816","18432"]]},"deriv_order":2}],"step_multiplier":{"coeffs":[["0","0","0","-216","-3564","-6642","106623","132840","-1425600","1728000"],["0","0","0","-324","-5832","-19197","121905","344088","-1477440","1036800"],["0","0","0","-162","-3159","-14580","34101","196344","-419904","207360"],["0","0","0","-27","-567","-3321","-189","26568","-36288","13824"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","432","6048","-3672","-232200","294003","3088908","-11115360","14342400","-6912000"],["0","0","0","1152","17136","6552","-591012","314514","7911450","-23390352","25637760","-9907200"],["0","0","0","1224","19368","26658","-579816","-153918","7732404","-18379296","16770816","-5437440"],["0","0","0","648","10908","25812","-268596","-311148","3547368","-6723648","5156352","-1437696"],["0","0","0","171","3060","10242","-56556","-127701","754848","-1155456","755712","-184320"],["0","0","0","18","342","1476","-3924","-15750","59742","-75312","42624","-9216"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-144","-2304","-2304","87876","67545","-1483281","1478052","6132960","-13190400","6912000"],["0","0","0","-288","-5400","-17712","151146","529848","-2465046","-2474820","18371232","-22844160","8755200"],["0","0","0","-216","-4644","-24408","71172","609012","-1016496","-4440852","12914208","-11702016","3594240"],["0","0","0","-72","-1746","-12276","900","228024","-2178","-1756044","3296736","-2361600","608256"],["0","0","0","-9","-243","-2106","-3942","23571","33129","-201312","279936","-165888","36864"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","72","1620","8262","-39501","-281232","760347","2655072","-10938240","12441600","-4608000"],["0","0","0","0","108","2592","16443","-30537","-438939","465021","4004640","-10378368","9123840","-2764800"],["0","0","0","0","54","1377","10368","2430","-198126","-43335","1661472","-3037824","2156544","-552960"],["0","0","0","0","9","243","2106","3942","-23571","-33129","201312","-279936","165888","-36864"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","-288","-3852","7002","190602","-155106","-2573766","6729840","-6083712","1889280","0"],["0","0","0","-576","-8874","-7254","307296","98424","-3917718","8631342","-7559856","2687616","-230400"],["0","0","0","-432","-7254","-16974","178884","203076","-2306142","4652730","-4260240","1878912","-322560"],["0","0","0","-144","-2538","-8046","47628","82836","-651186","1259658","-1169424","542592","-101376"],["0","0","0","-18","-324","-1134","5400","11826","-75492","135054","-117936","51840","-9216"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","72","1206","2187","-41202","-80244","542376","-91071","-1182060","629856","679680","-460800"],["0","0","0","108","2169","9639","-41310","-238086","569997","1196451","-5013144","6246720","-3469824","737280"],["0","0","0","54","1251","8019","-6318","-152388","131463","1119339","-3083724","3367008","-1734912","350208"],["0","0","0","9","234","1863","1836","-27513","-9558","234441","-481248","445824","-202752","36864"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","-36","-828","-4617","15660","136134","-301320","-1179873","4794336","-6500736","3962880","-921600"],["0","0","0","0","-36","-882","-5994","5292","133704","-103194","-1136538","3132864","-3462912","1806336","-368640"],["0","0","0","0","-9","-234","-1863","-1836","27513","9558","-234441","481248","-445824","202752","-36864"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["-2","20"],["-7","34"],["-7","16"],["-2","2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["2","-18","-20"],["3","5","-44"],["1","7","-8"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-2","-11","40"],["0","-1","-7","8"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","-648","-14148","-100062","-323055","-1919160","-9783504","13343616","171051264","43407360","-1183334400","1327104000"],["0","0","0","-1404","-35712","-297963","-815445","-1860642","-25656444","-45741096","425409984","477476352","-2816962560","2344550400"],["0","0","0","-1206","-36657","-361350","-969390","1332738","-19469250","-120214944","335961936","904484736","-2728682496","1760993280"],["0","0","0","-513","-19575","-230292","-689616","2509290","-1798344","-96381612","76951152","724655232","-1411771392","729096192"],["0","0","0","-108","-5733","-82350","-303831","1255986","4034772","-34770168","-26124768","302282496","-424617984","179748864"],["0","0","0","-9","-873","-16083","-79263","257400","1908180","-5572872","-17423712","69163776","-74631168","26394624"],["0","0","0","0","-54","-1476","-10872","15372","326142","-229032","-3366000","8251776","-7123968","2138112"],["0","0","0","0","0","-36","-576","-792","18864","18972","-226512","402048","-285696","73728"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","-1944","-40176","-149040","1657287","10284570","-18745020","-139587840","251947584","658368000","-2220134400","1658880000"],["0","0","0","0","-4212","-105624","-683388","2137203","29865483","-3485016","-400462794","364153968","2106403200","-4890332160","2930688000"],["0","0","0","0","-3618","-111420","-1016370","-315297","31762530","44318682","-426996054","17877780","2611196640","-4447662336","2201241600"],["0","0","0","0","-1539","-60426","-720144","-1821645","15888078","52243380","-217806120","-231282828","1660280544","-2185963776","911370240"],["0","0","0","0","-324","-17766","-270684","-1180854","3662892","25712604","-53103204","-165413160","596404800","-630480384","224686080"],["0","0","0","0","-27","-2682","-53478","-335754","194643","6320412","-4036914","-50736888","122733504","-107076096","32993280"],["0","0","0","0","0","-162","-4806","-43704","-59220","741798","561690","-7455276","13524192","-9937152","2672640"],["0","0","0","0","0","0","-108","-1980","-7416","30888","86148","-429804","619488","-389376","92160"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","-648","-13176","-39258","708048","4145526","-8420652","-68857344","79596864","388247040","-727142400","331776000"],["0","0","0","0","0","-1404","-35064","-213669","1004922","12023109","-129780","-173279970","48981168","944178048","-1418664960","586137600"],["0","0","0","0","0","-1206","-37278","-335646","60336","12454794","20543346","-161181342","-90284796","962211168","-1183677696","440248320"],["0","0","0","0","0","-513","-20304","-243657","-604134","5886612","21683880","-70440768","-124783452","532492128","-546243840","182274048"],["0","0","0","0","0","-108","-5976","-92556","-421200","1189404","9703584","-13604436","-64389384","172991808","-150308352","44937216"],["0","0","0","0","0","-9","-900","-18324","-121248","9567","2156580","-186858","-16844184","33036480","-24629760","6598656"],["0","0","0","0","0","0","-54","-1638","-15624","-29772","224730","306162","-2233404","3438432","-2223360","534528"],["0","0","0","0","0","0","0","-36","-684","-2952","7848","31500","-119484","150624","-85248","18432"]]},"deriv_order":2}],"step_multiplier":{"coeffs":[["0","0","0","-216","-3564","-6642","106623","132840","-1425600","1728000"],["0","0","0","-324","-5832","-19197","121905","344088","-1477440","1036800"],["0","0","0","-162","-3159","-14580","34101","196344","-419904","207360"],["0","0","0","-27","-567","-3321","-189","26568","-36288","13824"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","1296","16200","-45684","-799146","1761912","11741760","-44582400","41472000"],["0","0","0","3888","54108","-50544","-2311173","2224584","33141312","-91445760","66355200"],["0","0","0","4824","73638","47115","-2623140","-324450","35938512","-74054016","42531840"],["0","0","0","3168","52425","104193","-1479942","-1727172","19311264","-30327552","14063616"],["0","0","0","1161","20628","65205","-426762","-992520","5438016","-6649344","2543616"],["0","0","0","225","4257","17847","-55989","-224676","762912","-744192","239616"],["0","0","0","18","360","1836","-2088","-17838","41904","-33408","9216"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-432","-6696","-972","312066","211842","-5675832","3119040","30758400","-41472000"],["0","0","0","-1008","-18324","-48276","629091","1934613","-10235916","-12035232","72840960","-59443200"],["0","0","0","-936","-19458","-91359","400959","2714670","-5221764","-21073248","53611776","-30320640"],["0","0","0","-432","-10071","-65070","58941","1418364","-274212","-10797408","16913664","-7243776"],["0","0","0","-99","-2547","-20385","-24237","293400","338796","-2172384","2416896","-829440"],["0","0","0","-9","-252","-2358","-6300","17271","50400","-150912","129024","-36864"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","216","4860","24570","-123795","-878850","2334528","8951040","-33177600","27648000"],["0","0","0","0","396","9468","58959","-129582","-1693449","1812960","16437888","-37693440","21196800"],["0","0","0","0","270","6831","50085","-8559","-1084563","-197856","9472896","-14321664","6082560"],["0","0","0","0","81","2160","18090","25272","-262467","-353376","2063232","-2267136","774144"],["0","0","0","0","9","252","2358","6300","-17271","-50400","150912","-129024","36864"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","-864","-10476","41958","661392","-816264","-9637056","23542272","-12718080","0"],["0","0","0","-2016","-29250","12312","1281510","95544","-16912692","32048928","-17876736","1382400"],["0","0","0","-1872","-30510","-52074","927252","1031022","-11576106","18972432","-11435904","2165760"],["0","0","0","-864","-15192","-46098","318870","647226","-4078710","6198768","-3954816","930816"],["0","0","0","-198","-3654","-14076","54180","160722","-764190","1079856","-669312","156672"],["0","0","0","-18","-342","-1476","3924","15750","-59742","75312","-42624","9216"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","216","3510","3537","-149607","-265734","2165670","604584","-7960896","2833920","2764800"],["0","0","0","396","7677","29088","-195390","-930168","2492433","5537628","-18049248","15070464","-3962880"],["0","0","0","270","6003","35028","-60282","-783450","680895","5440320","-12580992","10100736","-2838528"],["0","0","0","81","2007","14886","7758","-238995","-65493","1856556","-3274848","2269440","-571392"],["0","0","0","9","243","2106","3942","-23571","-33129","201312","-279936","165888","-36864"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","-108","-2484","-13743","49680","427545","-915354","-3989952","14397696","-15482880","5529600"],["0","0","0","0","-144","-3510","-23355","28917","571023","-436131","-5112288","12403584","-10561536","3133440"],["0","0","0","0","-63","-1620","-12474","-6372","221697","76464","-1862784","3317760","-2322432","589824"],["0","0","0","0","-9","-243","-2106","-3942","23571","33129","-201312","279936","-165888","36864"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["0","0","0","-216","-3564","-6642","106623","132840","-1425600","1728000"],["0","0","0","-324","-5832","-19197","121905","344088","-1477440","1036800"],["0","0","0","-162","-3159","-14580","34101","196344","-419904","207360"],["0","0","0","-27","-567","-3321","-189","26568","-36288","13824"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["0","-2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-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 = f(n, theta) = 1 + (2) theta + (1) theta^2; 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.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, 2, 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 [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":"f(n, theta) = 1 + (2) theta + (1) theta^2","kind":"preserver_image","operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["2"]},{"denominator":["1"],"numerator":["1"]}],"shape":"euler_polynomial"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1","1"],["1","3"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","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 + (2) theta + (1) theta^2, 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 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":"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":"the parent rows are not the canonical boundary rows (Mismatch)","route":"paper_theorem","success":false,"variant":"weighted_renewal_window"},{"detail":"the parent rows are not the canonical boundary rows (Mismatch)","route":"paper_theorem","success":false,"variant":"fixed_delay_predecessor_window"},{"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) = (1), V_n(x) = 0, W_n(x) = (2) x; open hypotheses: seed_degree_step: degrees 1 and 1 (exact); seed_strict_interlacing: the Bezout test fails or the degrees do not differ by one (exact); degree_step_positive: fails at n = 2: lambda_n = 0 = 0 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) = (1), B_n(x) = (2) x: 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-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) = (1), B_n(x) = (2) x","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-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 = f(n, theta) = 1 + (2) theta + (1) theta^2 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"}