{"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","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["3","3"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","1"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"basis_map_A007318 of Pascal-(1,3,1) array."},"identifying_rows":2,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["-192","-1824","-6168","-9186","-6078","-1320","108"],["0","-576","-3696","-7632","-6336","-1725","99"],["0","0","-528","-1944","-2262","-816","30"],["0","0","0","-144","-312","-165","3"],["0","0","0","0","-12","-12","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","-576","-5472","-18504","-27558","-18234","-3960","324"],["0","0","-1728","-11088","-22896","-19008","-5175","297"],["0","0","0","-1584","-5832","-6786","-2448","90"],["0","0","0","0","-432","-936","-495","9"],["0","0","0","0","0","-36","-36","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0","-192","-1824","-6168","-9186","-6078","-1320","108"],["0","0","0","-576","-3696","-7632","-6336","-1725","99"],["0","0","0","0","-528","-1944","-2262","-816","30"],["0","0","0","0","0","-144","-312","-165","3"],["0","0","0","0","0","0","-12","-12","0"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["-128","-960","-2480","-2748","-1304","-177","27"],["0","-384","-1920","-2992","-1788","-308","27"],["0","0","-352","-976","-812","-185","9"],["0","0","0","-96","-144","-46","1"],["0","0","0","0","-8","-4","0"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-384","-2880","-7440","-8244","-3912","-531","81"],["0","0","-1152","-5760","-8976","-5364","-924","81"],["0","0","0","-1056","-2928","-2436","-555","27"],["0","0","0","0","-288","-432","-138","3"],["0","0","0","0","0","-24","-12","0"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["0","0","-128","-960","-2480","-2748","-1304","-177","27"],["0","0","0","-384","-1920","-2992","-1788","-308","27"],["0","0","0","0","-352","-976","-812","-185","9"],["0","0","0","0","0","-96","-144","-46","1"],["0","0","0","0","0","0","-8","-4","0"]]},"deriv_order":2,"shift":1},{"coeff":{"coeffs":[["64","352","648","470","98","-12"],["0","192","688","704","196","-16"],["0","0","176","328","138","-7"],["0","0","0","48","40","-1"],["0","0","0","0","4","0"]]},"deriv_order":0,"shift":2},{"coeff":{"coeffs":[["0","192","1056","1944","1410","294","-36"],["0","0","576","2064","2112","588","-48"],["0","0","0","528","984","414","-21"],["0","0","0","0","144","120","-3"],["0","0","0","0","0","12","0"]]},"deriv_order":1,"shift":2},{"coeff":{"coeffs":[["0","0","64","352","648","470","98","-12"],["0","0","0","192","688","704","196","-16"],["0","0","0","0","176","328","138","-7"],["0","0","0","0","0","48","40","-1"],["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","4"]],"recurrence":{"denominator":{"coeffs":[["64","-32","-24","-10","2","0"],["0","192","-16","-32","-4","0"],["0","0","176","40","-6","-1"],["0","0","0","48","8","-1"],["0","0","0","0","4","0"]]},"terms":[{"coeff":{"coeffs":[["192","672","888","546","150","6","-6"],["0","576","1584","1584","648","57","-15"],["0","0","528","1080","678","114","-12"],["0","0","0","144","216","69","-3"],["0","0","0","0","12","12","0"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["128","192","48","-100","-48","-3","-1"],["0","384","512","240","12","-8","-3"],["0","0","352","400","140","5","-3"],["0","0","0","96","80","14","-1"],["0","0","0","0","8","4","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","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["3","3"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","1"]]},"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","262144","3014656","15286272","45236224","86877184","113593344","102877632","64150080","26671944","6857678","902684","20292","-6088","-514","-12"],["0","0","0","786432","9830400","53395456","167444480","338000896","461608960","434625088","280861568","120887688","32288890","4514216","154616","-22972","-2162","-52"],["0","0","0","786432","11403264","69189632","236584960","512314368","742127616","735324992","497481600","223666808","62581538","9359298","434319","-31763","-3621","-91"],["0","0","0","262144","5373952","40058880","157646848","379053056","596627456","633580992","455464448","216632200","64211606","10362214","610924","-17212","-3042","-82"],["0","0","0","0","786432","9699328","49332224","140140544","249404416","292128256","228211264","116970144","37299112","6565654","472490","746","-1306","-40"],["0","0","0","0","0","720896","6258688","23654400","51050496","69202688","60891264","34580816","12120968","2359782","202008","4612","-240","-10"],["0","0","0","0","0","0","196608","1392640","4259840","7326720","7717376","5068480","2012928","441476","44299","1737","1","-1"],["0","0","0","0","0","0","0","16384","98304","248832","343040","276672","129792","32900","3852","204","4","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","786432","9043968","45858816","135708672","260631552","340780032","308632896","192450240","80015832","20573034","2708052","60876","-18264","-1542","-36"],["0","0","0","0","2359296","29491200","160186368","502333440","1014002688","1384826880","1303875264","842584704","362663064","96866670","13542648","463848","-68916","-6486","-156"],["0","0","0","0","2359296","34209792","207568896","709754880","1536943104","2226382848","2205974976","1492444800","671000424","187744614","28077894","1302957","-95289","-10863","-273"],["0","0","0","0","786432","16121856","120176640","472940544","1137159168","1789882368","1900742976","1366393344","649896600","192634818","31086642","1832772","-51636","-9126","-246"],["0","0","0","0","0","2359296","29097984","147996672","420421632","748213248","876384768","684633792","350910432","111897336","19696962","1417470","2238","-3918","-120"],["0","0","0","0","0","0","2162688","18776064","70963200","153151488","207608064","182673792","103742448","36362904","7079346","606024","13836","-720","-30"],["0","0","0","0","0","0","0","589824","4177920","12779520","21980160","23152128","15205440","6038784","1324428","132897","5211","3","-3"],["0","0","0","0","0","0","0","0","49152","294912","746496","1029120","830016","389376","98700","11556","612","12","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","262144","3014656","15286272","45236224","86877184","113593344","102877632","64150080","26671944","6857678","902684","20292","-6088","-514","-12"],["0","0","0","0","0","786432","9830400","53395456","167444480","338000896","461608960","434625088","280861568","120887688","32288890","4514216","154616","-22972","-2162","-52"],["0","0","0","0","0","786432","11403264","69189632","236584960","512314368","742127616","735324992","497481600","223666808","62581538","9359298","434319","-31763","-3621","-91"],["0","0","0","0","0","262144","5373952","40058880","157646848","379053056","596627456","633580992","455464448","216632200","64211606","10362214","610924","-17212","-3042","-82"],["0","0","0","0","0","0","786432","9699328","49332224","140140544","249404416","292128256","228211264","116970144","37299112","6565654","472490","746","-1306","-40"],["0","0","0","0","0","0","0","720896","6258688","23654400","51050496","69202688","60891264","34580816","12120968","2359782","202008","4612","-240","-10"],["0","0","0","0","0","0","0","0","196608","1392640","4259840","7326720","7717376","5068480","2012928","441476","44299","1737","1","-1"],["0","0","0","0","0","0","0","0","0","16384","98304","248832","343040","276672","129792","32900","3852","204","4","0"]]},"deriv_order":2}],"shift":0}],"row_annihilation":{"kind":"system","system":{"generators":[{"annihilator":{"terms":[{"coeff":{"coeffs":[["-2","-1"],["3","1"],["-4","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-24","-27","-3"],["16","16","1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-16","-32","-17","-1"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["1"],["1"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","0","917504","8716288","36364288","87736320","135362048","139068416","95753120","43124096","11861156","1673211","51364","-9710","-880","-21"],["0","0","0","0","0","2752512","27721728","121184256","304058368","485480960","514683648","365242208","169684336","48385716","7224998","299563","-30987","-3203","-79"],["0","0","0","0","0","2752512","30867456","145891328","389312512","654678528","726764800","538450784","261121296","78080308","12484148","668658","-32362","-4382","-114"],["0","0","0","0","0","917504","13434880","74211328","220999680","405065216","483623168","382459424","197328848","62927564","10933266","733792","-7652","-2716","-78"],["0","0","0","0","0","0","1572864","13664256","51662848","111503360","151090944","132798848","75240688","26240664","5046725","414598","6996","-686","-25"],["0","0","0","0","0","0","0","524288","3702784","11292672","19363840","20330240","13302912","5258224","1144520","112821","4175","-17","-3"],["0","0","0","0","0","0","0","0","49152","294912","746496","1029120","830016","389376","98700","11556","612","12","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","-1835008","-18350080","-80855040","-207560704","-344931328","-389067264","-302938176","-161791200","-57331320","-12420278","-1299155","12048","13486","958","21"],["0","0","0","0","0","-3670016","-39452672","-183599104","-491905024","-845690880","-979666432","-778181248","-421253792","-150457200","-32861336","-3605730","-41579","25227","1927","43"],["0","0","0","0","0","-1835008","-23855104","-124960768","-362962944","-660397056","-794748416","-644748352","-350038432","-122793560","-25811358","-2781918","-93991","7067","665","15"],["0","0","0","0","0","0","-2752512","-22544384","-80257024","-162037760","-202412544","-159154688","-75482080","-18281408","-646268","498662","24873","-6625","-665","-17"],["0","0","0","0","0","0","0","-327680","-1441792","-958464","6287360","18399232","23778048","17199008","7057168","1481733","112867","-565","-399","-12"],["0","0","0","0","0","0","0","0","196608","1474560","4747264","8546304","9370368","6366080","2592720","573528","55334","1794","-30","-2"],["0","0","0","0","0","0","0","0","0","32768","196608","497664","686080","553344","259584","65800","7704","408","8","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","-786432","-8126464","-37142528","-99344384","-172895232","-205417984","-169564480","-96697120","-36891736","-8711878","-1034841","-9512","8554","662","15"],["0","0","0","0","0","0","-1572864","-17694720","-86605824","-245440512","-449312768","-558565888","-480558720","-284892256","-112962896","-27907920","-3609598","-103409","19665","1741","41"],["0","0","0","0","0","0","-786432","-11010048","-62373888","-197238784","-394259456","-527657472","-483967808","-303859552","-127231896","-33370670","-4759150","-231327","12275","1537","39"],["0","0","0","0","0","0","0","-1441792","-13500416","-55599104","-132587520","-202481152","-206387200","-141623584","-64214560","-18256276","-2910078","-198995","-653","491","15"],["0","0","0","0","0","0","0","0","-589824","-4521984","-15171584","-29163520","-35283456","-27751936","-14126336","-4472832","-806893","-70085","-2241","25","2"],["0","0","0","0","0","0","0","0","0","-65536","-425984","-1191936","-1869824","-1792768","-1072512","-391184","-81208","-8520","-424","-8","0"]]},"deriv_order":2}],"step_multiplier":{"coeffs":[["0","0","0","4096","24576","62208","85760","69168","32448","8225","963","51","1"],["0","0","0","12288","73728","186624","257280","207504","97344","24675","2889","153","3"],["0","0","0","12288","73728","186624","257280","207504","97344","24675","2889","153","3"],["0","0","0","4096","24576","62208","85760","69168","32448","8225","963","51","1"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","4096","32768","111360","210176","240688","170784","73121","17413","1977","103","2"],["0","0","0","-4096","0","85248","287488","445392","382560","186463","48387","5727","305","6"],["0","0","0","-36864","-196608","-412416","-398592","-107952","122976","120663","40683","5319","297","6"],["0","0","0","-45056","-262144","-635136","-818944","-589328","-218592","-25579","5857","1365","91","2"],["0","0","0","-16384","-98304","-248832","-343040","-276672","-129792","-32900","-3852","-204","-4","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-32768","-241664","-776192","-1419520","-1621120","-1191952","-561064","-163075","-27451","-2495","-113","-2"],["0","0","0","0","-24576","-159744","-446976","-701184","-672288","-402192","-146694","-30453","-3195","-159","-3"],["0","0","0","98304","675840","2009088","3364608","3460992","2231280","878808","195837","21447","1095","21","0"],["0","0","0","65536","458752","1392640","2392064","2541056","1711616","719936","179456","24449","1795","67","1"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","-65536","-524288","-1851392","-3784704","-4933120","-4252672","-2431552","-899392","-203905","-26244","-1862","-68","-1"],["0","0","0","-131072","-1048576","-3702784","-7569408","-9866240","-8505344","-4863104","-1798784","-407810","-52488","-3724","-136","-2"],["0","0","0","-65536","-524288","-1851392","-3784704","-4933120","-4252672","-2431552","-899392","-203905","-26244","-1862","-68","-1"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","-32768","-229376","-690176","-1159168","-1177216","-727168","-256216","-41056","113","547","43","1"],["0","-98304","-704512","-2168832","-3726336","-3874688","-2458176","-898440","-156068","-3513","1437","125","3"],["0","-98304","-737280","-2365440","-4224000","-4560768","-3011520","-1158024","-221868","-11217","1029","117","3"],["0","-32768","-278528","-985088","-1905664","-2206336","-1557184","-645592","-139756","-11443","-65","31","1"],["0","0","-16384","-98304","-248832","-343040","-276672","-129792","-32900","-3852","-204","-4","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","65536","491520","1609728","3008512","3513600","2631552","1239600","338328","40830","-1207","-633","-45","-1"],["0","131072","1048576","3678208","7409664","9419264","7804160","4190816","1396592","261116","22035","529","-23","-1"],["0","65536","622592","2527232","5793792","8297728","7713664","4662832","1778200","399742","47691","2957","89","1"],["0","0","65536","458752","1392640","2392064","2541056","1711616","719936","179456","24449","1795","67","1"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","-65536","-524288","-1851392","-3784704","-4933120","-4252672","-2431552","-899392","-203905","-26244","-1862","-68","-1"],["0","0","-131072","-1048576","-3702784","-7569408","-9866240","-8505344","-4863104","-1798784","-407810","-52488","-3724","-136","-2"],["0","0","-65536","-524288","-1851392","-3784704","-4933120","-4252672","-2431552","-899392","-203905","-26244","-1862","-68","-1"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["8","4","-1"],["0","4","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-16","-8","10","2"],["0","-16","-16","-1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","16","32","17","1"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","524288","4849664","19628032","45670400","67385344","65455616","41955456","17218720","4185248","494632","7538","-3386","-266","-6"],["0","0","0","0","1572864","15400960","65175552","157323264","239659008","239808768","158399616","67263280","17115264","2201808","65721","-11013","-981","-23"],["0","0","0","0","1572864","17104896","77987840","199454720","318930944","333461248","230021632","102422224","27664072","3922312","177382","-11998","-1366","-34"],["0","0","0","0","524288","7405568","39190528","111144960","192790528","216336128","159564800","76150864","22282904","3535308","217052","-3572","-868","-24"],["0","0","0","0","0","851968","6979584","24883200","50595840","64494336","53228928","28271248","9238200","1670652","131004","1932","-228","-8"],["0","0","0","0","0","0","229376","1556480","4560896","7515136","7584640","4774720","1819144","383380","37003","1337","-7","-1"],["0","0","0","0","0","0","0","16384","98304","248832","343040","276672","129792","32900","3852","204","4","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","-1048576","-10223616","-43712512","-108216320","-172036096","-183649280","-133373696","-65094080","-20439584","-3708400","-264314","21560","4932","296","6"],["0","0","0","0","-2097152","-21757952","-96993280","-246464512","-396378112","-421100544","-297622528","-136361536","-37494304","-4953416","3868","61830","5562","186","2"],["0","0","0","0","-1048576","-12845056","-62586880","-165724160","-266137600","-267090944","-160780544","-46178880","4438336","7559312","1977232","137336","-5208","-872","-24"],["0","0","0","0","0","-1310720","-9043968","-24657920","-29450240","68608","47232512","66141504","45933152","17610008","3408740","223868","-5972","-1156","-32"],["0","0","0","0","0","0","262144","3080192","14213120","35450880","53682688","51529984","31325344","11530000","2288626","182952","1676","-424","-14"],["0","0","0","0","0","0","0","262144","1900544","5939200","10416128","11163136","7438592","2983904","654736","63854","2218","-22","-2"],["0","0","0","0","0","0","0","0","32768","196608","497664","686080","553344","259584","65800","7704","408","8","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","-786432","-8126464","-37142528","-99344384","-172895232","-205417984","-169564480","-96697120","-36891736","-8711878","-1034841","-9512","8554","662","15"],["0","0","0","0","0","-1572864","-17694720","-86605824","-245440512","-449312768","-558565888","-480558720","-284892256","-112962896","-27907920","-3609598","-103409","19665","1741","41"],["0","0","0","0","0","-786432","-11010048","-62373888","-197238784","-394259456","-527657472","-483967808","-303859552","-127231896","-33370670","-4759150","-231327","12275","1537","39"],["0","0","0","0","0","0","-1441792","-13500416","-55599104","-132587520","-202481152","-206387200","-141623584","-64214560","-18256276","-2910078","-198995","-653","491","15"],["0","0","0","0","0","0","0","-589824","-4521984","-15171584","-29163520","-35283456","-27751936","-14126336","-4472832","-806893","-70085","-2241","25","2"],["0","0","0","0","0","0","0","0","-65536","-425984","-1191936","-1869824","-1792768","-1072512","-391184","-81208","-8520","-424","-8","0"]]},"deriv_order":2}],"step_multiplier":{"coeffs":[["0","0","0","4096","24576","62208","85760","69168","32448","8225","963","51","1"],["0","0","0","12288","73728","186624","257280","207504","97344","24675","2889","153","3"],["0","0","0","12288","73728","186624","257280","207504","97344","24675","2889","153","3"],["0","0","0","4096","24576","62208","85760","69168","32448","8225","963","51","1"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","32768","229376","690176","1159168","1177216","727168","256216","41056","-113","-547","-43","-1"],["0","0","0","98304","704512","2168832","3726336","3874688","2458176","898440","156068","3513","-1437","-125","-3"],["0","0","0","98304","737280","2365440","4224000","4560768","3011520","1158024","221868","11217","-1029","-117","-3"],["0","0","0","32768","278528","985088","1905664","2206336","1557184","645592","139756","11443","65","-31","-1"],["0","0","0","0","16384","98304","248832","343040","276672","129792","32900","3852","204","4","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-65536","-491520","-1609728","-3008512","-3513600","-2631552","-1239600","-338328","-40830","1207","633","45","1"],["0","0","0","-131072","-1048576","-3678208","-7409664","-9419264","-7804160","-4190816","-1396592","-261116","-22035","-529","23","1"],["0","0","0","-65536","-622592","-2527232","-5793792","-8297728","-7713664","-4662832","-1778200","-399742","-47691","-2957","-89","-1"],["0","0","0","0","-65536","-458752","-1392640","-2392064","-2541056","-1711616","-719936","-179456","-24449","-1795","-67","-1"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","65536","524288","1851392","3784704","4933120","4252672","2431552","899392","203905","26244","1862","68","1"],["0","0","0","0","131072","1048576","3702784","7569408","9866240","8505344","4863104","1798784","407810","52488","3724","136","2"],["0","0","0","0","65536","524288","1851392","3784704","4933120","4252672","2431552","899392","203905","26244","1862","68","1"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","65536","462848","1413120","2429696","2564608","1695024","683216","155233","17187","883","17"],["0","0","196608","1404928","4337664","7537920","8036864","5361744","2179440","498599","55413","2853","55"],["0","0","196608","1437696","4534272","8035584","8722944","5915088","2439024","564399","63117","3261","63"],["0","0","65536","512000","1708032","3176192","3593728","2525040","1072592","253933","28743","1495","29"],["0","0","0","16384","98304","248832","343040","276672","129792","32900","3852","204","4"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","-131072","-1015808","-3461120","-6793216","-8446720","-6884224","-3671152","-1237720","-244735","-25037","-1229","-23","0"],["0","0","-262144","-2097152","-7380992","-14979072","-19285504","-16309504","-9053920","-3195376","-668926","-74523","-4253","-113","-1"],["0","0","-131072","-1146880","-4378624","-9578496","-13230848","-11966336","-7094384","-2677592","-603647","-73935","-4819","-157","-2"],["0","0","0","-65536","-458752","-1392640","-2392064","-2541056","-1711616","-719936","-179456","-24449","-1795","-67","-1"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","65536","524288","1851392","3784704","4933120","4252672","2431552","899392","203905","26244","1862","68","1"],["0","0","0","131072","1048576","3702784","7569408","9866240","8505344","4863104","1798784","407810","52488","3724","136","2"],["0","0","0","65536","524288","1851392","3784704","4933120","4252672","2431552","899392","203905","26244","1862","68","1"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["0","0","0","4096","24576","62208","85760","69168","32448","8225","963","51","1"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-3","-3"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-2","-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 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","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["3","3"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","1"]]},"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) + (1) x, V_n(x) = 0, W_n(x) = (3) + (3) 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) + (1) x, B_n(x) = (3) + (3) x: every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, -1] (so its coefficients have one sign); for n >= 1, P_(n-1) interlaces P_n (weakly, in the sense of Liu and Wang), and deg P_n - deg P_(n-1) is 0 or 1 for n >= 2","route":"liu_wang_three_term","success":true,"variant":"liu_wang_three_term"}],"conditional_on":[],"interlacing":{"from_index":1,"justification":{"premises":["every hypothesis of the theorem is verified exactly for every index: P_n = A_n(x) P_(n-1) + B_n(x) P_(n-2) for n >= 2, with A_n(x) = (2) + (1) x, B_n(x) = (3) + (3) x","every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, -1] (so its coefficients have one sign); for n >= 1, P_(n-1) interlaces P_n (weakly, in the sense of Liu and Wang), and deg P_n - deg P_(n-1) is 0 or 1 for n >= 2"],"theorem":"liu_wang_three_term: L. L. Liu and Y. Wang, Adv. Appl. Math. 38 (2007) 542-560, Theorem 2.1 and Corollary 2.4 (A unified approach to polynomial sequences with only real zeros; the lag row as the interlacer, b_n = 0), weak interlacing of consecutive rows, with nonnegativity of the coefficients replaced, where a root region is certified, by an exact root-location induction"},"kind":"weak","orientation":"previous_interlaces_next"},"route":"liu_wang_three_term","rows_checked":10,"statement":"every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign","status":"proved"},"rows_compared":16,"schema":"polytool.recurrence-preserver-image.v1","statement":"proved: Q_n = lambda(n) T_n(P_(n+0)) with T = 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"}
