{"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"],["2","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["3","6"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"basis_map_A013609 of Pascal-(1,3,1) array."},"identifying_rows":2,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["-12","-228","-1542","-4593","-6078","-2640","432"],["0","-72","-924","-3816","-6336","-3450","396"],["0","0","-132","-972","-2262","-1632","120"],["0","0","0","-72","-312","-330","12"],["0","0","0","0","-12","-24","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","-36","-684","-4626","-13779","-18234","-7920","1296"],["0","0","-216","-2772","-11448","-19008","-10350","1188"],["0","0","0","-396","-2916","-6786","-4896","360"],["0","0","0","0","-216","-936","-990","36"],["0","0","0","0","0","-36","-72","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0","-12","-228","-1542","-4593","-6078","-2640","432"],["0","0","0","-72","-924","-3816","-6336","-3450","396"],["0","0","0","0","-132","-972","-2262","-1632","120"],["0","0","0","0","0","-72","-312","-330","12"],["0","0","0","0","0","0","-12","-24","0"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["-8","-120","-620","-1374","-1304","-354","108"],["0","-48","-480","-1496","-1788","-616","108"],["0","0","-88","-488","-812","-370","36"],["0","0","0","-48","-144","-92","4"],["0","0","0","0","-8","-8","0"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-24","-360","-1860","-4122","-3912","-1062","324"],["0","0","-144","-1440","-4488","-5364","-1848","324"],["0","0","0","-264","-1464","-2436","-1110","108"],["0","0","0","0","-144","-432","-276","12"],["0","0","0","0","0","-24","-24","0"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["0","0","-8","-120","-620","-1374","-1304","-354","108"],["0","0","0","-48","-480","-1496","-1788","-616","108"],["0","0","0","0","-88","-488","-812","-370","36"],["0","0","0","0","0","-48","-144","-92","4"],["0","0","0","0","0","0","-8","-8","0"]]},"deriv_order":2,"shift":1},{"coeff":{"coeffs":[["4","44","162","235","98","-24"],["0","24","172","352","196","-32"],["0","0","44","164","138","-14"],["0","0","0","24","40","-2"],["0","0","0","0","4","0"]]},"deriv_order":0,"shift":2},{"coeff":{"coeffs":[["0","12","132","486","705","294","-72"],["0","0","72","516","1056","588","-96"],["0","0","0","132","492","414","-42"],["0","0","0","0","72","120","-6"],["0","0","0","0","0","12","0"]]},"deriv_order":1,"shift":2},{"coeff":{"coeffs":[["0","0","4","44","162","235","98","-24"],["0","0","0","24","172","352","196","-32"],["0","0","0","0","44","164","138","-14"],["0","0","0","0","0","24","40","-2"],["0","0","0","0","0","0","4","0"]]},"deriv_order":2,"shift":2}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0,1],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["1"],["2","8"]],"recurrence":{"denominator":{"coeffs":[["4","-4","-6","-5","2","0"],["0","24","-4","-16","-4","0"],["0","0","44","20","-6","-2"],["0","0","0","24","8","-2"],["0","0","0","0","4","0"]]},"terms":[{"coeff":{"coeffs":[["12","84","222","273","150","12","-24"],["0","72","396","792","648","114","-60"],["0","0","132","540","678","228","-48"],["0","0","0","72","216","138","-12"],["0","0","0","0","12","24","0"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["8","24","12","-50","-48","-6","-4"],["0","48","128","120","12","-16","-12"],["0","0","88","200","140","10","-12"],["0","0","0","48","80","28","-4"],["0","0","0","0","8","8","0"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["1","3","3","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"],["2","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["3","6"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_leader_shift":2,"parent_valid_from_base":0,"quotients":[{"differentiations":[{"coeff":{"coeffs":[["0","0","0","256","5888","59712","353408","1357456","3549792","6429852","8018760","6667986","3428839","902684","40584","-24352","-4112","-192"],["0","0","0","768","19200","208576","1308160","5281264","14425280","27164068","35107696","30221922","16144445","4514216","309232","-91888","-17296","-832"],["0","0","0","768","22272","270272","1848320","8004912","23191488","45957812","62185200","55916702","31290769","9359298","868638","-127052","-28968","-1456"],["0","0","0","256","10496","156480","1231616","5922704","18644608","39598812","56933056","54158050","32105803","10362214","1221848","-68848","-24336","-1312"],["0","0","0","0","1536","37888","385408","2189696","7793888","18258016","28526408","29242536","18649556","6565654","944980","2984","-10448","-640"],["0","0","0","0","0","2816","48896","369600","1595328","4325168","7611408","8645204","6060484","2359782","404016","18448","-1920","-160"],["0","0","0","0","0","0","1536","21760","133120","457920","964672","1267120","1006464","441476","88598","6948","8","-16"],["0","0","0","0","0","0","0","256","3072","15552","42880","69168","64896","32900","7704","816","32","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","768","17664","179136","1060224","4072368","10649376","19289556","24056280","20003958","10286517","2708052","121752","-73056","-12336","-576"],["0","0","0","0","2304","57600","625728","3924480","15843792","43275840","81492204","105323088","90665766","48433335","13542648","927696","-275664","-51888","-2496"],["0","0","0","0","2304","66816","810816","5544960","24014736","69574464","137873436","186555600","167750106","93872307","28077894","2605914","-381156","-86904","-4368"],["0","0","0","0","768","31488","469440","3694848","17768112","55933824","118796436","170799168","162474150","96317409","31086642","3665544","-206544","-73008","-3936"],["0","0","0","0","0","4608","113664","1156224","6569088","23381664","54774048","85579224","87727608","55948668","19696962","2834940","8952","-31344","-1920"],["0","0","0","0","0","0","8448","146688","1108800","4785984","12975504","22834224","25935612","18181452","7079346","1212048","55344","-5760","-480"],["0","0","0","0","0","0","0","4608","65280","399360","1373760","2894016","3801360","3019392","1324428","265794","20844","24","-48"],["0","0","0","0","0","0","0","0","768","9216","46656","128640","207504","194688","98700","23112","2448","96","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","256","5888","59712","353408","1357456","3549792","6429852","8018760","6667986","3428839","902684","40584","-24352","-4112","-192"],["0","0","0","0","0","768","19200","208576","1308160","5281264","14425280","27164068","35107696","30221922","16144445","4514216","309232","-91888","-17296","-832"],["0","0","0","0","0","768","22272","270272","1848320","8004912","23191488","45957812","62185200","55916702","31290769","9359298","868638","-127052","-28968","-1456"],["0","0","0","0","0","256","10496","156480","1231616","5922704","18644608","39598812","56933056","54158050","32105803","10362214","1221848","-68848","-24336","-1312"],["0","0","0","0","0","0","1536","37888","385408","2189696","7793888","18258016","28526408","29242536","18649556","6565654","944980","2984","-10448","-640"],["0","0","0","0","0","0","0","2816","48896","369600","1595328","4325168","7611408","8645204","6060484","2359782","404016","18448","-1920","-160"],["0","0","0","0","0","0","0","0","1536","21760","133120","457920","964672","1267120","1006464","441476","88598","6948","8","-16"],["0","0","0","0","0","0","0","0","0","256","3072","15552","42880","69168","64896","32900","7704","816","32","0"]]},"deriv_order":2}],"shift":0}],"row_annihilation":{"kind":"system","system":{"generators":[{"annihilator":{"terms":[{"coeff":{"coeffs":[["-2","-2"],["3","2"],["-4","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-12","-27","-6"],["8","16","2"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-4","-16","-17","-2"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["1"],["1"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","0","3584","68096","568192","2741760","8460128","17383552","23938280","21562048","11861156","3346422","205456","-77680","-14080","-672"],["0","0","0","0","0","10752","216576","1893504","9501824","30342560","64335456","91310552","84842168","48385716","14449996","1198252","-247896","-51248","-2528"],["0","0","0","0","0","10752","241152","2279552","12166016","40917408","90845600","134612696","130560648","78080308","24968296","2674632","-258896","-70112","-3648"],["0","0","0","0","0","3584","104960","1159552","6906240","25316576","60452896","95614856","98664424","62927564","21866532","2935168","-61216","-43456","-2496"],["0","0","0","0","0","0","12288","213504","1614464","6968960","18886368","33199712","37620344","26240664","10093450","1658392","55968","-10976","-800"],["0","0","0","0","0","0","0","8192","115712","705792","2420480","5082560","6651456","5258224","2289040","451284","33400","-272","-96"],["0","0","0","0","0","0","0","0","1536","18432","93312","257280","415008","389376","197400","46224","4896","192","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","-3584","-71680","-631680","-3243136","-10779104","-24316704","-37867272","-40447800","-28665660","-12420278","-2598310","48192","107888","15328","672"],["0","0","0","0","0","-7168","-154112","-1434368","-7686016","-26427840","-61229152","-97272656","-105313448","-75228600","-32861336","-7211460","-166316","201816","30832","1376"],["0","0","0","0","0","-3584","-93184","-976256","-5671296","-20637408","-49671776","-80593544","-87509608","-61396780","-25811358","-5563836","-375964","56536","10640","480"],["0","0","0","0","0","0","-10752","-176128","-1254016","-5063680","-12650784","-19894336","-18870520","-9140704","-646268","997324","99492","-53000","-10640","-544"],["0","0","0","0","0","0","0","-2560","-22528","-29952","392960","2299904","5944512","8599504","7057168","2963466","451468","-4520","-6384","-384"],["0","0","0","0","0","0","0","0","3072","46080","296704","1068288","2342592","3183040","2592720","1147056","221336","14352","-480","-64"],["0","0","0","0","0","0","0","0","0","1024","12288","62208","171520","276672","259584","131600","30816","3264","128","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","-1536","-31744","-290176","-1552256","-5402976","-12838624","-21195560","-24174280","-18445868","-8711878","-2069682","-38048","68432","10592","480"],["0","0","0","0","0","0","-3072","-69120","-676608","-3835008","-14041024","-34910368","-60069840","-71223064","-56481448","-27907920","-7219196","-413636","157320","27856","1312"],["0","0","0","0","0","0","-1536","-43008","-487296","-3081856","-12320608","-32978592","-60495976","-75964888","-63615948","-33370670","-9518300","-925308","98200","24592","1248"],["0","0","0","0","0","0","0","-5632","-105472","-868736","-4143360","-12655072","-25798400","-35405896","-32107280","-18256276","-5820156","-795980","-5224","7856","480"],["0","0","0","0","0","0","0","0","-4608","-70656","-474112","-1822720","-4410432","-6937984","-7063168","-4472832","-1613786","-280340","-17928","400","64"],["0","0","0","0","0","0","0","0","0","-1024","-13312","-74496","-233728","-448192","-536256","-391184","-162416","-34080","-3392","-128","0"]]},"deriv_order":2}],"step_multiplier":{"coeffs":[["0","0","0","64","768","3888","10720","17292","16224","8225","1926","204","8"],["0","0","0","192","2304","11664","32160","51876","48672","24675","5778","612","24"],["0","0","0","192","2304","11664","32160","51876","48672","24675","5778","612","24"],["0","0","0","64","768","3888","10720","17292","16224","8225","1926","204","8"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","64","1024","6960","26272","60172","85392","73121","34826","7908","824","32"],["0","0","0","-64","0","5328","35936","111348","191280","186463","96774","22908","2440","96"],["0","0","0","-576","-6144","-25776","-49824","-26988","61488","120663","81366","21276","2376","96"],["0","0","0","-704","-8192","-39696","-102368","-147332","-109296","-25579","11714","5460","728","32"],["0","0","0","-256","-3072","-15552","-42880","-69168","-64896","-32900","-7704","-816","-32","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-256","-3776","-24256","-88720","-202640","-297988","-280532","-163075","-54902","-9980","-904","-32"],["0","0","0","0","-384","-4992","-27936","-87648","-168072","-201096","-146694","-60906","-12780","-1272","-48"],["0","0","0","768","10560","62784","210288","432624","557820","439404","195837","42894","4380","168","0"],["0","0","0","512","7168","43520","149504","317632","427904","359968","179456","48898","7180","536","16"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","-256","-4096","-28928","-118272","-308320","-531584","-607888","-449696","-203905","-52488","-7448","-544","-16"],["0","0","0","-512","-8192","-57856","-236544","-616640","-1063168","-1215776","-899392","-407810","-104976","-14896","-1088","-32"],["0","0","0","-256","-4096","-28928","-118272","-308320","-531584","-607888","-449696","-203905","-52488","-7448","-544","-16"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","-256","-3584","-21568","-72448","-147152","-181792","-128108","-41056","226","2188","344","16"],["0","-768","-11008","-67776","-232896","-484336","-614544","-449220","-156068","-7026","5748","1000","48"],["0","-768","-11520","-73920","-264000","-570096","-752880","-579012","-221868","-22434","4116","936","48"],["0","-256","-4352","-30784","-119104","-275792","-389296","-322796","-139756","-22886","-260","248","16"],["0","0","-256","-3072","-15552","-42880","-69168","-64896","-32900","-7704","-816","-32","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","256","3840","25152","94016","219600","328944","309900","169164","40830","-2414","-2532","-360","-16"],["0","512","8192","57472","231552","588704","975520","1047704","698296","261116","44070","2116","-184","-16"],["0","256","4864","39488","181056","518608","964208","1165708","889100","399742","95382","11828","712","16"],["0","0","512","7168","43520","149504","317632","427904","359968","179456","48898","7180","536","16"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","-256","-4096","-28928","-118272","-308320","-531584","-607888","-449696","-203905","-52488","-7448","-544","-16"],["0","0","-512","-8192","-57856","-236544","-616640","-1063168","-1215776","-899392","-407810","-104976","-14896","-1088","-32"],["0","0","-256","-4096","-28928","-118272","-308320","-531584","-607888","-449696","-203905","-52488","-7448","-544","-16"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["4","4","-2"],["0","4","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-4","-4","10","4"],["0","-8","-16","-2"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","4","16","17","2"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","2048","37888","306688","1427200","4211584","8181952","10488864","8609360","4185248","989264","30152","-27088","-4256","-192"],["0","0","0","0","6144","120320","1018368","4916352","14978688","29976096","39599904","33631640","17115264","4403616","262884","-88104","-15696","-736"],["0","0","0","0","6144","133632","1218560","6232960","19933184","41682656","57505408","51211112","27664072","7844624","709528","-95984","-21856","-1088"],["0","0","0","0","2048","57856","612352","3473280","12049408","27042016","39891200","38075432","22282904","7070616","868208","-28576","-13888","-768"],["0","0","0","0","0","6656","109056","777600","3162240","8061792","13307232","14135624","9238200","3341304","524016","15456","-3648","-256"],["0","0","0","0","0","0","3584","48640","285056","939392","1896160","2387360","1819144","766760","148012","10696","-112","-32"],["0","0","0","0","0","0","0","512","6144","31104","85760","138336","129792","65800","15408","1632","64","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","-2048","-39936","-341504","-1690880","-5376128","-11478080","-16671712","-16273520","-10219792","-3708400","-528628","86240","39456","4736","192"],["0","0","0","0","-4096","-84992","-757760","-3851008","-12386816","-26318784","-37202816","-34090384","-18747152","-4953416","7736","247320","44496","2976","64"],["0","0","0","0","-2048","-50176","-488960","-2589440","-8316800","-16693184","-20097568","-11544720","2219168","7559312","3954464","549344","-41664","-13952","-768"],["0","0","0","0","0","-5120","-70656","-385280","-920320","4288","5904064","16535376","22966576","17610008","6817480","895472","-47776","-18496","-1024"],["0","0","0","0","0","0","2048","48128","444160","2215680","6710336","12882496","15662672","11530000","4577252","731808","13408","-6784","-448"],["0","0","0","0","0","0","0","4096","59392","371200","1302016","2790784","3719296","2983904","1309472","255416","17744","-352","-64"],["0","0","0","0","0","0","0","0","1024","12288","62208","171520","276672","259584","131600","30816","3264","128","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","-1536","-31744","-290176","-1552256","-5402976","-12838624","-21195560","-24174280","-18445868","-8711878","-2069682","-38048","68432","10592","480"],["0","0","0","0","0","-3072","-69120","-676608","-3835008","-14041024","-34910368","-60069840","-71223064","-56481448","-27907920","-7219196","-413636","157320","27856","1312"],["0","0","0","0","0","-1536","-43008","-487296","-3081856","-12320608","-32978592","-60495976","-75964888","-63615948","-33370670","-9518300","-925308","98200","24592","1248"],["0","0","0","0","0","0","-5632","-105472","-868736","-4143360","-12655072","-25798400","-35405896","-32107280","-18256276","-5820156","-795980","-5224","7856","480"],["0","0","0","0","0","0","0","-4608","-70656","-474112","-1822720","-4410432","-6937984","-7063168","-4472832","-1613786","-280340","-17928","400","64"],["0","0","0","0","0","0","0","0","-1024","-13312","-74496","-233728","-448192","-536256","-391184","-162416","-34080","-3392","-128","0"]]},"deriv_order":2}],"step_multiplier":{"coeffs":[["0","0","0","64","768","3888","10720","17292","16224","8225","1926","204","8"],["0","0","0","192","2304","11664","32160","51876","48672","24675","5778","612","24"],["0","0","0","192","2304","11664","32160","51876","48672","24675","5778","612","24"],["0","0","0","64","768","3888","10720","17292","16224","8225","1926","204","8"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","256","3584","21568","72448","147152","181792","128108","41056","-226","-2188","-344","-16"],["0","0","0","768","11008","67776","232896","484336","614544","449220","156068","7026","-5748","-1000","-48"],["0","0","0","768","11520","73920","264000","570096","752880","579012","221868","22434","-4116","-936","-48"],["0","0","0","256","4352","30784","119104","275792","389296","322796","139756","22886","260","-248","-16"],["0","0","0","0","256","3072","15552","42880","69168","64896","32900","7704","816","32","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-256","-3840","-25152","-94016","-219600","-328944","-309900","-169164","-40830","2414","2532","360","16"],["0","0","0","-512","-8192","-57472","-231552","-588704","-975520","-1047704","-698296","-261116","-44070","-2116","184","16"],["0","0","0","-256","-4864","-39488","-181056","-518608","-964208","-1165708","-889100","-399742","-95382","-11828","-712","-16"],["0","0","0","0","-512","-7168","-43520","-149504","-317632","-427904","-359968","-179456","-48898","-7180","-536","-16"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","256","4096","28928","118272","308320","531584","607888","449696","203905","52488","7448","544","16"],["0","0","0","0","512","8192","57856","236544","616640","1063168","1215776","899392","407810","104976","14896","1088","32"],["0","0","0","0","256","4096","28928","118272","308320","531584","607888","449696","203905","52488","7448","544","16"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","512","7232","44160","151856","320576","423756","341608","155233","34374","3532","136"],["0","0","1536","21952","135552","471120","1004608","1340436","1089720","498599","110826","11412","440"],["0","0","1536","22464","141696","502224","1090368","1478772","1219512","564399","126234","13044","504"],["0","0","512","8000","53376","198512","449216","631260","536296","253933","57486","5980","232"],["0","0","0","256","3072","15552","42880","69168","64896","32900","7704","816","32"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","-512","-7936","-54080","-212288","-527920","-860528","-917788","-618860","-244735","-50074","-4916","-184","0"],["0","0","-1024","-16384","-115328","-468096","-1205344","-2038688","-2263480","-1597688","-668926","-149046","-17012","-904","-16"],["0","0","-512","-8960","-68416","-299328","-826928","-1495792","-1773596","-1338796","-603647","-147870","-19276","-1256","-32"],["0","0","0","-512","-7168","-43520","-149504","-317632","-427904","-359968","-179456","-48898","-7180","-536","-16"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","256","4096","28928","118272","308320","531584","607888","449696","203905","52488","7448","544","16"],["0","0","0","512","8192","57856","236544","616640","1063168","1215776","899392","407810","104976","14896","1088","32"],["0","0","0","256","4096","28928","118272","308320","531584","607888","449696","203905","52488","7448","544","16"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["0","0","0","64","768","3888","10720","17292","16224","8225","1926","204","8"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-3","-6"]]},"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"],["2","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["3","6"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":1,"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) = (3) + (6) x; open hypotheses: multipliers_vanish_at_zero: [x^0] c_2(n, x) = 3 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 = 3 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 = 3 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) = (2) + (2) x, B_n(x) = (3) + (6) x: every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, -1/2] (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) = (3) + (6) x","every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, -1/2] (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"}
