{"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"],["4","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","4"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["4","4"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"basis_map_A013609 of Triangle T(n, k) is coefficient of z^n*w^k in 1/(1 - 2*z - 2*w - 2*z*w) read by rows in order 00, 10, 01, 20, 11, 02, ..."},"identifying_rows":2,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["-6","-114","-766","-2204","-2624","-640","576"],["0","-36","-462","-1878","-2948","-1240","528"],["0","0","-66","-486","-1106","-716","160"],["0","0","0","-36","-156","-160","16"],["0","0","0","0","-6","-12","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","-18","-342","-2298","-6612","-7872","-1920","1728"],["0","0","-108","-1386","-5634","-8844","-3720","1584"],["0","0","0","-198","-1458","-3318","-2148","480"],["0","0","0","0","-108","-468","-480","48"],["0","0","0","0","0","-18","-36","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0","-6","-114","-766","-2204","-2624","-640","576"],["0","0","0","-36","-462","-1878","-2948","-1240","528"],["0","0","0","0","-66","-486","-1106","-716","160"],["0","0","0","0","0","-36","-156","-160","16"],["0","0","0","0","0","0","-6","-12","0"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["-12","-180","-920","-1916","-1436","144","432"],["0","-72","-720","-2184","-2352","-384","432"],["0","0","-132","-732","-1168","-420","144"],["0","0","0","-72","-216","-128","16"],["0","0","0","0","-12","-12","0"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-36","-540","-2760","-5748","-4308","432","1296"],["0","0","-216","-2160","-6552","-7056","-1152","1296"],["0","0","0","-396","-2196","-3504","-1260","432"],["0","0","0","0","-216","-648","-384","48"],["0","0","0","0","0","-36","-36","0"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["0","0","-12","-180","-920","-1916","-1436","144","432"],["0","0","0","-72","-720","-2184","-2352","-384","432"],["0","0","0","0","-132","-732","-1168","-420","144"],["0","0","0","0","0","-72","-216","-128","16"],["0","0","0","0","0","0","-12","-12","0"]]},"deriv_order":2,"shift":1},{"coeff":{"coeffs":[["3","33","119","150","16","-48"],["0","18","129","249","92","-64"],["0","0","33","123","91","-28"],["0","0","0","18","30","-4"],["0","0","0","0","3","0"]]},"deriv_order":0,"shift":2},{"coeff":{"coeffs":[["0","9","99","357","450","48","-144"],["0","0","54","387","747","276","-192"],["0","0","0","99","369","273","-84"],["0","0","0","0","54","90","-12"],["0","0","0","0","0","9","0"]]},"deriv_order":1,"shift":2},{"coeff":{"coeffs":[["0","0","3","33","119","150","16","-48"],["0","0","0","18","129","249","92","-64"],["0","0","0","0","33","123","91","-28"],["0","0","0","0","0","18","30","-4"],["0","0","0","0","0","0","3","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"],["4","16"]],"recurrence":{"denominator":{"coeffs":[["3","-3","-7","0","4","0"],["0","18","-3","-27","-8","0"],["0","0","33","15","-17","-4"],["0","0","0","18","6","-4"],["0","0","0","0","3","0"]]},"terms":[{"coeff":{"coeffs":[["6","42","106","104","0","-64","-32"],["0","36","198","366","204","-88","-80"],["0","0","66","270","314","44","-64"],["0","0","0","36","108","64","-16"],["0","0","0","0","6","12","0"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["12","36","8","-100","-132","-64","-16"],["0","72","192","120","-112","-144","-48"],["0","0","132","300","160","-60","-48"],["0","0","0","72","120","32","-16"],["0","0","0","0","12","12","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"],["4","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","4"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["4","4"]]},"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","81","1863","18927","112428","434646","1149012","2116572","2701200","2296456","1149024","161984","-176896","-120192","-31232","-3072"],["0","0","0","243","6075","66096","415935","1690524","4675050","8988588","11991636","10760112","5905560","1312816","-528608","-470208","-130816","-13312"],["0","0","0","243","7047","85617","587250","2561247","7526088","15293682","21553380","20587812","12418464","3704408","-366992","-702432","-218048","-23296"],["0","0","0","81","3321","49545","390906","1893699","6057828","13251642","20017596","20584420","13695888","5077304","373968","-478368","-182336","-20992"],["0","0","0","0","486","11988","122148","699246","2533248","6135156","10145448","11406696","8426496","3724624","700000","-117696","-78208","-10240"],["0","0","0","0","0","891","15471","117720","517158","1451628","2715228","3415584","2834904","1463552","400576","21888","-14720","-2560"],["0","0","0","0","0","0","486","6885","42660","151470","339012","495180","471744","283416","98608","15648","-192","-256"],["0","0","0","0","0","0","0","81","972","5022","14580","26028","29376","20760","8784","2016","192","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","243","5589","56781","337284","1303938","3447036","6349716","8103600","6889368","3447072","485952","-530688","-360576","-93696","-9216"],["0","0","0","0","729","18225","198288","1247805","5071572","14025150","26965764","35974908","32280336","17716680","3938448","-1585824","-1410624","-392448","-39936"],["0","0","0","0","729","21141","256851","1761750","7683741","22578264","45881046","64660140","61763436","37255392","11113224","-1100976","-2107296","-654144","-69888"],["0","0","0","0","243","9963","148635","1172718","5681097","18173484","39754926","60052788","61753260","41087664","15231912","1121904","-1435104","-547008","-62976"],["0","0","0","0","0","1458","35964","366444","2097738","7599744","18405468","30436344","34220088","25279488","11173872","2100000","-353088","-234624","-30720"],["0","0","0","0","0","0","2673","46413","353160","1551474","4354884","8145684","10246752","8504712","4390656","1201728","65664","-44160","-7680"],["0","0","0","0","0","0","0","1458","20655","127980","454410","1017036","1485540","1415232","850248","295824","46944","-576","-768"],["0","0","0","0","0","0","0","0","243","2916","15066","43740","78084","88128","62280","26352","6048","576","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","81","1863","18927","112428","434646","1149012","2116572","2701200","2296456","1149024","161984","-176896","-120192","-31232","-3072"],["0","0","0","0","0","243","6075","66096","415935","1690524","4675050","8988588","11991636","10760112","5905560","1312816","-528608","-470208","-130816","-13312"],["0","0","0","0","0","243","7047","85617","587250","2561247","7526088","15293682","21553380","20587812","12418464","3704408","-366992","-702432","-218048","-23296"],["0","0","0","0","0","81","3321","49545","390906","1893699","6057828","13251642","20017596","20584420","13695888","5077304","373968","-478368","-182336","-20992"],["0","0","0","0","0","0","486","11988","122148","699246","2533248","6135156","10145448","11406696","8426496","3724624","700000","-117696","-78208","-10240"],["0","0","0","0","0","0","0","891","15471","117720","517158","1451628","2715228","3415584","2834904","1463552","400576","21888","-14720","-2560"],["0","0","0","0","0","0","0","0","486","6885","42660","151470","339012","495180","471744","283416","98608","15648","-192","-256"],["0","0","0","0","0","0","0","0","0","81","972","5022","14580","26028","29376","20760","8784","2016","192","0"]]},"deriv_order":2}],"shift":0}],"row_annihilation":{"kind":"system","system":{"generators":[{"annihilator":{"terms":[{"coeff":{"coeffs":[["-4","-4"],["1","4"],["-3","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-9","-24","-12"],["6","12","4"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-3","-12","-14","-4"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["1"],["1"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","0","2268","43092","358884","1731240","5365656","11159424","15706320","14552736","8013472","1559744","-987648","-778240","-212480","-21504"],["0","0","0","0","0","6804","137052","1196208","6007608","19319040","41662512","60976224","59338656","35499072","9530112","-2235776","-2602752","-769536","-80896"],["0","0","0","0","0","6804","152604","1440504","7705692","26180496","59450760","91734192","94949136","62266176","21400032","-106176","-3065472","-1046784","-116736"],["0","0","0","0","0","2268","66420","733104","4384800","16295472","40031712","66583392","74655168","54291328","22865984","3325056","-1338112","-645632","-79872"],["0","0","0","0","0","0","7776","135108","1027728","4509000","12624336","23512464","29366208","24065568","12102720","3069184","24576","-164352","-25600"],["0","0","0","0","0","0","0","5184","73224","452304","1600560","3568320","5186592","4907328","2915520","991488","145920","-6144","-3072"],["0","0","0","0","0","0","0","0","972","11664","60264","174960","312336","352512","249120","105408","24192","2304","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","-2268","-45360","-400680","-2071332","-6976368","-16075368","-25785744","-28514640","-20642560","-8132256","143680","1990144","1030656","237056","21504"],["0","0","0","0","0","-4536","-97524","-909576","-4909572","-17141760","-40771944","-67428912","-77203536","-58966400","-26685792","-3632960","3140608","1992192","479744","44032"],["0","0","0","0","0","-2268","-58968","-618732","-3623292","-13433256","-33459912","-57454368","-68159856","-54628960","-27735456","-7300032","109312","671232","176640","15360"],["0","0","0","0","0","0","-6804","-111456","-801252","-3318840","-8731368","-15144192","-17380080","-12921888","-6076896","-2066432","-923776","-487680","-148480","-17408"],["0","0","0","0","0","0","0","-1620","-14256","-22464","213840","1327968","3595104","5598528","5205696","2683072","506496","-157440","-91648","-12288"],["0","0","0","0","0","0","0","0","1944","29160","189648","701136","1620864","2423520","2335680","1392192","459392","56064","-7680","-2048"],["0","0","0","0","0","0","0","0","0","648","7776","40176","116640","208224","235008","166080","70272","16128","1536","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","-972","-20088","-184032","-990252","-3484512","-8422488","-14239440","-16708080","-13004736","-5774816","-384064","1135104","664064","162304","15360"],["0","0","0","0","0","0","-1944","-43740","-428976","-2445876","-9062928","-22993416","-40801680","-50509008","-42225216","-21579360","-4279872","1984768","1597440","425472","41984"],["0","0","0","0","0","0","-972","-27216","-308772","-1964412","-7958736","-21820104","-41609232","-55421136","-50540736","-29676960","-9242880","77184","1163520","374784","39936"],["0","0","0","0","0","0","0","-3564","-66744","-552852","-2675160","-8397864","-17928000","-26472432","-26868000","-18116192","-7418752","-1345920","173312","120832","15360"],["0","0","0","0","0","0","0","0","-2916","-44712","-303264","-1196640","-3037824","-5177088","-5990976","-4644864","-2308032","-659840","-74496","7680","2048"],["0","0","0","0","0","0","0","0","0","-648","-8424","-47952","-156816","-324864","-443232","-401088","-236352","-86400","-17664","-1536","0"]]},"deriv_order":2}],"step_multiplier":{"coeffs":[["0","0","0","27","324","1674","4860","8676","9792","6920","2928","672","64"],["0","0","0","81","972","5022","14580","26028","29376","20760","8784","2016","192"],["0","0","0","81","972","5022","14580","26028","29376","20760","8784","2016","192"],["0","0","0","27","324","1674","4860","8676","9792","6920","2928","672","64"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","54","864","5940","23112","56232","88992","92176","61216","24768","5504","512"],["0","0","0","81","1620","12798","54756","142668","237600","255768","174864","72288","16320","1536"],["0","0","0","-81","-324","2754","25596","90612","178848","214248","157296","68256","15936","1536"],["0","0","0","-189","-2052","-9126","-20628","-21852","864","29896","34864","18720","4928","512"],["0","0","0","-81","-972","-5022","-14580","-26028","-29376","-20760","-8784","-2016","-192","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-81","-1296","-9126","-37260","-97740","-172368","-207672","-170160","-92512","-31680","-6144","-512"],["0","0","0","0","-324","-4212","-23976","-78408","-162432","-221616","-200544","-118176","-43200","-8832","-768"],["0","0","0","243","3240","18954","63828","136404","192240","179784","109392","41184","8640","768","0"],["0","0","0","162","2268","14040","50544","117072","182304","193728","139776","66848","20160","3456","256"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","-81","-1296","-9288","-39312","-109080","-208224","-279168","-263616","-173200","-76928","-21888","-3584","-256"],["0","0","0","-162","-2592","-18576","-78624","-218160","-416448","-558336","-527232","-346400","-153856","-43776","-7168","-512"],["0","0","0","-81","-1296","-9288","-39312","-109080","-208224","-279168","-263616","-173200","-76928","-21888","-3584","-256"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","-81","-1134","-6858","-23328","-48492","-61992","-44808","-11136","8096","7488","2304","256"],["0","-243","-3483","-21546","-75006","-160056","-212004","-163800","-54168","15504","20448","6720","768"],["0","-243","-3645","-23490","-85050","-189216","-264060","-222552","-95688","-2064","16416","6336","768"],["0","-81","-1377","-9774","-38394","-92232","-140076","-132936","-73416","-18256","1440","1728","256"],["0","0","-81","-972","-5022","-14580","-26028","-29376","-20760","-8784","-2016","-192","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","81","1215","7992","30186","71820","110484","106800","55944","3040","-15584","-9792","-2560","-256"],["0","162","2592","18252","74412","194184","338040","395904","305616","145856","35680","576","-1664","-256"],["0","81","1539","12528","58266","172908","344628","471408","443400","282592","118112","30528","4352","256"],["0","0","162","2268","14040","50544","117072","182304","193728","139776","66848","20160","3456","256"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","-81","-1296","-9288","-39312","-109080","-208224","-279168","-263616","-173200","-76928","-21888","-3584","-256"],["0","0","-162","-2592","-18576","-78624","-218160","-416448","-558336","-527232","-346400","-153856","-43776","-7168","-512"],["0","0","-81","-1296","-9288","-39312","-109080","-208224","-279168","-263616","-173200","-76928","-21888","-3584","-256"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["3","3","-4"],["0","3","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-3","-3","10","8"],["0","-6","-12","-4"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","3","12","14","4"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","1296","23976","193536","899640","2667168","5256144","6919008","5872800","2821376","307648","-460416","-279296","-67072","-6144"],["0","0","0","0","3888","76140","642816","3104244","9531216","19456632","26656848","23892720","12743808","2588832","-1177792","-939648","-244992","-23552"],["0","0","0","0","3888","84564","769500","3944700","12761928","27396792","39625056","38019024","22685664","6674208","-544064","-1120128","-337152","-34816"],["0","0","0","0","1296","36612","386964","2205360","7774056","18032112","28182480","29532864","19925408","7649152","865536","-507392","-211456","-24576"],["0","0","0","0","0","4212","69012","495720","2055240","5439744","9580464","11319648","8779680","4175808","989312","-8448","-55296","-8192"],["0","0","0","0","0","0","2268","30780","182952","624024","1343520","1890000","1735008","1002720","332224","47232","-2304","-1024"],["0","0","0","0","0","0","0","324","3888","20088","58320","104112","117504","83040","35136","8064","768","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","-1296","-25272","-216648","-1081080","-3491856","-7652880","-11546304","-11806560","-7637824","-2357440","527744","855040","366592","74752","6144"],["0","0","0","0","-2592","-53784","-480600","-2463696","-8078832","-17778528","-26627232","-26694528","-16741184","-5106432","646912","1155840","394752","54272","2048"],["0","0","0","0","-1296","-31752","-309960","-1658880","-5474520","-11639808","-15845136","-12738720","-4088224","1941504","1942848","32128","-492288","-198144","-24576"],["0","0","0","0","0","-3240","-44712","-248400","-643680","-333504","2783808","9092352","13946112","12039296","5352320","422144","-660992","-269312","-32768"],["0","0","0","0","0","0","1296","30456","280800","1410480","4365792","8772192","11589504","9850560","4991104","1166336","-82944","-99328","-14336"],["0","0","0","0","0","0","0","2592","37584","237600","857952","1945728","2866752","2736768","1628544","545792","73728","-6144","-2048"],["0","0","0","0","0","0","0","0","648","7776","40176","116640","208224","235008","166080","70272","16128","1536","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","-972","-20088","-184032","-990252","-3484512","-8422488","-14239440","-16708080","-13004736","-5774816","-384064","1135104","664064","162304","15360"],["0","0","0","0","0","-1944","-43740","-428976","-2445876","-9062928","-22993416","-40801680","-50509008","-42225216","-21579360","-4279872","1984768","1597440","425472","41984"],["0","0","0","0","0","-972","-27216","-308772","-1964412","-7958736","-21820104","-41609232","-55421136","-50540736","-29676960","-9242880","77184","1163520","374784","39936"],["0","0","0","0","0","0","-3564","-66744","-552852","-2675160","-8397864","-17928000","-26472432","-26868000","-18116192","-7418752","-1345920","173312","120832","15360"],["0","0","0","0","0","0","0","-2916","-44712","-303264","-1196640","-3037824","-5177088","-5990976","-4644864","-2308032","-659840","-74496","7680","2048"],["0","0","0","0","0","0","0","0","-648","-8424","-47952","-156816","-324864","-443232","-401088","-236352","-86400","-17664","-1536","0"]]},"deriv_order":2}],"step_multiplier":{"coeffs":[["0","0","0","27","324","1674","4860","8676","9792","6920","2928","672","64"],["0","0","0","81","972","5022","14580","26028","29376","20760","8784","2016","192"],["0","0","0","81","972","5022","14580","26028","29376","20760","8784","2016","192"],["0","0","0","27","324","1674","4860","8676","9792","6920","2928","672","64"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","81","1134","6858","23328","48492","61992","44808","11136","-8096","-7488","-2304","-256"],["0","0","0","243","3483","21546","75006","160056","212004","163800","54168","-15504","-20448","-6720","-768"],["0","0","0","243","3645","23490","85050","189216","264060","222552","95688","2064","-16416","-6336","-768"],["0","0","0","81","1377","9774","38394","92232","140076","132936","73416","18256","-1440","-1728","-256"],["0","0","0","0","81","972","5022","14580","26028","29376","20760","8784","2016","192","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-81","-1215","-7992","-30186","-71820","-110484","-106800","-55944","-3040","15584","9792","2560","256"],["0","0","0","-162","-2592","-18252","-74412","-194184","-338040","-395904","-305616","-145856","-35680","-576","1664","256"],["0","0","0","-81","-1539","-12528","-58266","-172908","-344628","-471408","-443400","-282592","-118112","-30528","-4352","-256"],["0","0","0","0","-162","-2268","-14040","-50544","-117072","-182304","-193728","-139776","-66848","-20160","-3456","-256"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","81","1296","9288","39312","109080","208224","279168","263616","173200","76928","21888","3584","256"],["0","0","0","0","162","2592","18576","78624","218160","416448","558336","527232","346400","153856","43776","7168","512"],["0","0","0","0","81","1296","9288","39312","109080","208224","279168","263616","173200","76928","21888","3584","256"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","162","2322","14580","52596","120096","180216","178608","114448","45024","9792","896"],["0","0","486","7047","44712","162810","374868","566676","565200","364104","143856","31392","2880"],["0","0","486","7209","46656","172854","404028","618732","623952","405624","161424","35424","3264"],["0","0","162","2565","17496","67662","163836","258300","266736","176728","71376","15840","1472"],["0","0","0","81","972","5022","14580","26028","29376","20760","8784","2016","192"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","-162","-2511","-17280","-69498","-180900","-318708","-385968","-319560","-176240","-61344","-12096","-1024","0"],["0","0","-324","-5184","-36828","-153036","-412344","-754488","-954240","-832848","-492256","-189536","-44352","-5504","-256"],["0","0","-162","-2835","-21816","-97578","-281988","-552852","-750576","-707016","-455792","-195040","-52416","-7936","-512"],["0","0","0","-162","-2268","-14040","-50544","-117072","-182304","-193728","-139776","-66848","-20160","-3456","-256"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","81","1296","9288","39312","109080","208224","279168","263616","173200","76928","21888","3584","256"],["0","0","0","162","2592","18576","78624","218160","416448","558336","527232","346400","153856","43776","7168","512"],["0","0","0","81","1296","9288","39312","109080","208224","279168","263616","173200","76928","21888","3584","256"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["0","0","0","27","324","1674","4860","8676","9792","6920","2928","672","64"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-2","-4"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-4","-4"]]},"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"],["4","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","4"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["4","4"]]},"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) = (4) + (4) x, V_n(x) = 0, W_n(x) = (2) + (4) x; open hypotheses: multipliers_vanish_at_zero: [x^0] c_2(n, x) = 2 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 = 2 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 = 2 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) = (4) + (4) x, B_n(x) = (2) + (4) x: every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, -1/2] (so its coefficients have one sign); for n >= 1, P_(n-1) interlaces P_n (weakly, in the sense of Liu and Wang), and deg P_n - deg P_(n-1) is 0 or 1 for n >= 2","route":"liu_wang_three_term","success":true,"variant":"liu_wang_three_term"}],"conditional_on":[],"interlacing":{"from_index":1,"justification":{"premises":["every hypothesis of the theorem is verified exactly for every index: P_n = A_n(x) P_(n-1) + B_n(x) P_(n-2) for n >= 2, with A_n(x) = (4) + (4) x, B_n(x) = (2) + (4) x","every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, -1/2] (so its coefficients have one sign); for n >= 1, P_(n-1) interlaces P_n (weakly, in the sense of Liu and Wang), and deg P_n - deg P_(n-1) is 0 or 1 for n >= 2"],"theorem":"liu_wang_three_term: L. L. Liu and Y. Wang, Adv. Appl. Math. 38 (2007) 542-560, Theorem 2.1 and Corollary 2.4 (A unified approach to polynomial sequences with only real zeros; the lag row as the interlacer, b_n = 0), weak interlacing of consecutive rows, with nonnegativity of the coefficients replaced, where a root region is certified, by an exact root-location induction"},"kind":"weak","orientation":"previous_interlaces_next"},"route":"liu_wang_three_term","rows_checked":10,"statement":"every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign","status":"proved"},"rows_compared":16,"schema":"polytool.recurrence-preserver-image.v1","statement":"proved: Q_n = lambda(n) T_n(P_(n+0)) with T = f(n, theta) = 1 + (2) theta + (1) theta^2 for every n >= 0, the side conditions hold for every n, and every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign; so every Q_n, n >= 0, is zero or real-rooted with roots in (-inf, 0]"},"kind":"preserver_image"}