{"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"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-1","-1","-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"Triangle T(n,k) = number of k-part order-consecutive partitions of n (1<=k<=n)."},"identifying_rows":2,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["36","128","696","1192","1576","1008","476"],["0","-2","582","1256","2126","1542","868"],["0","-22","99","313","907","786","572"],["0","0","-2","-10","150","152","160"],["0","0","1","-7","9","8","16"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","108","384","2088","3576","4728","3024","1428"],["0","0","-6","1746","3768","6378","4626","2604"],["0","0","-66","297","939","2721","2358","1716"],["0","0","0","-6","-30","450","456","480"],["0","0","0","3","-21","27","24","48"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0","36","128","696","1192","1576","1008","476"],["0","0","0","-2","582","1256","2126","1542","868"],["0","0","0","-22","99","313","907","786","572"],["0","0","0","0","-2","-10","150","152","160"],["0","0","0","0","1","-7","9","8","16"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["-72","-344","-616","-744","-472","-200"],["0","-40","-980","-1988","-1384","-624"],["0","44","-194","-762","-1076","-664"],["0","0","8","-8","-272","-256"],["0","0","-2","14","-16","-32"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-216","-1032","-1848","-2232","-1416","-600"],["0","0","-120","-2940","-5964","-4152","-1872"],["0","0","132","-582","-2286","-3228","-1992"],["0","0","0","24","-24","-816","-768"],["0","0","0","-6","42","-48","-96"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["0","0","-72","-344","-616","-744","-472","-200"],["0","0","0","-40","-980","-1988","-1384","-624"],["0","0","0","44","-194","-762","-1076","-664"],["0","0","0","0","8","-8","-272","-256"],["0","0","0","0","-2","14","-16","-32"]]},"deriv_order":2,"shift":1},{"coeff":{"coeffs":[["36","72","108","72","36"],["0","42","332","254","140"],["0","-22","133","190","188"],["0","0","-6","24","96"],["0","0","1","-8","16"]]},"deriv_order":0,"shift":2},{"coeff":{"coeffs":[["0","108","216","324","216","108"],["0","0","126","996","762","420"],["0","0","-66","399","570","564"],["0","0","0","-18","72","288"],["0","0","0","3","-24","48"]]},"deriv_order":1,"shift":2},{"coeff":{"coeffs":[["0","0","36","72","108","72","36"],["0","0","0","42","332","254","140"],["0","0","0","-22","133","190","188"],["0","0","0","0","-6","24","96"],["0","0","0","0","1","-8","16"]]},"deriv_order":2,"shift":2}]},"exceptional_bases":[0],"gauge":{"kind":"none"},"identifying_indices":[0,1],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["1"],["1","4"]],"recurrence":{"denominator":{"coeffs":[["36","-100","40","4","-4"],["0","130","-304","38","28"],["0","-22","193","-146","-4"],["0","0","-14","88","-32"],["0","0","1","-8","16"]]},"terms":[{"coeff":{"coeffs":[["-36","-44","40","100","104","20","-4"],["0","-86","-130","-108","-10","34","12"],["0","22","-135","-205","-223","-66","4"],["0","0","10","-46","-78","-88","-32"],["0","0","-1","7","-9","-8","-16"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["72","88","-472","-472","88","72"],["0","216","44","-516","-168","16"],["0","-44","290","378","-172","-104"],["0","0","-24","120","144","0"],["0","0","2","-14","16","32"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["0","0","0","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"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-1","-1","-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_leader_shift":2,"parent_valid_from_base":0,"quotients":[{"differentiations":[{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","-18432","-36864","-55296","18432","92160","165888","55296","-55296","-165888","-92160","-18432","55296","36864","18432"],["0","0","0","0","-21504","-169984","-130048","-7168","509952","390144","150528","-509952","-390144","-193536","169984","130048","71680"],["0","0","0","0","11264","-68096","-97280","-130048","204288","291840","322560","-204288","-291840","-300032","68096","97280","96256"],["0","0","0","0","0","3072","-12288","-49152","-9216","36864","147456","9216","-36864","-147456","-3072","12288","49152"],["0","0","0","0","0","-512","4096","-8192","1536","-12288","24576","-1536","12288","-24576","512","-4096","8192"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","-55296","-110592","-165888","55296","276480","497664","165888","-165888","-497664","-276480","-55296","165888","110592","55296"],["0","0","0","0","0","-64512","-509952","-390144","-21504","1529856","1170432","451584","-1529856","-1170432","-580608","509952","390144","215040"],["0","0","0","0","0","33792","-204288","-291840","-390144","612864","875520","967680","-612864","-875520","-900096","204288","291840","288768"],["0","0","0","0","0","0","9216","-36864","-147456","-27648","110592","442368","27648","-110592","-442368","-9216","36864","147456"],["0","0","0","0","0","0","-1536","12288","-24576","4608","-36864","73728","-4608","36864","-73728","1536","-12288","24576"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","-18432","-36864","-55296","18432","92160","165888","55296","-55296","-165888","-92160","-18432","55296","36864","18432"],["0","0","0","0","0","0","-21504","-169984","-130048","-7168","509952","390144","150528","-509952","-390144","-193536","169984","130048","71680"],["0","0","0","0","0","0","11264","-68096","-97280","-130048","204288","291840","322560","-204288","-291840","-300032","68096","97280","96256"],["0","0","0","0","0","0","0","3072","-12288","-49152","-9216","36864","147456","9216","-36864","-147456","-3072","12288","49152"],["0","0","0","0","0","0","0","-512","4096","-8192","1536","-12288","24576","-1536","12288","-24576","512","-4096","8192"]]},"deriv_order":2}],"shift":0}],"row_annihilation":{"kind":"system","system":{"generators":[{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0"],["-3","-8"],["-1","4"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["2","6","10"],["0","-4","-8"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","4","4","4"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["0"],["2"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","-22528","-45056","-67584","22528","112640","202752","67584","-67584","-202752","-112640","-22528","67584","45056","22528"],["0","0","0","0","-11264","-5120","-301056","-203776","-111616","903168","678912","365568","-903168","-701440","-375808","301056","237568","126976"],["0","0","0","0","0","26624","-174592","-209920","-294912","523776","629760","724992","-523776","-629760","-671744","174592","209920","215040"],["0","0","0","0","0","1024","2048","-28672","-134144","-6144","86016","396288","6144","-86016","-394240","-2048","28672","131072"],["0","0","0","0","0","0","-1536","12288","-24576","4608","-36864","73728","-4608","36864","-73728","1536","-12288","24576"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","61440","122880","184320","-61440","-307200","-552960","-184320","184320","552960","307200","61440","-184320","-122880","-61440"],["0","0","0","0","0","-33792","135168","286720","299008","-284672","-860160","-694272","43008","860160","626688","227328","-286720","-197632","-120832"],["0","0","0","0","0","0","1024","-47104","51200","25600","141312","-153600","-82944","-141312","153600","84992","47104","-51200","-28672"],["0","0","0","0","0","0","3072","-15360","0","-58368","46080","0","156672","-46080","0","-150528","15360","0","49152"],["0","0","0","0","0","0","0","-1024","8192","-16384","3072","-24576","49152","-3072","24576","-49152","1024","-8192","16384"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","32768","65536","98304","-32768","-163840","-294912","-98304","98304","294912","163840","32768","-98304","-65536","-32768"],["0","0","0","0","0","0","-11264","59392","208896","186368","-90112","-626688","-491520","-86016","626688","468992","204800","-208896","-152576","-88064"],["0","0","0","0","0","0","0","-7168","29696","81920","95232","-89088","-245760","-242688","89088","245760","228352","-29696","-81920","-73728"],["0","0","0","0","0","0","0","1024","-7168","8192","13312","21504","-24576","-46080","-21504","24576","48128","7168","-8192","-16384"]]},"deriv_order":2}],"step_multiplier":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","-512","0","0","1536","0","0","-1536","0","0","512"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","256","-1024","0","-768","3072","0","768","-3072","0","-256","1024"],["0","0","0","256","-1024","0","-768","3072","0","768","-3072","0","-256","1024"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","-512","-512","-512","1536","1536","1536","-1536","-1536","-1536","512","512","512"],["0","0","0","0","1024","2048","0","-3072","-6144","0","3072","6144","0","-1024","-2048"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","-1024","-1024","-1024","3072","3072","3072","-3072","-3072","-3072","1024","1024","1024"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","512","1536","3072","3072","1536","-1536","-3072","-3072","-1536","-512"],["0","0","0","768","768","2304","1536","3072","0","-768","-3840","-2304","-1536"],["0","0","0","256","-768","-768","-1536","1536","1536","2304","-768","-768","-1024"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","-512","-2048","-4608","-6144","-4608","0","4608","6144","4608","2048","512"],["0","0","0","0","1024","3072","3072","0","-6144","-6144","-3072","3072","3072","2048"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","-1024","-2048","-3072","0","3072","6144","3072","0","-3072","-2048","-1024"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["1","7","-2"],["1","-5","4"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-2","-8","-8","6"],["0","4","4","-8"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-4","0","0","4"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","-22528","-83968","-200704","-276480","-245760","-43008","172032","301056","245760","133120","28672","-2048","-6144"],["0","0","0","0","-11264","-24576","-339968","-711680","-1078272","-528384","258048","1041408","887808","475136","61440","-19456","-10240"],["0","0","0","0","0","26624","-136192","-432128","-890880","-740352","-190464","688128","875520","663552","176128","1024","-40960"],["0","0","0","0","0","1024","4608","-29184","-167424","-276480","-273408","36864","244224","339456","129536","27648","-36864"],["0","0","0","0","0","0","-1536","9728","-7680","-12288","-55296","-12288","1536","53760","19968","12288","-8192"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","61440","217088","499712","634880","491520","-61440","-540672","-749568","-491520","-184320","40960","53248","28672"],["0","0","0","0","0","-33792","90112","424960","980992","1139712","632832","-334848","-1056768","-1047552","-645120","-173056","-10240","32768"],["0","0","0","0","0","0","1024","-53248","20480","150528","491520","448512","230400","-288768","-423936","-381952","-149504","-45056"],["0","0","0","0","0","0","3072","-11264","-17408","-73728","-12288","24576","193536","113664","58368","-122880","-90112","-65536"],["0","0","0","0","0","0","0","-1024","7168","-9216","-6144","-30720","18432","15360","39936","-9216","-8192","-16384"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","32768","98304","196608","163840","0","-294912","-393216","-294912","0","163840","196608","98304","32768"],["0","0","0","0","0","0","-11264","48128","257024","443392","353280","-273408","-764928","-850944","-224256","244736","449536","240640","88064"],["0","0","0","0","0","0","0","-7168","22528","104448","199680","110592","-135168","-377856","-288768","-43008","185344","155648","73728"],["0","0","0","0","0","0","0","1024","-6144","2048","15360","36864","12288","-33792","-55296","-30720","17408","24576","16384"]]},"deriv_order":2}],"step_multiplier":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","-512","0","0","1536","0","0","-1536","0","0","512"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","-512","-512","-512","1536","1536","1536","-1536","-1536","-1536","512","512","512"],["0","0","0","-768","768","-1536","2304","-2304","4608","-2304","2304","-4608","768","-768","1536"],["0","0","0","-256","1280","-1024","768","-3840","3072","-768","3840","-3072","256","-1280","1024"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","512","1024","1024","-1024","-3072","-3072","0","3072","3072","1024","-1024","-1024","-512"],["0","0","0","0","-1024","-1024","2048","3072","3072","-6144","-3072","-3072","6144","1024","1024","-2048"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","1024","0","0","-4096","0","0","6144","0","0","-4096","0","0","1024"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","-1024","-2048","-3072","0","3072","6144","3072","0","-3072","-2048","-1024"],["0","0","0","-1280","-1024","-3072","768","0","6144","2304","3072","-3072","-1792","-2048"],["0","0","0","-256","1024","0","768","-3072","0","-768","3072","0","256","-1024"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","512","2560","4608","4608","-1536","-7680","-10752","-4608","1536","5632","3584","1536"],["0","0","0","0","-1024","-2048","0","3072","6144","0","-3072","-6144","0","1024","2048"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","1024","1024","1024","-3072","-3072","-3072","3072","3072","3072","-1024","-1024","-1024"]]},"deriv_order":2}]]}],"restart_bases":[0],"row_multiplier":{"coeffs":[["0","0","0","-512","0","0","1536","0","0","-1536","0","0","512"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["1","1","1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-2","-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 = 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 2 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"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-1","-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 = 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":"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) = (2) + (2) x, V_n(x) = 0, W_n(x) = (-1) + (-1) x + (-1) x^2; open hypotheses: multipliers_vanish_at_zero: [x^0] c_2(n, x) = -1 is not the zero polynomial","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) = (2) + (2) x, B_n(x) = (-1) + (-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-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) = (2) + (2) x, B_n(x) = (-1) + (-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-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"}