{"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"],["3"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-1","1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"Triangle of coefficients of polynomials v(n,x) jointly generated with A208508; see the Formula section."},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["24","-72","72","-24","0"],["16","-8","180","32","-36"],["0","-108","-68","60","-60"],["0","-40","-18","49","-37"],["0","0","22","20","-10"],["0","0","4","3","-1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","200","-888","1464","-1064","288"],["0","48","-1048","2700","-1520","372"],["0","0","-644","900","-900","116"],["0","0","-120","202","-189","-31"],["0","0","0","98","20","-22"],["0","0","0","12","9","-3"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0","184","-912","1632","-1264","360"],["0","0","16","-1288","2880","-1988","564"],["0","0","0","-508","1312","-1290","310"],["0","0","0","-40","302","-371","63"],["0","0","0","0","62","-30","0"],["0","0","0","0","4","3","-1"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["0","0","0","32","-168","312","-248","72"],["0","0","0","0","-256","540","-404","120"],["0","0","0","0","-80","276","-270","74"],["0","0","0","0","0","64","-84","20"],["0","0","0","0","0","8","-10","2"]]},"deriv_order":3,"shift":0},{"coeff":{"coeffs":[["-8","24","-24","8"],["-16","24","-84","28"],["0","68","-72","38"],["0","40","-38","25"],["0","0","-18","8"],["0","0","-4","1"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-24","72","-72","24"],["0","-48","72","-252","84"],["0","0","204","-216","114"],["0","0","120","-114","75"],["0","0","0","-54","24"],["0","0","0","-12","3"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["0","0","-8","24","-24","8"],["0","0","-16","24","-84","28"],["0","0","0","68","-72","38"],["0","0","0","40","-38","25"],["0","0","0","0","-18","8"],["0","0","0","0","-4","1"]]},"deriv_order":2,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"denominator":{"coeffs":[["8","28","12","0"],["-16","8","-2","0"],["0","-52","-26","1"],["0","40","-6","3"],["0","0","2","3"],["0","0","-4","1"]]},"terms":[{"coeff":{"coeffs":[["-8","132","140","28","-4"],["-16","-88","-194","6","-8"],["0","-12","-78","-3","-1"],["0","40","66","1","7"],["0","0","-2","-5","5"],["0","0","-4","-3","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","-32","-8","8","40","-8"],["0","0","96","-148","76","-24"],["0","0","80","-132","78","-26"],["0","0","0","-32","44","-12"],["0","0","0","-8","10","-2"]]},"deriv_order":1,"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"],["3"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-1","1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_leader_shift":2,"parent_valid_from_base":0,"quotients":[],"row_annihilation":{"kind":"system","system":{"generators":[{"annihilator":{"terms":[{"coeff":{"coeffs":[["-36","0","0"],["32","-12","1"],["-16","8","-1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["96","-192","66","-6"],["0","64","-32","4"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","64","-96","36","-4"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["12"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","-589824","5308416","-21233664","49545216","-74317824","74317824","-49545216","21233664","-5308416","589824"],["0","0","0","-4718592","38043648","-140673024","312311808","-455639040","448561152","-294617088","122978304","-29196288","2949120"],["0","0","0","-14155776","105873408","-381763584","850378752","-1246445568","1210761216","-764264448","299188224","-65912832","6340608"],["0","0","0","-18874368","149815296","-587169792","1371193344","-2002305024","1861779456","-1101201408","403292160","-84197376","7667712"],["0","0","0","-9437184","127401984","-599408640","1427668992","-1991208960","1739501568","-973725696","341286912","-67792896","5713920"],["0","0","0","0","75497472","-394002432","905674752","-1208696832","1026828288","-563152896","190457856","-35297280","2691072"],["0","0","0","0","23592960","-128581632","315555840","-449961984","397670400","-216308736","68797440","-11547648","783360"],["0","0","0","0","0","-14155776","61341696","-107937792","99090432","-50853888","14542848","-2156544","129024"],["0","0","0","0","0","-2359296","9437184","-15040512","12238848","-5465088","1354752","-175104","9216"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","-1769472","15925248","-63700992","148635648","-222953472","222953472","-148635648","63700992","-15925248","1769472"],["0","0","0","0","-14155776","114130944","-422019072","936935424","-1366917120","1345683456","-883851264","368934912","-87588864","8847360"],["0","0","0","0","-42467328","317620224","-1145290752","2551136256","-3739336704","3632283648","-2292793344","897564672","-197738496","19021824"],["0","0","0","0","-56623104","449445888","-1761509376","4113580032","-6006915072","5585338368","-3303604224","1209876480","-252592128","23003136"],["0","0","0","0","-28311552","382205952","-1798225920","4283006976","-5973626880","5218504704","-2921177088","1023860736","-203378688","17141760"],["0","0","0","0","0","226492416","-1182007296","2717024256","-3626090496","3080484864","-1689458688","571373568","-105891840","8073216"],["0","0","0","0","0","70778880","-385744896","946667520","-1349885952","1193011200","-648926208","206392320","-34642944","2350080"],["0","0","0","0","0","0","-42467328","184025088","-323813376","297271296","-152561664","43628544","-6469632","387072"],["0","0","0","0","0","0","-7077888","28311552","-45121536","36716544","-16395264","4064256","-525312","27648"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","-589824","5308416","-21233664","49545216","-74317824","74317824","-49545216","21233664","-5308416","589824"],["0","0","0","0","0","-4718592","38043648","-140673024","312311808","-455639040","448561152","-294617088","122978304","-29196288","2949120"],["0","0","0","0","0","-14155776","105873408","-381763584","850378752","-1246445568","1210761216","-764264448","299188224","-65912832","6340608"],["0","0","0","0","0","-18874368","149815296","-587169792","1371193344","-2002305024","1861779456","-1101201408","403292160","-84197376","7667712"],["0","0","0","0","0","-9437184","127401984","-599408640","1427668992","-1991208960","1739501568","-973725696","341286912","-67792896","5713920"],["0","0","0","0","0","0","75497472","-394002432","905674752","-1208696832","1026828288","-563152896","190457856","-35297280","2691072"],["0","0","0","0","0","0","23592960","-128581632","315555840","-449961984","397670400","-216308736","68797440","-11547648","783360"],["0","0","0","0","0","0","0","-14155776","61341696","-107937792","99090432","-50853888","14542848","-2156544","129024"],["0","0","0","0","0","0","0","-2359296","9437184","-15040512","12238848","-5465088","1354752","-175104","9216"]]},"deriv_order":2}],"step_multiplier":{"coeffs":[["0","0","0","884736","-5308416","13271040","-17694720","13271040","-5308416","884736"],["0","0","0","5308416","-27869184","59719680","-66355200","39813120","-11943936","1327104"],["0","0","0","10616832","-47775744","85598208","-76972032","35831808","-7962624","663552"],["0","0","0","7077888","-26542080","38486016","-27095040","9621504","-1658880","110592"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","294912","-2064384","6193152","-10321920","10321920","-6193152","2064384","-294912","0"],["0","0","0","1769472","-10764288","27353088","-37158912","28385280","-11354112","1548288","294912","-73728"],["0","0","0","2359296","-10027008","13418496","921600","-20090880","21602304","-10248192","2248704","-184320"],["0","0","0","-4718592","33030144","-93782016","141262848","-122849280","62595072","-18100224","2727936","-165888"],["0","0","0","-14155776","73138176","-156303360","178716672","-118462464","46384128","-10533888","1281024","-64512"],["0","0","0","-9437184","40108032","-69599232","63995904","-34099200","10884096","-2055168","211968","-9216"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","7077888","-51904512","165298176","-298303488","333398016","-236371968","104251392","-26689536","3391488","-147456"],["0","0","0","42467328","-274857984","759398400","-1162469376","1068613632","-595795968","192282624","-31334400","1622016","73728"],["0","0","0","84934656","-467140608","1061683200","-1271365632","835743744","-269070336","12607488","16588800","-4313088","331776"],["0","0","0","56623104","-231211008","327942144","-116195328","-175251456","225810432","-113319936","29233152","-3833856","202752"],["0","0","0","0","37748736","-160432128","278396928","-255983616","136396800","-43536384","8220672","-847872","36864"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","4718592","-35389440","115900416","-216760320","253919232","-191987712","92897280","-27426816","4423680","-294912"],["0","0","0","0","28311552","-191102976","557383680","-917028864","931627008","-601178112","244187136","-59719680","7962624","-442368"],["0","0","0","0","56623104","-339738624","870580224","-1242169344","1079599104","-588570624","200392704","-41140224","4644864","-221184"],["0","0","0","0","37748736","-198180864","438829056","-534380544","392380416","-179933184","51757056","-9068544","884736","-36864"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","18874368","-113246208","290193408","-414056448","359866368","-196190208","66797568","-13713408","1548288","-73728"],["0","0","0","75497472","-410517504","937820160","-1165197312","850894848","-367718400","89358336","-10395648","221184","36864"],["0","0","0","84934656","-410517504","810418176","-835190784","473665536","-139290624","14155776","2543616","-774144","55296"],["0","0","0","37748736","-169869312","318504960","-325582848","200392704","-77635584","19104768","-2903040","248832","-9216"],["0","0","0","37748736","-169869312","318504960","-325582848","200392704","-77635584","19104768","-2903040","248832","-9216"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-56623104","377487360","-1111228416","1903951872","-2105008128","1569521664","-797368320","270729216","-58171392","7077888","-368640"],["0","0","0","-226492416","1358954496","-3538944000","5251792896","-4905861120","3008987136","-1226465280","328237056","-55296000","5308416","-221184"],["0","0","0","-226492416","1132462080","-2335703040","2548039680","-1552711680","491028480","-40642560","-23224320","8294400","-1105920","55296"],["0","0","0","0","-150994944","679477248","-1274019840","1302331392","-801570816","310542336","-76419072","11612160","-995328","36864"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","-37748736","264241152","-806879232","1408499712","-1547845632","1112113152","-525975552","161021952","-30523392","3244032","-147456"],["0","0","0","0","-150994944","943718400","-2548039680","3892838400","-3707043840","2289254400","-926760960","243302400","-39813120","3686400","-147456"],["0","0","0","0","-150994944","830472192","-1953497088","2576351232","-2103902208","1112113152","-386961408","88031232","-12607488","1032192","-36864"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0"],["-2","-2"],["6","1"],["-4","1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["12","-24","12"],["24","-34","-2"],["0","16","-4"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","8","-16","8"],["0","16","-20","4"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","4718592","-33030144","92897280","-131825664","96436224","-39813120","34504704","-48660480","34504704","-10911744","1179648"],["0","0","0","28311552","-191102976","509607936","-720617472","687882240","-669745152","705134592","-541900800","243744768","-56623104","5308416"],["0","0","0","56623104","-408158208","1179648000","-2027667456","2690924544","-3052044288","2663202816","-1564213248","566525952","-114868224","10027008"],["0","0","0","37748736","-419954688","1646788608","-3644522496","5393793024","-5634035712","4141264896","-2082779136","678776832","-127401984","10321920"],["0","0","0","0","-254803968","1445068800","-3578462208","5186838528","-4989726720","3374069760","-1593501696","489498624","-85248000","6266880"],["0","0","0","0","-94371840","582746112","-1545338880","2372419584","-2385764352","1644466176","-760430592","218456064","-34430976","2248704"],["0","0","0","0","0","51904512","-264241152","571539456","-683311104","490936320","-215156736","55609344","-7723008","442368"],["0","0","0","0","0","9437184","-47185920","97910784","-109117440","70815744","-27279360","6119424","-737280","36864"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","14155776","-115605504","414941184","-858193920","1127153664","-978518016","569769984","-224722944","61931520","-12386304","1474560"],["0","0","0","0","84934656","-622854144","2102132736","-4264427520","5702565888","-5213749248","3295199232","-1431502848","416268288","-75202560","6635520"],["0","0","0","0","169869312","-1224474624","4305715200","-9316712448","13213458432","-12544303104","8014823424","-3425107968","955441152","-161243136","12533760"],["0","0","0","0","113246208","-1193803776","5212864512","-12355928064","17787396096","-16492253184","10160381952","-4196081664","1132683264","-181407744","12902400"],["0","0","0","0","0","-764411904","4137025536","-9863626752","13705371648","-12322713600","7466471424","-3044284416","798861312","-120526848","7833600"],["0","0","0","0","0","-283115520","1583087616","-3954769920","5800181760","-5473456128","3405514752","-1376492544","344097792","-47858688","2810880"],["0","0","0","0","0","0","155713536","-726663168","1417347072","-1504935936","950519808","-366004224","83994624","-10524672","552960"],["0","0","0","0","0","0","28311552","-125042688","227672064","-222068736","126775296","-43582464","8875008","-986112","46080"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","4718592","-40108032","151289856","-332660736","470679552","-445906944","284884992","-120324096","31850496","-4718592","294912"],["0","0","0","0","0","28311552","-212336640","744947712","-1594294272","2262712320","-2177335296","1408942080","-594542592","154386432","-22118400","1327104"],["0","0","0","0","0","56623104","-408158208","1480458240","-3341500416","4899889152","-4711145472","2962685952","-1199702016","300441600","-42098688","2506752"],["0","0","0","0","0","37748736","-391643136","1749417984","-4220485632","6105784320","-5611032576","3365904384","-1315381248","321232896","-44126208","2580480"],["0","0","0","0","0","0","-254803968","1360134144","-3206873088","4411367424","-3908358144","2297733120","-883501056","210696192","-27961344","1566720"],["0","0","0","0","0","0","-94371840","511967232","-1253376000","1809727488","-1670123520","997115904","-376704000","85939200","-10736640","562176"],["0","0","0","0","0","0","0","51904512","-235929600","444137472","-449740800","267098112","-95385600","20109312","-2304000","110592"],["0","0","0","0","0","0","0","9437184","-40108032","69599232","-63995904","34099200","-10884096","2055168","-211968","9216"]]},"deriv_order":2}],"step_multiplier":{"coeffs":[["0","0","0","884736","-5308416","13271040","-17694720","13271040","-5308416","884736"],["0","0","0","5308416","-27869184","59719680","-66355200","39813120","-11943936","1327104"],["0","0","0","10616832","-47775744","85598208","-76972032","35831808","-7962624","663552"],["0","0","0","7077888","-26542080","38486016","-27095040","9621504","-1658880","110592"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","-147456","1105920","-3538944","6266880","-6635520","4202496","-1474560","221184"],["0","0","0","-1327104","8921088","-25325568","39260160","-35758080","19021824","-5419008","626688"],["0","0","0","-4718592","28164096","-70225920","94316544","-73138176","32403456","-7483392","681984"],["0","0","0","-8257536","43352064","-94003200","108251136","-70751232","25906176","-4856832","359424"],["0","0","0","-7077888","32440320","-60604416","59166720","-32200704","9676800","-1492992","92160"],["0","0","0","-2359296","9437184","-15040512","12238848","-5465088","1354752","-175104","9216"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","2654208","-19021824","58834944","-102187008","108380160","-71221248","27869184","-5750784","442368"],["0","0","0","17694720","-112951296","306044928","-455196672","399974400","-206438400","57286656","-6340608","-73728"],["0","0","0","42467328","-235929600","541605888","-654372864","432599040","-139419648","7741440","6377472","-1069056"],["0","0","0","42467328","-194641920","343277568","-268738560","47720448","65249280","-45453312","11059200","-940032"],["0","0","0","14155776","-40108032","8257536","91570176","-139474944","91090944","-30081024","4902912","-313344"],["0","0","0","0","9437184","-37748736","60162048","-48955392","21860352","-5419008","700416","-36864"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","1769472","-13271040","43352064","-80510976","92897280","-68124672","30965760","-7962624","884736"],["0","0","0","0","11796480","-80216064","235192320","-387219456","390021120","-244776960","92749824","-19169280","1622016"],["0","0","0","0","28311552","-173408256","452984832","-655810560","571760640","-304791552","95993856","-16146432","1105920"],["0","0","0","0","28311552","-155713536","360972288","-457408512","343609344","-155271168","40919040","-5750784","331776"],["0","0","0","0","9437184","-47185920","97910784","-109117440","70815744","-27279360","6119424","-737280","36864"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","7962624","-47333376","118996992","-163897344","133816320","-65470464","18579456","-2875392","221184"],["0","0","0","38338560","-208945152","475398144","-581640192","409595904","-163823616","33693696","-2580480","-36864"],["0","0","0","61341696","-304939008","621379584","-663146496","390408192","-120029184","14561280","626688","-202752"],["0","0","0","42467328","-194641920","361857024","-348364800","183582720","-51287040","6552576","-138240","-27648"],["0","0","0","23592960","-103809024","188153856","-182550528","103606272","-35407872","7170048","-792576","36864"],["0","0","0","9437184","-40108032","69599232","-63995904","34099200","-10884096","2055168","-211968","9216"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-21233664","138018816","-393265152","647405568","-683458560","484614144","-233127936","73654272","-13713408","1105920"],["0","0","0","-99090432","586285056","-1499037696","2174607360","-1978122240","1177288704","-462127104","115826688","-16662528","1032192"],["0","0","0","-141557760","736100352","-1606680576","1913683968","-1357074432","588847104","-155271168","23777280","-1880064","55296"],["0","0","0","-56623104","212336640","-261881856","33619968","213000192","-220575744","102297600","-25214976","3207168","-165888"],["0","0","0","0","-37748736","160432128","-278396928","255983616","-136396800","43536384","-8220672","847872","-36864"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","-14155776","99090432","-301694976","522436608","-564461568","392380416","-174292992","47333376","-7077888","442368"],["0","0","0","0","-66060288","417595392","-1137770496","1745141760","-1651359744","993558528","-377782272","87146496","-11059200","589824"],["0","0","0","0","-94371840","537919488","-1309409280","1776549888","-1471979520","768503808","-252149760","50208768","-5529600","258048"],["0","0","0","0","-37748736","198180864","-438829056","534380544","-392380416","179933184","-51757056","9068544","-884736","36864"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["0","0","0","884736","-5308416","13271040","-17694720","13271040","-5308416","884736"],["0","0","0","5308416","-27869184","59719680","-66355200","39813120","-11943936","1327104"],["0","0","0","10616832","-47775744","85598208","-76972032","35831808","-7962624","663552"],["0","0","0","7077888","-26542080","38486016","-27095040","9621504","-1658880","110592"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["1","-1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-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 1 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"],["3"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-1","1"]]},"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_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), V_n(x) = 0, W_n(x) = (-1) + (1) x; open hypotheses: seed_degree_step: degrees 0 and 0 (exact); seed_strict_interlacing: the Bezout test fails or the degrees do not differ by one (exact); degree_step_positive: fails at n = 2: lambda_n = 0 = 0 there (exact); multipliers_vanish_at_zero: [x^0] c_2(n, x) = -1 is not the zero polynomial","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), B_n(x) = (-1) + (1) 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-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), B_n(x) = (-1) + (1) 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-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"}