{"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":[["4","4"]]},"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,4,1) array."},"identifying_rows":2,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["-320","-3040","-10288","-15384","-10296","-2336","144"],["0","-960","-6160","-12744","-10648","-2972","132"],["0","0","-880","-3240","-3780","-1380","40"],["0","0","0","-240","-520","-276","4"],["0","0","0","0","-20","-20","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","-960","-9120","-30864","-46152","-30888","-7008","432"],["0","0","-2880","-18480","-38232","-31944","-8916","396"],["0","0","0","-2640","-9720","-11340","-4140","120"],["0","0","0","0","-720","-1560","-828","12"],["0","0","0","0","0","-60","-60","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0","-320","-3040","-10288","-15384","-10296","-2336","144"],["0","0","0","-960","-6160","-12744","-10648","-2972","132"],["0","0","0","0","-880","-3240","-3780","-1380","40"],["0","0","0","0","0","-240","-520","-276","4"],["0","0","0","0","0","0","-20","-20","0"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["-160","-1200","-3104","-3464","-1682","-255","27"],["0","-480","-2400","-3752","-2268","-412","27"],["0","0","-440","-1220","-1020","-238","9"],["0","0","0","-120","-180","-58","1"],["0","0","0","0","-10","-5","0"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-480","-3600","-9312","-10392","-5046","-765","81"],["0","0","-1440","-7200","-11256","-6804","-1236","81"],["0","0","0","-1320","-3660","-3060","-714","27"],["0","0","0","0","-360","-540","-174","3"],["0","0","0","0","0","-30","-15","0"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["0","0","-160","-1200","-3104","-3464","-1682","-255","27"],["0","0","0","-480","-2400","-3752","-2268","-412","27"],["0","0","0","0","-440","-1220","-1020","-238","9"],["0","0","0","0","0","-120","-180","-58","1"],["0","0","0","0","0","0","-10","-5","0"]]},"deriv_order":2,"shift":1},{"coeff":{"coeffs":[["80","440","812","598","134","-12"],["0","240","860","886","256","-16"],["0","0","220","410","175","-7"],["0","0","0","60","50","-1"],["0","0","0","0","5","0"]]},"deriv_order":0,"shift":2},{"coeff":{"coeffs":[["0","240","1320","2436","1794","402","-36"],["0","0","720","2580","2658","768","-48"],["0","0","0","660","1230","525","-21"],["0","0","0","0","180","150","-3"],["0","0","0","0","0","15","0"]]},"deriv_order":1,"shift":2},{"coeff":{"coeffs":[["0","0","80","440","812","598","134","-12"],["0","0","0","240","860","886","256","-16"],["0","0","0","0","220","410","175","-7"],["0","0","0","0","0","60","50","-1"],["0","0","0","0","0","0","5","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":[["80","-40","-28","-14","2","0"],["0","240","-20","-34","-4","0"],["0","0","220","50","-5","-1"],["0","0","0","60","10","-1"],["0","0","0","0","5","0"]]},"terms":[{"coeff":{"coeffs":[["320","1120","1488","936","280","24","-8"],["0","960","2640","2664","1128","124","-20"],["0","0","880","1800","1140","204","-16"],["0","0","0","240","360","116","-4"],["0","0","0","0","20","20","0"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["160","240","64","-120","-54","-1","-1"],["0","480","640","312","28","-4","-3"],["0","0","440","500","180","10","-3"],["0","0","0","120","100","18","-1"],["0","0","0","0","10","5","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":[["4","4"]]},"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","640000","7360000","37312000","110368000","211795200","276531200","249820000","155110640","64028652","16274834","2116004","59516","-8276","-622","-12"],["0","0","0","1920000","24000000","130336000","408560000","824033600","1123591200","1054824400","678146920","289306736","76112928","10393506","374858","-30902","-2618","-52"],["0","0","0","1920000","27840000","168896000","577312000","1249073600","1806142400","1783540400","1199375920","533554616","146512830","21181479","945526","-41716","-4388","-91"],["0","0","0","640000","13120000","97792000","384736000","924251200","1451856000","1535846800","1096455040","515161352","149350862","23087831","1244159","-20729","-3689","-82"],["0","0","0","0","1920000","23680000","120416000","341760000","606897600","707848000","548749200","277454240","86283576","14441424","922376","3544","-1584","-40"],["0","0","0","0","0","1760000","15280000","57704000","124268000","167721200","146396200","81941420","27951450","5145570","384400","7580","-290","-10"],["0","0","0","0","0","0","480000","3400000","10384000","17790000","18592400","12032300","4645200","959805","83214","2712","2","-1"],["0","0","0","0","0","0","0","40000","240000","606000","830000","660300","301200","71805","7215","315","5","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","1920000","22080000","111936000","331104000","635385600","829593600","749460000","465331920","192085956","48824502","6348012","178548","-24828","-1866","-36"],["0","0","0","0","5760000","72000000","391008000","1225680000","2472100800","3370773600","3164473200","2034440760","867920208","228338784","31180518","1124574","-92706","-7854","-156"],["0","0","0","0","5760000","83520000","506688000","1731936000","3747220800","5418427200","5350621200","3598127760","1600663848","439538490","63544437","2836578","-125148","-13164","-273"],["0","0","0","0","1920000","39360000","293376000","1154208000","2772753600","4355568000","4607540400","3289365120","1545484056","448052586","69263493","3732477","-62187","-11067","-246"],["0","0","0","0","0","5760000","71040000","361248000","1025280000","1820692800","2123544000","1646247600","832362720","258850728","43324272","2767128","10632","-4752","-120"],["0","0","0","0","0","0","5280000","45840000","173112000","372804000","503163600","439188600","245824260","83854350","15436710","1153200","22740","-870","-30"],["0","0","0","0","0","0","0","1440000","10200000","31152000","53370000","55777200","36096900","13935600","2879415","249642","8136","6","-3"],["0","0","0","0","0","0","0","0","120000","720000","1818000","2490000","1980900","903600","215415","21645","945","15","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","640000","7360000","37312000","110368000","211795200","276531200","249820000","155110640","64028652","16274834","2116004","59516","-8276","-622","-12"],["0","0","0","0","0","1920000","24000000","130336000","408560000","824033600","1123591200","1054824400","678146920","289306736","76112928","10393506","374858","-30902","-2618","-52"],["0","0","0","0","0","1920000","27840000","168896000","577312000","1249073600","1806142400","1783540400","1199375920","533554616","146512830","21181479","945526","-41716","-4388","-91"],["0","0","0","0","0","640000","13120000","97792000","384736000","924251200","1451856000","1535846800","1096455040","515161352","149350862","23087831","1244159","-20729","-3689","-82"],["0","0","0","0","0","0","1920000","23680000","120416000","341760000","606897600","707848000","548749200","277454240","86283576","14441424","922376","3544","-1584","-40"],["0","0","0","0","0","0","0","1760000","15280000","57704000","124268000","167721200","146396200","81941420","27951450","5145570","384400","7580","-290","-10"],["0","0","0","0","0","0","0","0","480000","3400000","10384000","17790000","18592400","12032300","4645200","959805","83214","2712","2","-1"],["0","0","0","0","0","0","0","0","0","40000","240000","606000","830000","660300","301200","71805","7215","315","5","0"]]},"deriv_order":2}],"shift":0}],"row_annihilation":{"kind":"system","system":{"generators":[{"annihilator":{"terms":[{"coeff":{"coeffs":[["-2","-1"],["4","1"],["-5","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-30","-33","-3"],["20","20","1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-20","-40","-21","-1"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["1"],["1"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","0","2240000","21280000","88800000","214256000","330358400","338774400","232327760","103845960","28185258","3899011","131864","-13134","-1066","-21"],["0","0","0","0","0","6720000","67680000","295920000","742408000","1184303200","1252551600","884545880","407224940","114225384","16570866","683415","-41331","-3883","-79"],["0","0","0","0","0","6720000","75360000","356240000","950368000","1596127200","1766574400","1301187080","624246960","182996184","28163817","1406433","-41483","-5317","-114"],["0","0","0","0","0","2240000","32800000","181200000","539336000","986866400","1173975600","922053560","469831740","146392428","24271780","1459094","-6858","-3298","-78"],["0","0","0","0","0","0","3840000","33360000","126040000","271492000","366380400","319580600","178573460","60675150","11055933","794874","12024","-832","-25"],["0","0","0","0","0","0","0","1280000","9040000","27528000","47020000","48986000","31590600","12142380","2491530","212307","6541","-19","-3"],["0","0","0","0","0","0","0","0","120000","720000","1818000","2490000","1980900","903600","215415","21645","945","15","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","-4480000","-44800000","-197344000","-506176000","-839798400","-944643200","-732416800","-388791200","-136662684","-29368064","-3114995","-21020","18530","1156","21"],["0","0","0","0","0","-8960000","-96320000","-448128000","-1199584000","-2058444800","-2376510400","-1877376000","-1007616320","-355271768","-76190506","-8229916","-157149","34389","2323","43"],["0","0","0","0","0","-4480000","-58240000","-305024000","-885120000","-1606742400","-1925195200","-1550028800","-830816240","-285194844","-57734600","-5836388","-191989","9181","793","15"],["0","0","0","0","0","0","-6720000","-55040000","-195712000","-393904000","-488816000","-379248800","-174647120","-38698520","444402","1528362","79457","-9101","-815","-17"],["0","0","0","0","0","0","0","-800000","-3520000","-2288000","15608000","45380800","58305200","41734440","16773300","3364809","225815","-209","-487","-12"],["0","0","0","0","0","0","0","0","480000","3600000","11576000","20772000","22621200","15167800","6019140","1258590","104928","2844","-36","-2"],["0","0","0","0","0","0","0","0","0","80000","480000","1212000","1660000","1320600","602400","143610","14430","630","10","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","-1920000","-19840000","-90656000","-242304000","-421129600","-499235200","-410685600","-233004160","-88239996","-20639244","-2449001","-46684","11694","800","15"],["0","0","0","0","0","0","-3840000","-43200000","-211392000","-598656000","-1094307200","-1356876800","-1162461600","-684562960","-268609312","-65288898","-8261640","-262611","26547","2105","41"],["0","0","0","0","0","0","-1920000","-26880000","-152256000","-481120000","-960137600","-1281120000","-1169033600","-727831840","-300582636","-77028024","-10548114","-484119","15787","1859","39"],["0","0","0","0","0","0","0","-3520000","-32960000","-135648000","-322912000","-491454400","-497956800","-338292640","-150822720","-41635950","-6279782","-382831","-1941","593","15"],["0","0","0","0","0","0","0","0","-1440000","-11040000","-36992000","-70880000","-85231200","-66320800","-33134800","-10147200","-1716777","-130329","-3525","29","2"],["0","0","0","0","0","0","0","0","0","-160000","-1040000","-2904000","-4532000","-4301200","-2525400","-889620","-172470","-15690","-650","-10","0"]]},"deriv_order":2}],"step_multiplier":{"coeffs":[["0","0","0","8000","48000","121200","166000","132060","60240","14361","1443","63","1"],["0","0","0","24000","144000","363600","498000","396180","180720","43083","4329","189","3"],["0","0","0","24000","144000","363600","498000","396180","180720","43083","4329","189","3"],["0","0","0","8000","48000","121200","166000","132060","60240","14361","1443","63","1"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","8000","64000","217200","408400","464060","324360","134841","30165","2949","127","2"],["0","0","0","-16000","-48000","45600","395200","731880","671880","332718","83280","8532","376","6"],["0","0","0","-96000","-528000","-1166400","-1264800","-588720","69480","189108","68850","7902","366","6"],["0","0","0","-112000","-656000","-1600800","-2081600","-1516840","-579240","-80574","8520","2004","112","2"],["0","0","0","-40000","-240000","-606000","-830000","-660300","-301200","-71805","-7215","-315","-5","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-80000","-584000","-1852000","-3331600","-3721000","-2651180","-1190850","-321603","-48111","-3715","-139","-2"],["0","0","0","0","-48000","-312000","-871200","-1359600","-1290360","-757620","-266886","-51741","-4707","-195","-3"],["0","0","0","240000","1656000","4932000","8252400","8443800","5372820","2057310","431037","40851","1731","27","0"],["0","0","0","160000","1120000","3392000","5792000","6082400","4012000","1624080","376320","44481","2723","83","1"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","-160000","-1280000","-4512000","-9184000","-11874400","-10094400","-5636080","-2000400","-420801","-47204","-2806","-84","-1"],["0","0","0","-320000","-2560000","-9024000","-18368000","-23748800","-20188800","-11272160","-4000800","-841602","-94408","-5612","-168","-2"],["0","0","0","-160000","-1280000","-4512000","-9184000","-11874400","-10094400","-5636080","-2000400","-420801","-47204","-2806","-84","-1"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","-80000","-560000","-1684000","-2824000","-2859400","-1757000","-613950","-97800","-699","803","53","1"],["0","-240000","-1720000","-5292000","-9078000","-9408200","-5931300","-2143050","-365205","-9312","2094","154","3"],["0","-240000","-1800000","-5772000","-10290000","-11068200","-7251900","-2745450","-508815","-23742","1464","144","3"],["0","-80000","-680000","-2404000","-4642000","-5349400","-3737900","-1517550","-313215","-22344","-142","38","1"],["0","0","-40000","-240000","-606000","-830000","-660300","-301200","-71805","-7215","-315","-5","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","160000","1200000","3928000","7332000","8542800","6373400","2984900","809550","99198","-907","-909","-55","-1"],["0","320000","2560000","8976000","18056000","22877600","18829200","9981800","3243180","574716","42667","905","-27","-1"],["0","160000","1520000","6168000","14116000","20126800","18538200","11008900","4057710","851838","88055","4537","111","1"],["0","0","160000","1120000","3392000","5792000","6082400","4012000","1624080","376320","44481","2723","83","1"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","-160000","-1280000","-4512000","-9184000","-11874400","-10094400","-5636080","-2000400","-420801","-47204","-2806","-84","-1"],["0","0","-320000","-2560000","-9024000","-18368000","-23748800","-20188800","-11272160","-4000800","-841602","-94408","-5612","-168","-2"],["0","0","-160000","-1280000","-4512000","-9184000","-11874400","-10094400","-5636080","-2000400","-420801","-47204","-2806","-84","-1"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["10","5","-1"],["0","5","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-20","-10","12","2"],["0","-20","-20","-1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","20","40","21","1"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","1280000","11840000","47936000","111552000","164483200","159419200","101686240","41349600","9895728","1150882","26272","-4556","-320","-6"],["0","0","0","0","3840000","37600000","159168000","384192000","584665600","583384800","383094720","160920640","40174344","5022879","164150","-14664","-1182","-23"],["0","0","0","0","3840000","41760000","190448000","486944000","777493600","810059200","554929720","243997520","64431474","8778555","382587","-15509","-1649","-34"],["0","0","0","0","1280000","18080000","95696000","271240000","469559200","524666800","383913240","180625020","51506838","7779016","432796","-3788","-1050","-24"],["0","0","0","0","0","2080000","17040000","60696000","123124000","156205200","127815000","66852340","21239190","3631278","250286","3390","-276","-8"],["0","0","0","0","0","0","560000","3800000","11116000","18238000","18253000","11314100","4186410","830625","69414","2092","-8","-1"],["0","0","0","0","0","0","0","40000","240000","606000","830000","660300","301200","71805","7215","315","5","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","-2560000","-24960000","-106688000","-263872000","-418668800","-445408000","-321731200","-155787040","-48422688","-8728820","-665994","25664","6836","356","6"],["0","0","0","0","-5120000","-53120000","-236736000","-600928000","-964137600","-1019633600","-714914400","-323053360","-86662456","-10901608","31724","105462","7842","218","2"],["0","0","0","0","-2560000","-31360000","-152768000","-404000000","-646604800","-644075200","-380995200","-102984400","15387792","19293424","4711726","292130","-6606","-1066","-24"],["0","0","0","0","0","-3200000","-22080000","-60064000","-70992000","2638400","118708000","163645520","112124200","42080352","7808144","462288","-7160","-1408","-32"],["0","0","0","0","0","0","640000","7520000","34704000","86488000","130612000","124626000","74869240","26920500","5081586","356144","3316","-516","-14"],["0","0","0","0","0","0","0","640000","4640000","14480000","25304000","26922400","17693200","6908760","1431060","120618","3494","-26","-2"],["0","0","0","0","0","0","0","0","80000","480000","1212000","1660000","1320600","602400","143610","14430","630","10","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","-1920000","-19840000","-90656000","-242304000","-421129600","-499235200","-410685600","-233004160","-88239996","-20639244","-2449001","-46684","11694","800","15"],["0","0","0","0","0","-3840000","-43200000","-211392000","-598656000","-1094307200","-1356876800","-1162461600","-684562960","-268609312","-65288898","-8261640","-262611","26547","2105","41"],["0","0","0","0","0","-1920000","-26880000","-152256000","-481120000","-960137600","-1281120000","-1169033600","-727831840","-300582636","-77028024","-10548114","-484119","15787","1859","39"],["0","0","0","0","0","0","-3520000","-32960000","-135648000","-322912000","-491454400","-497956800","-338292640","-150822720","-41635950","-6279782","-382831","-1941","593","15"],["0","0","0","0","0","0","0","-1440000","-11040000","-36992000","-70880000","-85231200","-66320800","-33134800","-10147200","-1716777","-130329","-3525","29","2"],["0","0","0","0","0","0","0","0","-160000","-1040000","-2904000","-4532000","-4301200","-2525400","-889620","-172470","-15690","-650","-10","0"]]},"deriv_order":2}],"step_multiplier":{"coeffs":[["0","0","0","8000","48000","121200","166000","132060","60240","14361","1443","63","1"],["0","0","0","24000","144000","363600","498000","396180","180720","43083","4329","189","3"],["0","0","0","24000","144000","363600","498000","396180","180720","43083","4329","189","3"],["0","0","0","8000","48000","121200","166000","132060","60240","14361","1443","63","1"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","80000","560000","1684000","2824000","2859400","1757000","613950","97800","699","-803","-53","-1"],["0","0","0","240000","1720000","5292000","9078000","9408200","5931300","2143050","365205","9312","-2094","-154","-3"],["0","0","0","240000","1800000","5772000","10290000","11068200","7251900","2745450","508815","23742","-1464","-144","-3"],["0","0","0","80000","680000","2404000","4642000","5349400","3737900","1517550","313215","22344","142","-38","-1"],["0","0","0","0","40000","240000","606000","830000","660300","301200","71805","7215","315","5","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-160000","-1200000","-3928000","-7332000","-8542800","-6373400","-2984900","-809550","-99198","907","909","55","1"],["0","0","0","-320000","-2560000","-8976000","-18056000","-22877600","-18829200","-9981800","-3243180","-574716","-42667","-905","27","1"],["0","0","0","-160000","-1520000","-6168000","-14116000","-20126800","-18538200","-11008900","-4057710","-851838","-88055","-4537","-111","-1"],["0","0","0","0","-160000","-1120000","-3392000","-5792000","-6082400","-4012000","-1624080","-376320","-44481","-2723","-83","-1"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","160000","1280000","4512000","9184000","11874400","10094400","5636080","2000400","420801","47204","2806","84","1"],["0","0","0","0","320000","2560000","9024000","18368000","23748800","20188800","11272160","4000800","841602","94408","5612","168","2"],["0","0","0","0","160000","1280000","4512000","9184000","11874400","10094400","5636080","2000400","420801","47204","2806","84","1"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","160000","1128000","3432000","5865200","6127200","3978060","1552260","330441","31563","1343","21"],["0","0","480000","3424000","10536000","18201600","19211600","12594480","4957980","1063128","101904","4344","68"],["0","0","480000","3504000","11016000","19413600","20871600","13915080","5560380","1206738","116334","4974","78"],["0","0","160000","1248000","4152000","7683200","8617200","5958960","2455860","545856","53208","2288","36"],["0","0","0","40000","240000","606000","830000","660300","301200","71805","7215","315","5"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","-320000","-2480000","-8440000","-16516000","-20417200","-16467800","-8620980","-2809950","-519999","-46297","-1897","-29","0"],["0","0","-640000","-5120000","-18000000","-36424000","-46626400","-39018000","-21253960","-7243980","-1416318","-137075","-6517","-141","-1"],["0","0","-320000","-2800000","-10680000","-23300000","-32001200","-28632600","-16644980","-6058110","-1272639","-135259","-7343","-195","-2"],["0","0","0","-160000","-1120000","-3392000","-5792000","-6082400","-4012000","-1624080","-376320","-44481","-2723","-83","-1"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","160000","1280000","4512000","9184000","11874400","10094400","5636080","2000400","420801","47204","2806","84","1"],["0","0","0","320000","2560000","9024000","18368000","23748800","20188800","11272160","4000800","841602","94408","5612","168","2"],["0","0","0","160000","1280000","4512000","9184000","11874400","10094400","5636080","2000400","420801","47204","2806","84","1"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["0","0","0","8000","48000","121200","166000","132060","60240","14361","1443","63","1"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-4","-4"]]},"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":[["4","4"]]},"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) = (4) + (4) x; open hypotheses: multipliers_vanish_at_zero: [x^0] c_2(n, x) = 4 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 = 4 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 = 4 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) = (4) + (4) 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) = (4) + (4) 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"}