{"certification":{"candidate":{"gauge":{"denominator":["1","1"],"kind":"closed","numerator":["8","4"]},"index_shift":2,"operator":{"factor":{"terms":[{"coefficient_offset":1,"index_offset":1,"kind":"binomial"}]},"shape":"hadamard_multiplier"},"parent":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"n-c8c19eba9d68881f"},"identifying_rows":3,"identity":{"certificate":{"certificate":{"factor":{"terms":[{"coefficient_offset":1,"index_offset":1,"kind":"binomial"}]},"hadamard":{"conjugated_input_relation":{"terms":[{"coeff":{"coeffs":[["-103680","255744","-456192","705024"],["-573696","1334016","-2156544","2633472"],["-1413072","3063024","-4410720","4208544"],["-2052456","4093816","-5152080","3802656"],["-1961732","3546012","-3818136","2150856"],["-1302198","2094218","-1881612","792432"],["-616546","862002","-626220","190656"],["-210078","247668","-139320","28944"],["-51186","48744","-19872","2520"],["-8706","6266","-1644","96"],["-982","474","-60","0"],["-66","16","0","0"],["-2","0","0","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","103680","-255744","456192","1057536"],["0","539136","-1142208","1244160","3950208"],["0","1233360","-2158416","1010016","6312816"],["0","1641336","-2248852","-268656","5703984"],["0","1414620","-1398132","-1065288","3226284"],["0","830658","-508649","-871236","1188648"],["0","339660","-84123","-384156","285984"],["0","96858","9894","-102744","43416"],["0","18900","8226","-16704","3780"],["0","2406","1807","-1524","144"],["0","180","189","-60","0"],["0","6","8","0","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0","-51840","127872","532224","352512"],["0","0","-243648","347328","1907712","1316736"],["0","0","-494856","279576","2878704","2104272"],["0","0","-573240","-77632","2396936","1901328"],["0","0","-420690","-297242","1198876","1075428"],["0","0","-204984","-241218","359982","396216"],["0","0","-67338","-105660","57006","95328"],["0","0","-14760","-28068","1164","14472"],["0","0","-2070","-4530","-1200","1260"],["0","0","-168","-410","-194","48"],["0","0","-6","-16","-10","0"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["0","0","0","17280","63936","76032","29376"],["0","0","0","63936","237600","283392","109728"],["0","0","0","101016","377388","451728","175356"],["0","0","0","90064","338572","406952","158444"],["0","0","0","50166","189951","229404","89619"],["0","0","0","18162","69342","84198","33018"],["0","0","0","4284","16512","20172","7944"],["0","0","0","636","2478","3048","1206"],["0","0","0","54","213","264","105"],["0","0","0","2","8","10","4"]]},"deriv_order":3,"shift":0},{"coeff":{"coeffs":[["673920","-428544","-756864"],["3262464","-1921536","-3177792"],["7069896","-3812256","-5828328"],["9097212","-4435664","-6177120"],["7758958","-3373416","-4202682"],["4628793","-1765084","-1922346"],["1983152","-649692","-599724"],["615447","-168528","-126180"],["137418","-30240","-17154"],["21543","-3580","-1362"],["2252","-252","-48"],["141","-8","0"],["4","0","0"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-449280","107136","-756864"],["0","-2025216","319680","-3177792"],["0","-4038192","312840","-5828328"],["0","-4718744","-568","-6177120"],["0","-3599724","-265278","-4202682"],["0","-1885954","-269444","-1922346"],["0","-693450","-144126","-599724"],["0","-179148","-48228","-126180"],["0","-31896","-10458","-17154"],["0","-3730","-1436","-1362"],["0","-258","-114","-48"],["0","-8","-4","0"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["0","0","112320","107136","-126144"],["0","0","450144","426816","-529632"],["0","0","784476","739656","-971388"],["0","0","787448","739088","-1029520"],["0","0","506207","473810","-700447"],["0","0","218385","204366","-320391"],["0","0","64170","60240","-99954"],["0","0","12702","12012","-21030"],["0","0","1623","1554","-2859"],["0","0","121","118","-227"],["0","0","4","4","-8"]]},"deriv_order":2,"shift":1},{"coeff":{"coeffs":[["-1036800","-69120"],["-4648320","3456"],["-9273312","624096"],["-10936104","1410728"],["-8519096","1554360"],["-4629306","1040098"],["-1802710","455958"],["-507618","134364"],["-102702","26460"],["-14574","3346"],["-1378","246"],["-78","8"],["-2","0"]]},"deriv_order":0,"shift":2},{"coeff":{"coeffs":[["0","345600","-34560"],["0","1434240","1728"],["0","2613024","312048"],["0","2774360","705364"],["0","1914912","777180"],["0","904798","520049"],["0","299304","227979"],["0","69438","67182"],["0","11088","13230"],["0","1162","1673"],["0","72","123"],["0","2","4"]]},"deriv_order":1,"shift":2},{"coeff":{"coeffs":[["466560"],["1959552"],["3616488"],["3891348"],["2721870"],["1302711"],["436104"],["102249"],["16470"],["1737"],["108"],["3"]]},"deriv_order":0,"shift":3}]},"conjugation_x_shift":0,"exceptional_bases":[],"factor":{"terms":[{"coefficient_offset":1,"index_offset":1,"kind":"binomial"}]},"gauge":{"denominator":["1","1"],"kind":"closed","numerator":["8","4"]},"identifying_indices":[0,1,2],"input_leader_shift":3,"input_relation":{"terms":[{"coeff":{"coeffs":[["-30","111","-132","51"],["-46","172","-206","80"],["-18","69","-84","33"],["-2","8","-10","4"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["130","-124","-146"],["131","-122","-175"],["41","-38","-67"],["4","-4","-8"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["-150","-15"],["-110","52"],["-26","31"],["-2","4"]]},"deriv_order":0,"shift":2},{"coeff":{"coeffs":[["54"],["27"],["3"]]},"deriv_order":0,"shift":3}]},"input_valid_from_base":0,"multiplier":["1"],"parent":{"first_index":0,"initial_polynomials":[["1","2","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_leader_shift":1,"parent_relation":{"terms":[{"coeff":{"coeffs":[["-1","-1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"shift":1}]},"parent_valid_from_base":0,"quotients":[{"differentiations":[{"coeff":{"coeffs":[["-103680","-677376","-1036800","4043520","22602240","52254720","73156608","67392000","41368320","16381440","3801600","393984"],["-573696","-3950208","-8522496","6397056","73281024","182456064","257499648","234088704","140403456","54013824","12130560","1213056"],["-1413072","-10102176","-26055648","-13059792","87577632","258660864","371589120","329566752","188597808","68051232","14096736","1275696"],["-2052456","-15068120","-43082880","-48335760","33433680","184545648","277875360","233425920","118324440","34691880","4931104","169680"],["-1961732","-14676088","-44657580","-65180040","-27526440","56777616","103439784","72463920","18145260","-5772440","-4677052","-850728"],["-1302198","-9875710","-31222992","-51462648","-43033332","-10726884","4463928","-10481592","-24336198","-18563982","-6620536","-940512"],["-616546","-4723982","-15291585","-26775165","-27121920","-17449992","-13408374","-18461310","-19557990","-11923570","-3857921","-520317"],["-210078","-1622856","-5329809","-9602631","-10364904","-7640892","-6277446","-7443234","-7167906","-4193604","-1330689","-177615"],["-51186","-398220","-1319616","-2402334","-2607516","-1856736","-1345176","-1511316","-1488834","-893316","-288600","-39006"],["-8706","-68182","-227262","-413658","-436692","-268380","-129276","-138612","-165258","-111342","-38374","-5394"],["-982","-7742","-25917","-46893","-47112","-21672","1554","2658","-5418","-6562","-2765","-429"],["-66","-524","-1761","-3159","-2976","-756","1386","1614","666","24","-65","-15"],["-2","-16","-54","-96","-84","0","84","96","54","16","2","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","103680","514944","760320","777600","6428160","26853120","55738368","68325120","52358400","24831360","6704640","791424"],["0","590976","3563136","8650368","15023232","41326848","120040704","228614400","273984768","208904832","99128448","26828928","3176064"],["0","1425168","9588600","27681120","52795800","106172640","234961776","406788480","474372720","359629200","170870040","46408608","5516280"],["0","1944384","14020300","44157176","87324444","149726496","266246232","414395856","467189976","351877344","167615196","45766648","5471756"],["0","1684812","12736494","42237408","84988422","131752008","194249916","267358896","288414108","215540172","103161558","28402704","3425502"],["0","981156","7675001","26325286","53443269","77054496","95837826","113525748","114957186","85028844","41065221","11465270","1402297"],["0","394146","3164157","11112588","22660317","30860028","32611194","31670352","28843938","20980242","10328553","2962548","371745"],["0","109710","898998","3213030","6564510","8522460","7641900","5511996","3958380","2761110","1438110","442590","58998"],["0","20808","173412","628272","1284228","1598832","1205064","495936","79272","17928","37332","21456","3924"],["0","2568","21713","79546","162549","194856","121170","252","-64254","-53376","-21219","-4198","-311"],["0","186","1593","5892","12033","13932","6930","-4032","-9558","-7542","-3243","-756","-75"],["0","6","52","194","396","444","168","-252","-456","-354","-156","-38","-4"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","-112320","-1118016","-4881600","-12156480","-18610560","-17055360","-7039872","2851200","5728320","3464640","1028160","126144"],["0","0","-450144","-4478112","-19516896","-48410784","-73503936","-66007872","-24857280","14675904","25072416","14775264","4339872","529632"],["0","0","-784476","-7799940","-33926652","-83781108","-126005112","-110444040","-36697752","32022648","47908692","27528588","8002836","971388"],["0","0","-787448","-7826120","-33970400","-83487120","-124239120","-105863856","-29551200","39288000","52785480","29623480","8526592","1029520"],["0","0","-506207","-5029673","-21787295","-53274525","-78366030","-64644594","-13965126","30232830","37224525","20445595","5830213","700447"],["0","0","-218385","-2169831","-9380763","-22817997","-33149178","-26353782","-3725190","15340662","17590203","9476397","2679153","320391"],["0","0","-64170","-637770","-2752326","-6659334","-9547236","-7279524","-386316","5223924","5649966","2992014","839346","99954"],["0","0","-12702","-126330","-544350","-1310130","-1852380","-1347444","69300","1183500","1219770","636270","177258","21030"],["0","0","-1623","-16161","-69555","-166545","-232110","-160146","28098","171270","169605","87315","24177","2859"],["0","0","-121","-1207","-5191","-12369","-16986","-11046","3570","14334","13731","6989","1925","227"],["0","0","-4","-40","-172","-408","-552","-336","168","528","492","248","68","8"]]},"deriv_order":2}],"shift":0},{"differentiations":[{"coeff":{"coeffs":[["570240","4734720","16951680","33592320","38465280","21772800","-2177280","-12856320","-9175680","-3006720","-397440"],["2688768","22235904","79128576","155188224","173892096","91445760","-21482496","-68097024","-46469376","-14978304","-1963008"],["5656824","46670832","165480408","322512192","356550768","178446240","-59140368","-152563392","-101749608","-32508432","-4240584"],["7044756","58100728","205892532","400884768","442264872","219577680","-76302072","-191763168","-127471932","-40673928","-5302076"],["5797226","47898804","170214066","333022704","371247156","191645496","-51837996","-150503184","-101769246","-32688844","-4276230"],["3326595","27596546","98672139","195092856","222355014","123957036","-15759954","-77038536","-54401769","-17758686","-2342809"],["1366606","11407392","41169258","82680672","97259148","59792544","2395092","-25735392","-19814778","-6661952","-892062"],["405369","3411708","12463767","25532928","31201002","21263256","4237758","-5282208","-4869747","-1724148","-236613"],["86232","733158","2717982","5698008","7259112","5456052","1834308","-501768","-769392","-300138","-42930"],["12837","110450","416385","895320","1190490","977004","437850","35160","-67455","-32910","-5083"],["1270","11076","42534","93936","130284","115416","62076","15984","-1314","-1916","-354"],["75","664","2601","5904","8526","8064","4914","1776","279","-24","-11"],["2","18","72","168","252","252","168","72","18","2","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","-345600","-3075840","-12130560","-27786240","-40642560","-39191040","-24675840","-9538560","-1866240","-34560","34560"],["0","-1434240","-12909888","-51648192","-120538368","-180859392","-180931968","-120693888","-51777792","-12970368","-1449792","-1728"],["0","-2613024","-23829264","-96877296","-230727744","-355453056","-368559072","-258812064","-120280896","-34750944","-5421456","-312048"],["0","-2774360","-25674604","-106225236","-258439344","-408819936","-438445224","-321922104","-159127536","-50362344","-9122636","-705364"],["0","-1914912","-18011388","-75931452","-188831088","-306562032","-339203592","-258777288","-134219952","-45212688","-8909532","-777180"],["0","-904798","-8663231","-37253169","-94724796","-157688664","-179530722","-141529206","-76256844","-26864946","-5585239","-520049"],["0","-299304","-2921715","-12826755","-33348780","-56862540","-66437658","-53866890","-29925180","-10900980","-2351115","-227979"],["0","-69438","-692124","-3104406","-8251344","-14392476","-17214120","-14297724","-8143056","-3043494","-674076","-67182"],["0","-11088","-113022","-518238","-1407672","-2508408","-3064068","-2598372","-1510488","-576072","-130158","-13230"],["0","-1162","-12131","-56889","-157836","-286944","-357210","-308406","-182364","-70686","-16219","-1673"],["0","-72","-771","-3699","-10476","-19404","-24570","-21546","-12924","-5076","-1179","-123"],["0","-2","-22","-108","-312","-588","-756","-672","-408","-162","-38","-4"]]},"deriv_order":1}],"shift":1},{"differentiations":[{"coeff":{"coeffs":[["-466560","-4199040","-16796160","-39191040","-58786560","-58786560","-39191040","-16796160","-4199040","-466560"],["-1959552","-17635968","-70543872","-164602368","-246903552","-246903552","-164602368","-70543872","-17635968","-1959552"],["-3616488","-32548392","-130193568","-303784992","-455677488","-455677488","-303784992","-130193568","-32548392","-3616488"],["-3891348","-35022132","-140088528","-326873232","-490309848","-490309848","-326873232","-140088528","-35022132","-3891348"],["-2721870","-24496830","-97987320","-228637080","-342955620","-342955620","-228637080","-97987320","-24496830","-2721870"],["-1302711","-11724399","-46897596","-109427724","-164141586","-164141586","-109427724","-46897596","-11724399","-1302711"],["-436104","-3924936","-15699744","-36632736","-54949104","-54949104","-36632736","-15699744","-3924936","-436104"],["-102249","-920241","-3680964","-8588916","-12883374","-12883374","-8588916","-3680964","-920241","-102249"],["-16470","-148230","-592920","-1383480","-2075220","-2075220","-1383480","-592920","-148230","-16470"],["-1737","-15633","-62532","-145908","-218862","-218862","-145908","-62532","-15633","-1737"],["-108","-972","-3888","-9072","-13608","-13608","-9072","-3888","-972","-108"],["-3","-27","-108","-252","-378","-378","-252","-108","-27","-3"]]},"deriv_order":0}],"shift":2}],"row_annihilator":[{"coeff":{"coeffs":[["2","4","2"],["1","2","1"]]},"deriv_order":0},{"coeff":{"coeffs":[["-1","-3","-3","-1"]]},"deriv_order":1}],"row_annihilator_quotient":[{"coeff":{"coeffs":[["0","0","222912","1451520","3991680","5951232","5080320","2322432","362880","-103680","-36288"],["0","-51840","465696","4195584","12273984","18147456","14342400","4962816","-599616","-988416","-216864"],["0","-191808","-10692","4237920","14390568","20916144","13630032","355968","-5018760","-2847312","-520236"],["0","-303048","-882060","1071264","7299456","10088880","2006952","-8305440","-9276576","-4084584","-680700"],["0","-270192","-1136177","-1310000","320306","-149884","-5915812","-10838072","-8746730","-3458924","-548659"],["0","-150498","-728504","-1341968","-1469454","-2468872","-5238898","-6841464","-4939058","-1861454","-288342"],["0","-54486","-277119","-566850","-733770","-1152198","-2061096","-2499894","-1754550","-654060","-100953"],["0","-12852","-64242","-123978","-137898","-202050","-403422","-529902","-388638","-148818","-23400"],["0","-1908","-8535","-11220","1614","7752","-21108","-54660","-49350","-20796","-3453"],["0","-162","-492","684","5070","8916","6498","348","-2526","-1530","-294"],["0","-6","11","230","802","1354","1264","626","110","-28","-11"],["0","0","2","14","42","70","70","42","14","2","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","60480","641088","2903040","7451136","12023424","12700800","8805888","3870720","979776","108864"],["0","0","206496","2224800","10169280","26236224","42432768","44827776","31026240","13590720","3422304","377568"],["0","0","289620","3201300","14840928","38578176","62590248","66112200","45622080","19872288","4962276","541188"],["0","0","214208","2474912","11739948","30875572","50319388","53107908","36452612","15723548","3869172","413388"],["0","0","85517","1085277","5377412","14437556","23700054","24952102","16941652","7166052","1711301","174949"],["0","0","13401","239457","1334343","3761289","6267597","6547191","4320477","1733763","379254","33372"],["0","0","-3168","768","90696","347256","621096","618072","341208","86376","-744","-3384"],["0","0","-2058","-13962","-43548","-86772","-128688","-148008","-125412","-71148","-23622","-3438"],["0","0","-447","-3615","-13602","-31542","-49728","-54852","-41790","-20922","-6177","-813"],["0","0","-47","-407","-1623","-3913","-6265","-6867","-5117","-2483","-708","-90"],["0","0","-2","-18","-74","-182","-294","-322","-238","-114","-32","-4"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","17280","167616","718848","1790208","2854656","3024000","2128896","960768","252288","29376"],["0","0","0","63936","621216","2668032","6652800","10620288","11261376","7934976","3583872","941760","109728"],["0","0","0","101016","983484","4231296","10566864","16891056","17931816","12648384","5718096","1503864","175356"],["0","0","0","90064","878956","3789344","9480016","15177344","16134664","11394656","5156944","1357616","158444"],["0","0","0","50166","490947","2121600","5318628","8530284","9082626","6423312","2910660","767118","89619"],["0","0","0","18162","178314","772680","1941576","3120348","3328332","2357544","1069800","282306","33018"],["0","0","0","4284","42216","183504","462336","744744","795984","564816","256704","67836","7944"],["0","0","0","636","6294","27456","69384","112056","120036","85344","38856","10284","1206"],["0","0","0","54","537","2352","5964","9660","10374","7392","3372","894","105"],["0","0","0","2","20","88","224","364","392","280","128","34","4"]]},"deriv_order":2}],"row_multiplier":["-1","-9","-36","-84","-126","-126","-84","-36","-9","-1"],"statement":"mu(x) w(n) M'' = sum_nu H_nu S^nu L + Z A (A the row annihilator of the product parent) with M'' the input relation conjugated by lambda(n) binom(n+1, k+1); so the candidate rows satisfy the input rule at every base n >= 0 (the exceptional bases checked exactly), and agreement on the 3 identifying rows gives Q_n = lambda(n) sum_k u(n,k) [x^k]P_n x^k for every n >= 0"},"index_shift":2,"input":{"first_index":0,"initial_polynomials":[["8"],["12","18"],["16","64","32"]],"recurrence":{"denominator":{"coeffs":[["0"],["9"],["3"]]},"terms":[{"coeff":{"coeffs":[["0","0"],["8","26"],["8","5"],["2","-4"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["2","-8","8"],["7","2","-11"],["-5","2","-5"],["-4","4","8"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["0","0","0","0"],["-8","26","-28","10"],["0","3","-6","3"],["2","-8","10","-4"]]},"deriv_order":0,"offset":3,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"}},"method":"hadamard_conjugation"},"status":"certified"},"input_first_index":0,"interlacing":{"reason":"the factor depends on n","status":"none"},"lift_summary":{"hypotheses":[{"evidence":"binom(n+1, k+1) is defined for every n >= 0","name":"factor_defined","statement":"the factor u(n, k) is defined on the index domain","status":{"kind":"verified"}},{"evidence":"binom(n+1, k+1): sum_k u(n,k) x^k / k! = L_(A-1)^(1)(-x) with A = n + a (zero when A < 1), a Laguerre polynomial with parameter 1 > -1, whose zeros are real and positive (Szego, Orthogonal Polynomials, Theorem 3.3.1); third condition of Theorem 40","name":"factor_multiplier_sequence","statement":"k -> u(n, k) is a nonnegative multiplier sequence for every n >= n0","status":{"kind":"verified"}},{"evidence":"lambda(n) = numerator(n) / denominator(n) != 0 for every integer n in [0, +inf) (exact; Taylor shift: the coefficients of lambda(n) = numerator(n) / denominator(n) at n = 0 + u have one sign)","name":"gauge_finite_nonzero","sign_decision":{"certificate":{"condition":"nonzero","denominator":["1","1"],"method":{"kind":"taylor_shift","shifted_denominator":["1","1"],"shifted_numerator":["8","4"]},"numerator":["8","4"],"range":{"first":"0","last":null}},"decision":"holds"},"statement":"lambda(n) is finite and nonzero for every n >= n0","status":{"kind":"verified"}}],"identity":{"method":"hadamard_conjugation","status":"certified"},"input_first_index":0,"input_interlacing":{"reason":"the factor depends on n","status":"not_proved"},"lean_replay":"not_attempted","operation":{"description":"x^k -> binom(n+1, k+1) x^k","kind":"preserver_image","operator":{"factor":{"terms":[{"coefficient_offset":1,"index_offset":1,"kind":"binomial"}]},"shape":"hadamard_multiplier"}},"parent":{"gauge":{"denominator":["1","1"],"kind":"closed","numerator":["8","4"]},"index_shift":2,"recurrence":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"relation":"Q_n = lambda(n) T_n(P_(n+2)) with T = x^k -> binom(n+1, k+1) x^k, for every n >= 0"},"parent_proof":{"route":"periodic_product","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":"Polya--Schur characterization of multiplier sequences (G. Polya and I. Schur, J. Reine Angew. Math. 144 (1914) 89--113; stated as Theorem 40 of P. Branden, Unimodality, log-concavity, real-rootedness and beyond, arXiv:1410.6601): a real sequence (lambda_k) is a multiplier sequence (x^k -> lambda_k x^k maps real-rooted polynomials to real-rooted polynomials or zero) iff sum_k binom(m,k) lambda_k x^k is real-rooted with zeros of one sign for every m, iff sum_k lambda_k x^k / k! (or its reflection) is C x^m e^(a x) prod (1 + alpha_j x) with a, alpha_j >= 0; a product of multiplier sequences is one (composition), and a nonzero factor lambda(n) of the row changes nothing"},"verdict":"proved"},"notes":[],"parent_interlacing_report":{"conclusion":{"first_index":0,"interlacing":"weak","interlacing_from":1,"root_region":{"upper":{"closed":false,"value":"0"}},"simple_roots":false,"statement":"every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0) (so its coefficients have one sign); deg P_n = deg P_(n-1) + 1 and P_(n-1) interlaces P_n (Liu--Wang) for n >= 1"},"hypotheses":[{"evidence":"P_0 has degree 0; checked exactly","name":"seed_roots_negative","statement":"P_0 is nonzero and real-rooted with every root < 0","status":{"kind":"verified"}},{"evidence":"lambda_n = 1 > 0 for every integer n in [1, +inf) (exact; Taylor shift: the coefficients of lambda_n = 1 at n = 1 + u have one sign)","name":"degree_step_positive","sign_decision":{"certificate":{"condition":"positive","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1"]},"numerator":["1"],"range":{"first":"1","last":null}},"decision":"holds"},"statement":"lambda_n = [x^1] a_n + (deg P_(n-1)) [x^2] b_n > 0 for every n >= 1 (deg P_n = deg P_(n-1) + 1 with leading coefficients of one sign)","status":{"kind":"verified"}},{"evidence":"[x^0] c_1(n, x) is the zero polynomial","name":"derivative_coefficient_vanishes_at_zero","statement":"b_n(0) = 0 for every n >= 1","status":{"kind":"verified"}},{"evidence":"b_n = 0","name":"derivative_coefficient_nonpositive","statement":"b_n(x) <= 0 for every x < 0 and every n >= 1","status":{"kind":"verified"}},{"evidence":"a_n(0) = 1 > 0 for every integer n in [1, +inf) (exact; Taylor shift: the coefficients of a_n(0) = 1 at n = 1 + 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":"1","last":null}},"decision":"holds"},"statement":"a_n(0) > 0 for every n >= 1","status":{"kind":"verified"}},{"evidence":"exact","name":"requested_root_region","statement":"the requested region (-inf, 0) contains (-inf, 0), the region this theorem certifies","status":{"kind":"verified"}}],"lean_replay":"not_attempted","normal_form":"P_n = a_n(x) P_(n-1) + b_n(x) P'_(n-1) for n >= 1, with a_n(x) = (1) + (1) x and b_n(x) = (0) + (0) x + (0) x^2","recurrence":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"deriv_order":0,"offset":1,"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 g = f' (as in their Corollary 2.4), with nonnegativity of the coefficients replaced by an exact induction keeping every root in (-inf, 0)","requested_root_region":{"upper":{"closed":false,"value":"0"}},"schema":"polytool.recurrence-real-rootedness-theorem.v1","status":"proved","theorem":"liu_wang"},"parent_proof":{"attempts":[{"detail":"c and the seeds are nonzero, real-rooted and of one sign, so P_(n0 + k m + i) = c^m P_(n0 + i) is too","route":"periodic_product","success":true,"variant":"P_(n+k) = c(x) P_n"}],"conditional_on":[],"route":"periodic_product","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+2)) with T = x^k -> binom(n+1, k+1) x^k 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"}