{"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","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","2"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"Triangular array:  row n gives the coefficients of the polynomial p(n,x) defined in Comments."},"identifying_rows":2,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["0","-32","-1284","-8792","-2352","-288"],["0","-16","-1024","-8480","-1760","-192"],["0","-2","-272","-3104","-416","-32"],["0","0","-24","-512","-32","0"],["0","0","0","-32","0","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","0","-96","-3852","-26376","-7056","-864"],["0","0","-48","-3072","-25440","-5280","-576"],["0","0","-6","-816","-9312","-1248","-96"],["0","0","0","-72","-1536","-96","0"],["0","0","0","0","-96","0","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0","0","-32","-1284","-8792","-2352","-288"],["0","0","0","-16","-1024","-8480","-1760","-192"],["0","0","0","-2","-272","-3104","-416","-32"],["0","0","0","0","-24","-512","-32","0"],["0","0","0","0","0","-32","0","0"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["-9","-366","-3104","-7296","-2288","-288"],["-6","-356","-3376","-7008","-1696","-192"],["-1","-114","-1384","-2640","-400","-32"],["0","-12","-248","-464","-32","0"],["0","0","-16","-32","0","0"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-27","-1098","-9312","-21888","-6864","-864"],["0","-18","-1068","-10128","-21024","-5088","-576"],["0","-3","-342","-4152","-7920","-1200","-96"],["0","0","-36","-744","-1392","-96","0"],["0","0","0","-48","-96","0","0"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["0","0","-9","-366","-3104","-7296","-2288","-288"],["0","0","-6","-356","-3376","-7008","-1696","-192"],["0","0","-1","-114","-1384","-2640","-400","-32"],["0","0","0","-12","-248","-464","-32","0"],["0","0","0","0","-16","-32","0","0"]]},"deriv_order":2,"shift":1},{"coeff":{"coeffs":[["9","254","1468","488","64"],["6","276","1840","512","64"],["1","100","880","160","16"],["0","12","192","16","0"],["0","0","16","0","0"]]},"deriv_order":0,"shift":2},{"coeff":{"coeffs":[["0","27","762","4404","1464","192"],["0","18","828","5520","1536","192"],["0","3","300","2640","480","48"],["0","0","36","576","48","0"],["0","0","0","48","0","0"]]},"deriv_order":1,"shift":2},{"coeff":{"coeffs":[["0","0","9","254","1468","488","64"],["0","0","6","276","1840","512","64"],["0","0","1","100","880","160","16"],["0","0","0","12","192","16","0"],["0","0","0","0","16","0","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"],["1","16"]],"recurrence":{"denominator":{"coeffs":[["1","6","28","-24","0"],["2","20","112","64","0"],["1","28","112","64","16"],["0","12","64","16","0"],["0","0","16","0","0"]]},"terms":[{"coeff":{"coeffs":[["0","8","132","664","240","32"],["0","8","224","1184","480","64"],["0","2","128","800","224","32"],["0","0","24","256","32","0"],["0","0","0","32","0","0"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["1","14","160","640","240","32"],["2","44","304","992","480","64"],["1","42","280","624","208","32"],["0","12","120","208","32","0"],["0","0","16","32","0","0"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["1"],"operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["2"]},{"denominator":["1"],"numerator":["1"]}],"shape":"euler_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["1","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","2"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_leader_shift":2,"parent_valid_from_base":0,"quotients":[{"differentiations":[{"coeff":{"coeffs":[["0","0","0","-4608","-295936","-7479296","-94339072","-613105664","-1860993024","-1928331264","-951058432","-250216448","-34865152","-2097152","0","0","0"],["0","0","0","-9984","-681984","-17724416","-222183424","-1354735616","-3221716992","392724480","3275096064","2208366592","662700032","99352576","6291456","0","0"],["0","0","0","-8576","-646400","-17590784","-221760512","-1274187776","-2125701120","4660903936","4332224512","-364347392","-1383661568","-544342016","-92012544","-6291456","0"],["0","0","0","-3648","-322304","-9410560","-121345024","-665048064","-609697792","4676681728","707887104","-3067396096","-1526923264","-72351744","100401152","25427968","2097152"],["0","0","0","-768","-89088","-2892288","-39163904","-210282496","-34988032","2210971648","-1058209792","-1989672960","-107479040","464912384","189267968","30932992","2097152"],["0","0","0","-64","-12928","-497152","-7405568","-41004032","19994624","582664192","-622788608","-518373376","247496704","264896512","74448896","9175040","524288"],["0","0","0","0","-768","-41472","-750592","-4675584","4202496","84721664","-135168000","-56819712","82903040","53870592","10223616","524288","0"],["0","0","0","0","0","-1024","-30720","-245760","229376","5406720","-10813440","-1835008","7864320","3932160","524288","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","-13824","-887808","-22437888","-283017216","-1839316992","-5582979072","-5784993792","-2853175296","-750649344","-104595456","-6291456","0","0","0"],["0","0","0","0","-29952","-2045952","-53173248","-666550272","-4064206848","-9665150976","1178173440","9825288192","6625099776","1988100096","298057728","18874368","0","0"],["0","0","0","0","-25728","-1939200","-52772352","-665281536","-3822563328","-6377103360","13982711808","12996673536","-1093042176","-4150984704","-1633026048","-276037632","-18874368","0"],["0","0","0","0","-10944","-966912","-28231680","-364035072","-1995144192","-1829093376","14030045184","2123661312","-9202188288","-4580769792","-217055232","301203456","76283904","6291456"],["0","0","0","0","-2304","-267264","-8676864","-117491712","-630847488","-104964096","6632914944","-3174629376","-5969018880","-322437120","1394737152","567803904","92798976","6291456"],["0","0","0","0","-192","-38784","-1491456","-22216704","-123012096","59983872","1747992576","-1868365824","-1555120128","742490112","794689536","223346688","27525120","1572864"],["0","0","0","0","0","-2304","-124416","-2251776","-14026752","12607488","254164992","-405504000","-170459136","248709120","161611776","30670848","1572864","0"],["0","0","0","0","0","0","-3072","-92160","-737280","688128","16220160","-32440320","-5505024","23592960","11796480","1572864","0","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","-4608","-295936","-7479296","-94339072","-613105664","-1860993024","-1928331264","-951058432","-250216448","-34865152","-2097152","0","0","0"],["0","0","0","0","0","-9984","-681984","-17724416","-222183424","-1354735616","-3221716992","392724480","3275096064","2208366592","662700032","99352576","6291456","0","0"],["0","0","0","0","0","-8576","-646400","-17590784","-221760512","-1274187776","-2125701120","4660903936","4332224512","-364347392","-1383661568","-544342016","-92012544","-6291456","0"],["0","0","0","0","0","-3648","-322304","-9410560","-121345024","-665048064","-609697792","4676681728","707887104","-3067396096","-1526923264","-72351744","100401152","25427968","2097152"],["0","0","0","0","0","-768","-89088","-2892288","-39163904","-210282496","-34988032","2210971648","-1058209792","-1989672960","-107479040","464912384","189267968","30932992","2097152"],["0","0","0","0","0","-64","-12928","-497152","-7405568","-41004032","19994624","582664192","-622788608","-518373376","247496704","264896512","74448896","9175040","524288"],["0","0","0","0","0","0","-768","-41472","-750592","-4675584","4202496","84721664","-135168000","-56819712","82903040","53870592","10223616","524288","0"],["0","0","0","0","0","0","0","-1024","-30720","-245760","229376","5406720","-10813440","-1835008","7864320","3932160","524288","0","0"]]},"deriv_order":2}],"shift":0}],"row_annihilation":{"kind":"system","system":{"generators":[{"annihilator":{"terms":[{"coeff":{"coeffs":[["-4","-16"],["4","-24"],["4","-8"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-1","10","20","-8"],["-1","-10","20","8"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","1","10","-20","-8"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["4"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","5120","133632","-183296","-35143680","-381386752","-1457307648","-1597210624","-806879232","-215220224","-30277632","-1835008","0","0","0"],["0","0","0","0","11776","246528","-3006464","-120310784","-1111564288","-3455901696","-596738048","2326757376","1776025600","556466176","85458944","5505024","0","0"],["0","0","0","0","10752","154496","-5809920","-157033984","-1282409472","-3035566080","4117831680","5084168192","623345664","-912424960","-429588480","-77463552","-5505024","0"],["0","0","0","0","4864","23872","-4738304","-105073664","-778830848","-1251650560","5401403392","1759969280","-3059056640","-1933328384","-287375360","50069504","19660800","1835008"],["0","0","0","0","1088","-13056","-1985536","-39613952","-274869248","-233347072","2939748352","-963756032","-2539995136","-362676224","473694208","217186304","37486592","2621440"],["0","0","0","0","96","-5696","-437760","-8506880","-57766400","-7498752","841646080","-786317312","-748019712","279199744","344326144","101842944","13238272","786432"],["0","0","0","0","0","-640","-45824","-972288","-6882304","3371008","127082496","-191021056","-87326720","114524160","76611584","14811136","786432","0"],["0","0","0","0","0","0","-1536","-46080","-368640","344064","8110080","-16220160","-2752512","11796480","5898240","786432","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","31488","1436672","25627648","224755712","1001709568","2141552640","1957527552","908066816","230096896","31195136","1835008","0","0","0"],["0","0","0","0","0","70272","3126528","53016064","416709632","1406881792","908304384","-3164749824","-4482564096","-2401206272","-650051584","-91357184","-5505024","0","0"],["0","0","0","0","0","62272","2725888","44137984","305059840","612428800","-1666744320","-3959668736","89718784","3145252864","2105540608","616431616","89653248","5505024","0"],["0","0","0","0","0","27360","1199680","18722048","109486592","-8824320","-1621009408","-164175872","2802302976","1558716416","-455753728","-608894976","-201195520","-30015488","-1835008"],["0","0","0","0","0","5952","272640","4166400","18231808","-88619008","-577583104","1080844288","812466176","-656130048","-711852032","-206110720","-10878976","4194304","524288"],["0","0","0","0","0","512","28160","426752","398848","-29785088","-92477440","485613568","-179191808","-429752320","-28639232","105840640","44957696","7602176","524288"],["0","0","0","0","0","0","768","7680","-289792","-4282368","-4595712","84721664","-99975168","-63111168","53411840","41287680","8650752","524288","0"],["0","0","0","0","0","0","0","-1024","-30720","-245760","229376","5406720","-10813440","-1835008","7864320","3932160","524288","0","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","12032","577536","11035648","106364928","538271744","1334181888","1295286272","619708416","160104448","22020096","1310720","0","0","0"],["0","0","0","0","0","0","26752","1269504","23580160","212964352","920539136","1376673792","-1185824768","-2585886720","-1536524288","-437583872","-63569920","-3932160","0","0"],["0","0","0","0","0","0","23616","1124096","20576256","175606784","628872192","152985600","-2873524224","-1414168576","1169866752","1163067392","386924544","60555264","3932160","0"],["0","0","0","0","0","0","10336","507328","9377536","76943872","218741248","-337103872","-1613619200","698138624","1542037504","357056512","-178847744","-100532224","-18481152","-1310720"],["0","0","0","0","0","0","2240","120576","2352896","19131904","40554496","-180865024","-376709120","623558656","444514304","-201457664","-223674368","-66715648","-8912896","-524288"],["0","0","0","0","0","0","192","13696","307968","2601472","3739648","-37490688","-32350208","147865600","29540352","-92045312","-53018624","-9830400","-524288","0"],["0","0","0","0","0","0","0","512","16384","153600","131072","-2932736","0","11730944","-2097152","-9830400","-4194304","-524288","0","0"]]},"deriv_order":2}],"step_multiplier":{"coeffs":[["0","0","0","-512","-18432","-227328","-1032192","-909312","-294912","-32768","0","0","0"],["0","0","0","-768","-26112","-285696","-866304","1732608","2285568","835584","98304","0","0"],["0","0","0","-384","-12288","-116736","-147456","1732608","-589824","-1867776","-786432","-98304","0"],["0","0","0","-64","-1920","-15360","14336","337920","-675840","-114688","491520","245760","32768"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","-1024","-31744","-270336","208896","8503296","8503296","2883584","327680","0","0","0"],["0","0","0","-3072","-94720","-807936","301056","19722240","-4546560","-18333696","-7831552","-983040","0","0"],["0","0","0","-3584","-108800","-897024","552960","19955712","-27451392","-17629184","9109504","6684672","983040","0"],["0","0","0","-2048","-60800","-472320","612352","10670080","-25006080","3088384","16875520","2949120","-1409024","-327680"],["0","0","0","-576","-16640","-119040","282624","2897920","-9461760","5726208","5570560","-2703360","-2162688","-327680"],["0","0","0","-64","-1792","-11520","45056","309248","-1351680","1236992","720896","-737280","-458752","-65536"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","256","9216","108544","331776","-1818624","-10174464","-9076736","-2949120","-327680","0","0","0","0"],["0","0","0","512","18944","235520","905216","-2088960","-13074432","11042816","19595264","7602176","917504","0","0","0"],["0","0","0","384","14592","187392","749568","-1781760","-10985472","19267584","7274496","-10125312","-5701632","-786432","0","0"],["0","0","0","128","4992","65024","240128","-995328","-4673536","13746176","-1622016","-9797632","-2523136","393216","131072","0"],["0","0","0","16","640","8320","25088","-200960","-634880","3436544","-2539520","-3215360","1605632","2129920","655360","65536"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","-128","-5888","-100352","-733184","-1634304","3268608","5865472","3211264","753664","65536","0","0","0"],["0","0","0","0","-192","-8448","-132864","-798720","-251904","9805824","-1007616","-12779520","-8503296","-2162688","-196608","0","0"],["0","0","0","0","-96","-4032","-57984","-266496","672768","5154816","-10309632","-5382144","8527872","7421952","2064384","196608","0"],["0","0","0","0","-16","-640","-8320","-25088","200960","634880","-3436544","2539520","3215360","-1605632","-2129920","-655360","-65536"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","-512","-16128","-147456","-118784","2408448","-1941504","-2097152","196608","393216","65536","0"],["0","0","0","-1280","-38784","-319744","161792","6533120","-11882496","-1728512","7569408","2883584","32768","-65536"],["0","0","0","-1152","-33792","-253440","442368","5910528","-16220160","6045696","10223616","-1474560","-2359296","-393216"],["0","0","0","-448","-12800","-88320","253952","2222080","-8110080","5955584","4587520","-3194880","-2228224","-327680"],["0","0","0","-64","-1792","-11520","45056","309248","-1351680","1236992","720896","-737280","-458752","-65536"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","128","4480","50944","157696","-507904","-1634304","2367488","1736704","-425984","-425984","-65536","0","0"],["0","0","0","192","6976","83456","277760","-1005568","-3971072","9240576","925696","-5324800","-1687552","131072","65536","0"],["0","0","0","96","3648","45696","151296","-771072","-2955264","10309632","-3416064","-6955008","-49152","1081344","196608","0"],["0","0","0","16","640","8320","25088","-200960","-634880","3436544","-2539520","-3215360","1605632","2129920","655360","65536"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","-64","-2816","-44288","-266240","-83968","3268608","-335872","-4259840","-2834432","-720896","-65536","0","0"],["0","0","0","0","-64","-2688","-38656","-177664","448512","3436544","-6873088","-3588096","5685248","4947968","1376256","131072","0"],["0","0","0","0","-16","-640","-8320","-25088","200960","634880","-3436544","2539520","3215360","-1605632","-2129920","-655360","-65536"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0"],["-8","16"],["-12","24"],["-4","8"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["2","-12","-16","0"],["3","14","-12","8"],["1","10","-20","-8"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-2","-24","-8","0"],["0","-1","-10","20","8"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","2560","58112","-389632","-19820544","-162791424","-228040704","1530118144","2249326592","1252130816","350158848","50724864","3145728","0","0"],["0","0","0","0","4608","78592","-1778944","-51106816","-366169088","-255246336","4307001344","3190620160","-522747904","-1156513792","-437583872","-73138176","-4980736","0"],["0","0","0","0","3072","27584","-2270720","-50480640","-327276544","-12352512","4566712320","208158720","-3555590144","-1880997888","-231866368","60948480","20447232","1835008"],["0","0","0","0","896","-4864","-1280000","-24886784","-152453120","79349760","2451980288","-1477656576","-2575007744","-279707648","503578624","221380608","37748736","2621440"],["0","0","0","0","96","-4416","-349696","-6527488","-40120832","36189184","731152384","-864141312","-729407488","301285376","349044736","102105088","13238272","786432"],["0","0","0","0","0","-640","-42752","-869888","-5809152","6074368","117841920","-195543040","-84574208","116359168","76873728","14811136","786432","0"],["0","0","0","0","0","0","-1536","-46080","-368640","344064","8110080","-16220160","-2752512","11796480","5898240","786432","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","15744","674816","10799616","75714560","169734144","-469204992","-2496970752","-2798780416","-1412726784","-374603776","-52297728","-3145728","0","0"],["0","0","0","0","0","27264","1150592","17663744","109641216","106761216","-1306161152","-2959253504","325173248","2789998592","1847623680","544407552","80084992","4980736","0"],["0","0","0","0","0","17504","739392","11013376","58985984","-51422720","-1106764800","-426450944","2258714624","1526308864","-294141952","-532348928","-186777600","-28966912","-1835008"],["0","0","0","0","0","4928","216576","3197696","13640192","-63975424","-416897024","705093632","648298496","-406110208","-508100608","-146341888","-2490368","4718592","524288"],["0","0","0","0","0","512","26624","402176","728576","-22559744","-72439808","382394368","-176635904","-334594048","22347776","115277824","45481984","7602176","524288"],["0","0","0","0","0","0","768","9728","-224256","-3659776","-3809280","75481088","-96829440","-53149696","57606144","41811968","8650752","524288","0"],["0","0","0","0","0","0","0","-1024","-30720","-245760","229376","5406720","-10813440","-1835008","7864320","3932160","524288","0","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","6016","276736","4940288","42146816","162770944","128819200","-686538752","-985432064","-539656192","-149094400","-21364736","-1310720","0","0"],["0","0","0","0","0","0","10368","475648","8327168","66768896","208066560","-133840896","-1497497600","-300941312","1102020608","852623360","267386880","40894464","2621440","0"],["0","0","0","0","0","0","6624","310976","5476096","42169856","101564928","-277392384","-974839808","819412992","1147150336","87375872","-250675200","-109707264","-19005440","-1310720"],["0","0","0","0","0","0","1856","94464","1754368","13485568","23814144","-147032064","-259678208","578142208","318717952","-260046848","-233766912","-67239936","-8912896","-524288"],["0","0","0","0","0","0","192","12672","273152","2224640","2723840","-33656832","-24682496","139739136","17481728","-96501760","-53542912","-9830400","-524288","0"],["0","0","0","0","0","0","0","512","16384","153600","131072","-2932736","0","11730944","-2097152","-9830400","-4194304","-524288","0","0"]]},"deriv_order":2}],"step_multiplier":{"coeffs":[["0","0","0","-512","-18432","-227328","-1032192","-909312","-294912","-32768","0","0","0"],["0","0","0","-768","-26112","-285696","-866304","1732608","2285568","835584","98304","0","0"],["0","0","0","-384","-12288","-116736","-147456","1732608","-589824","-1867776","-786432","-98304","0"],["0","0","0","-64","-1920","-15360","14336","337920","-675840","-114688","491520","245760","32768"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","3072","104448","1142784","3465216","-6930432","-9142272","-3342336","-393216","0","0","0"],["0","0","0","10240","338944","3495936","8122368","-33497088","-9682944","16285696","8716288","1179648","0","0"],["0","0","0","13824","443904","4263936","6193152","-57212928","28164096","41877504","-786432","-6684672","-1179648","0"],["0","0","0","9728","302336","2674176","1130496","-46104576","58269696","22003712","-27394048","-10616832","589824","393216"],["0","0","0","3776","113408","913152","-716800","-19032064","40378368","-5742592","-24051712","-540672","3866624","720896"],["0","0","0","768","22272","161280","-356352","-3883008","12165120","-6733824","-7274496","2949120","2555904","393216"],["0","0","0","64","1792","11520","-45056","-309248","1351680","-1236992","-720896","737280","458752","65536"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-768","-29184","-390144","-2009088","-1732608","9216000","9977856","3440640","393216","0","0","0","0"],["0","0","0","-1792","-68864","-931840","-4825088","-3489792","24797184","-1343488","-19398656","-8716288","-1114112","0","0","0"],["0","0","0","-1664","-64640","-876800","-4327424","491520","38768640","-19816448","-22446080","6062080","6258688","983040","0","0"],["0","0","0","-768","-30144","-406272","-1816320","2936832","25774080","-36839424","-16932864","13369344","5849088","-196608","-196608","0"],["0","0","0","-176","-6976","-92672","-354048","1420544","7026688","-20619264","2367488","15855616","3391488","-1835008","-720896","-65536"],["0","0","0","-16","-640","-8320","-25088","200960","634880","-3436544","2539520","3215360","-1605632","-2129920","-655360","-65536"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","384","18176","325632","2650112","8736768","4399104","-2260992","-2424832","-688128","-65536","0","0","0"],["0","0","0","0","704","32000","534272","3731456","6789120","-22880256","-22454272","-65536","5488640","1900544","196608","0","0"],["0","0","0","0","480","20928","323712","1863936","-168960","-24766464","12324864","30941184","8478720","-3096576","-1671168","-196608","0"],["0","0","0","0","144","6016","85632","380416","-1097984","-7507968","17182720","4636672","-14585856","-8290304","-622592","393216","65536"],["0","0","0","0","16","640","8320","25088","-200960","-634880","3436544","-2539520","-3215360","1605632","2129920","655360","65536"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","1536","52992","604160","2256896","319488","6660096","5799936","983040","-262144","-65536","0"],["0","0","0","4352","141696","1416448","2949120","-12615680","16773120","5611520","-10027008","-4653056","-294912","65536"],["0","0","0","4736","146944","1298432","622592","-20992000","33472512","-2523136","-21757952","-2719744","2490368","524288"],["0","0","0","2496","74368","585728","-616448","-12441600","29847552","-10174464","-16941056","4308992","4882432","786432"],["0","0","0","640","18432","130560","-327680","-3207168","10813440","-6963200","-6291456","3440640","2621440","393216"],["0","0","0","64","1792","11520","-45056","-309248","1351680","-1236992","-720896","737280","458752","65536"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-384","-14208","-184064","-940032","-1507328","-2396160","-8626176","-5996544","-819200","294912","65536","0","0"],["0","0","0","-704","-26432","-342528","-1584384","161792","10508288","-7208960","2940928","10567680","3784704","131072","-65536","0"],["0","0","0","-480","-18368","-238720","-989440","2020352","13772800","-23040000","-4530176","8560640","81920","-1736704","-327680","0"],["0","0","0","-144","-5632","-73344","-265216","1196288","5308416","-17182720","4161536","13012992","917504","-2523136","-786432","-65536"],["0","0","0","-16","-640","-8320","-25088","200960","634880","-3436544","2539520","3215360","-1605632","-2129920","-655360","-65536"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","192","8704","144640","999424","1718272","-6537216","-5529600","1048576","2080768","655360","65536","0","0"],["0","0","0","0","256","11136","171520","976384","-196608","-13242368","7880704","16367616","2818048","-2785280","-1179648","-131072","0"],["0","0","0","0","112","4672","66304","291584","-873728","-5789696","13746176","2842624","-11743232","-5816320","65536","458752","65536"],["0","0","0","0","16","640","8320","25088","-200960","-634880","3436544","-2539520","-3215360","1605632","2129920","655360","65536"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["0","0","0","-512","-18432","-227328","-1032192","-909312","-294912","-32768","0","0","0"],["0","0","0","-768","-26112","-285696","-866304","1732608","2285568","835584","98304","0","0"],["0","0","0","-384","-12288","-116736","-147456","1732608","-589824","-1867776","-786432","-98304","0"],["0","0","0","-64","-1920","-15360","14336","337920","-675840","-114688","491520","245760","32768"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["0","-2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-1","-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":{"from_index":1,"justification":"the parent theorem (LiuWangDerivativeLag) proves P_(m-1) strictly interlacing P_m for every m >= 1; T = f(n, theta) = 1 + (2) theta + (1) theta^2 is independent of n and maps every real-rooted polynomial to a real-rooted polynomial or zero, so by the Hermite--Kakeya--Obreschkoff theorem (both directions) T(P_(m-1)) and T(P_m) have weakly interlacing zeros; the nonzero gauge does not move zeros, so Q_(n-1) and Q_n interlace weakly (orientation not determined) for every n >= 1","kind":"weak","orientation":"unordered","status":"claimed"},"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":{"interlacing":{"from_index":1,"justification":{"premises":["the parent theorem (LiuWangDerivativeLag) proves P_(m-1) strictly interlacing P_m for every m >= 1; T = f(n, theta) = 1 + (2) theta + (1) theta^2 is independent of n and maps every real-rooted polynomial to a real-rooted polynomial or zero, so by the Hermite--Kakeya--Obreschkoff theorem (both directions) T(P_(m-1)) and T(P_m) have weakly interlacing zeros; the nonzero gauge does not move zeros, so Q_(n-1) and Q_n interlace weakly (orientation not determined) for every n >= 1"],"theorem":"Hermite--Kakeya--Obreschkoff theorem (N. Obreschkoff, Verteilung und Berechnung der Nullstellen reeller Polynome, 1963; see S. Fisk, Polynomials, Roots, and Interlacing, arXiv:math/0612833): real polynomials f, g have weakly interlacing zeros iff alpha f + beta g is real-rooted or zero for all real alpha, beta; a linear T independent of n that maps every real-rooted polynomial to a real-rooted polynomial or zero therefore maps interlacing pairs to pairs with weakly interlacing zeros (orientation not determined)"},"kind":"weak","orientation":"unordered"},"status":"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","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","2"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"relation":"Q_n = lambda(n) T_n(P_(n+0)) with T = f(n, theta) = 1 + (2) theta + (1) theta^2, for every n >= 0"},"parent_proof":{"route":"liu_wang_derivative_lag","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_interlacing_report":{"conclusion":{"first_index":0,"interlacing":"strict","interlacing_from":1,"root_region":{"upper":{"closed":false,"value":"0"}},"simple_roots":true,"statement":"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 has simple roots and P_(n-1) strictly interlaces P_n (no common root), and deg P_n = deg P_(n-1) + 1 for n >= 2"},"hypotheses":[{"evidence":"checked exactly","name":"seed_roots_negative","statement":"P_0 and P_1 are nonzero and real-rooted with every root < 0","status":{"kind":"verified"}},{"evidence":"degrees 0 and 1, leading coefficients of one sign","name":"seed_degree_step","statement":"deg P_1 = deg P_0 + 1, with leading coefficients of one sign","status":{"kind":"verified"}},{"evidence":"Bezout test, exact","name":"seed_strict_interlacing","statement":"P_0 strictly interlaces P_1 (simple real roots, no common root)","status":{"kind":"verified"}},{"evidence":"lambda_n = 2 > 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of lambda_n = 2 at n = 2 + u have one sign)","name":"degree_step_positive","sign_decision":{"certificate":{"condition":"positive","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["2"]},"numerator":["2"],"range":{"first":"2","last":null}},"decision":"holds"},"statement":"lambda_n = [x^1] A_n + (deg P_(n-1)) [x^2] V_n > 0 for every n >= 2 (deg P_n = deg P_(n-1) + 1 with leading coefficients of one sign)","status":{"kind":"verified"}},{"evidence":"[x^0] c_1 and [x^0] c_2 are zero polynomials","name":"multipliers_vanish_at_zero","statement":"V_n(0) = 0 and W_n(0) = 0 for every n >= 2","status":{"kind":"verified"}},{"evidence":"A_n(0) = 1 > 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of A_n(0) = 1 at n = 2 + 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":"2","last":null}},"decision":"holds"},"statement":"A_n(0) > 0 for every n >= 2","status":{"kind":"verified"}},{"evidence":"V_n = 0","name":"derivative_coefficient_nonpositive","statement":"V_n(x) <= 0 for every x < 0 and every n >= 2","status":{"kind":"verified"}},{"evidence":"W_n(x) = gamma(n) w(x) / f(n) with w(x) = 2 x, which is negative on (-inf, 0) (no root there, exact): gamma(n)/f(n) = 1 >= 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of gamma(n)/f(n) = 1 at n = 2 + u have one sign)","name":"lag_coefficient_nonpositive","sign_decision":{"certificate":{"condition":"nonnegative","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1"]},"numerator":["1"],"range":{"first":"2","last":null}},"decision":"holds"},"statement":"W_n(x) <= 0 for every x < 0 and every n >= 2","status":{"kind":"verified"}},{"evidence":"W_n(x) = gamma(n) w(x) / f(n) with w(x) = 2 x, which is negative on (-inf, 0) (no root there, exact): gamma(n)/f(n) = 1 > 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of gamma(n)/f(n) = 1 at n = 2 + u have one sign)","name":"derivative_or_lag_coefficient_negative","sign_decision":{"certificate":{"condition":"positive","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1"]},"numerator":["1"],"range":{"first":"2","last":null}},"decision":"holds"},"statement":"for every n >= 2 and x < 0, V_n(x) < 0 or W_n(x) < 0 (V_n < 0 on (-inf, 0) for every n, or W_n < 0 there for every n)","status":{"kind":"verified"}}],"lean_declarations":["RealRooted.threeTerm_interlaces_of_nonnegCoeffs","RealRooted.LiuWang.strictInterl_nonpos_lag_sequence"],"lean_replay":"not_attempted","lean_route":"sign","normal_form":"P_n = A_n(x) P_(n-1) + V_n(x) P'_(n-1) + W_n(x) P_(n-2) for n >= 2, with A_n(x) = (1) + (2) x, V_n(x) = 0, W_n(x) = (2) x","recurrence":{"first_index":0,"initial_polynomials":[["1"],["1","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","2"]]},"deriv_order":0,"offset":2,"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 the interlacers f' and the lag row (strict form, as in the derivative-lag theorems of the RealRooted library, https://github.com/PerAlexandersson/RealRooted), with nonnegativity of the coefficients replaced by an exact induction keeping every root in (-inf, 0)","schema":"polytool.recurrence-real-rootedness-theorem.v1","status":"proved","theorem":"liu_wang_derivative_lag"},"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":"no theorem matched (weighted_renewal_window: support must satisfy offset = 1 + ell * t_degree; fixed_delay_predecessor_window: more than one weighted lag)","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":"P_n = A_n(x) P_(n-1) + V_n(x) P'_(n-1) + W_n(x) P_(n-2) for n >= 2, with A_n(x) = (1) + (2) x, V_n(x) = 0, W_n(x) = (2) x: every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0) (so its coefficients have one sign); for n >= 1, P_n has simple roots and P_(n-1) strictly interlaces P_n (no common root), and deg P_n = deg P_(n-1) + 1 for n >= 2","route":"liu_wang_derivative_lag","success":true,"variant":"liu_wang_derivative_lag"}],"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) + V_n(x) P'_(n-1) + W_n(x) P_(n-2) for n >= 2, with A_n(x) = (1) + (2) x, V_n(x) = 0, W_n(x) = (2) x","every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0) (so its coefficients have one sign); for n >= 1, P_n has simple roots and P_(n-1) strictly interlaces P_n (no common root), and deg P_n = deg P_(n-1) + 1 for n >= 2"],"theorem":"liu_wang_derivative_lag: 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 the interlacers f' and the lag row (strict form, as in the derivative-lag theorems of the RealRooted library, https://github.com/PerAlexandersson/RealRooted), with nonnegativity of the coefficients replaced by an exact induction keeping every root in (-inf, 0)"},"kind":"strict","orientation":"previous_interlaces_next"},"route":"liu_wang_derivative_lag","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"}