{"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":[["4","7","2"],["5","16","11","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"Triangle of coefficients of polynomials u(n,x) jointly generated with A207607; see the Formula section."},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["40","-1480","292","2652","-384"],["8","-1128","2126","2696","-704"],["0","-260","1496","823","-504"],["0","-20","382","19","-176"],["0","0","42","-27","-30"],["0","0","2","-3","-2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","184","-8488","9908","8420","-1664"],["0","24","-4824","14658","7176","-2880"],["0","0","-940","6896","1417","-1928"],["0","0","-60","1434","-255","-624"],["0","0","0","142","-109","-98"],["0","0","0","6","-9","-6"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0","120","-6540","11582","3232","-1024"],["0","0","8","-2928","12476","1556","-1664"],["0","0","0","-460","4506","-492","-1024"],["0","0","0","-20","742","-371","-296"],["0","0","0","0","62","-62","-40"],["0","0","0","0","2","-3","-2"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["0","0","0","16","-1012","2258","116","-128"],["0","0","0","0","-360","2070","-228","-192"],["0","0","0","0","-40","602","-263","-104"],["0","0","0","0","0","72","-78","-24"],["0","0","0","0","0","4","-7","-2"]]},"deriv_order":3,"shift":0},{"coeff":{"coeffs":[["-32","1280","-2288","360"],["-8","984","-3112","744"],["0","240","-1580","610"],["0","20","-368","248"],["0","0","-40","50"],["0","0","-2","4"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-96","3840","-6864","1080"],["0","-24","2952","-9336","2232"],["0","0","720","-4740","1830"],["0","0","60","-1104","744"],["0","0","0","-120","150"],["0","0","0","-6","12"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["0","0","-32","1280","-2288","360"],["0","0","-8","984","-3112","744"],["0","0","0","240","-1580","610"],["0","0","0","20","-368","248"],["0","0","0","0","-40","50"],["0","0","0","0","-2","4"]]},"deriv_order":2,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["4","28","18"]],"recurrence":{"denominator":{"coeffs":[["-24","516","-426","24"],["-8","564","-906","88"],["0","180","-696","126"],["0","20","-228","88"],["0","0","-30","30"],["0","0","-2","4"]]},"terms":[{"coeff":{"coeffs":[["-32","592","680","-736","36"],["-8","668","-122","-1200","114"],["0","200","-582","-634","136"],["0","20","-234","-97","76"],["0","0","-32","12","20"],["0","0","-2","3","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","-16","692","-722","-152","18"],["0","0","280","-1066","-92","48"],["0","0","40","-410","71","44"],["0","0","0","-56","50","16"],["0","0","0","-4","7","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":[["4","7","2"],["5","16","11","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-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":[["3","-42","24"],["8","-26","20"],["1","-4","4"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-6","13","2","-8"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-4","15","-12","-4"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["6"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","4718592","-202899456","913342464","-1450377216","686905344","305989632","-208748160","-58867200","5256000","1620000"],["0","0","0","4718592","-303464448","1692426240","-3247607808","2009816064","545019264","-619088544","-127582560","25027200","5292000"],["0","0","0","1769472","-186900480","1321537536","-3080908800","2430383616","297588960","-768300192","-99168192","45200880","7540200"],["0","0","0","294912","-61028352","568327680","-1619335296","1603512864","-31354272","-520682112","-21248928","43235784","6120720"],["0","0","0","18432","-11211264","147648384","-517642848","636692832","-106023456","-209891808","15258456","24631200","3096072"],["0","0","0","0","-1105920","23924736","-103905792","157306752","-51275520","-51147432","12033360","8679456","999360"],["0","0","0","0","-46080","2416896","-13007808","23955120","-11980512","-7278048","3589200","1862208","201024"],["0","0","0","0","0","147456","-958464","2101248","-1433088","-546624","514944","223488","23040"],["0","0","0","0","0","4608","-33408","83808","-71352","-16704","29376","11520","1152"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","14155776","-608698368","2740027392","-4351131648","2060716032","917968896","-626244480","-176601600","15768000","4860000"],["0","0","0","0","14155776","-910393344","5077278720","-9742823424","6029448192","1635057792","-1857265632","-382747680","75081600","15876000"],["0","0","0","0","5308416","-560701440","3964612608","-9242726400","7291150848","892766880","-2304900576","-297504576","135602640","22620600"],["0","0","0","0","884736","-183085056","1704983040","-4858005888","4810538592","-94062816","-1562046336","-63746784","129707352","18362160"],["0","0","0","0","55296","-33633792","442945152","-1552928544","1910078496","-318070368","-629675424","45775368","73893600","9288216"],["0","0","0","0","0","-3317760","71774208","-311717376","471920256","-153826560","-153442296","36100080","26038368","2998080"],["0","0","0","0","0","-138240","7250688","-39023424","71865360","-35941536","-21834144","10767600","5586624","603072"],["0","0","0","0","0","0","442368","-2875392","6303744","-4299264","-1639872","1544832","670464","69120"],["0","0","0","0","0","0","13824","-100224","251424","-214056","-50112","88128","34560","3456"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","4718592","-202899456","913342464","-1450377216","686905344","305989632","-208748160","-58867200","5256000","1620000"],["0","0","0","0","0","4718592","-303464448","1692426240","-3247607808","2009816064","545019264","-619088544","-127582560","25027200","5292000"],["0","0","0","0","0","1769472","-186900480","1321537536","-3080908800","2430383616","297588960","-768300192","-99168192","45200880","7540200"],["0","0","0","0","0","294912","-61028352","568327680","-1619335296","1603512864","-31354272","-520682112","-21248928","43235784","6120720"],["0","0","0","0","0","18432","-11211264","147648384","-517642848","636692832","-106023456","-209891808","15258456","24631200","3096072"],["0","0","0","0","0","0","-1105920","23924736","-103905792","157306752","-51275520","-51147432","12033360","8679456","999360"],["0","0","0","0","0","0","-46080","2416896","-13007808","23955120","-11980512","-7278048","3589200","1862208","201024"],["0","0","0","0","0","0","0","147456","-958464","2101248","-1433088","-546624","514944","223488","23040"],["0","0","0","0","0","0","0","4608","-33408","83808","-71352","-16704","29376","11520","1152"]]},"deriv_order":2}],"step_multiplier":{"coeffs":[["0","0","0","-884736","2654208","-1824768","-774144","570240","259200","27000"],["0","0","0","-663552","2488320","-2239488","-642816","785376","320760","32400"],["0","0","0","-165888","746496","-870912","-129600","355752","132192","12960"],["0","0","0","-13824","72576","-106272","1512","53136","18144","1728"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","-3538944","20348928","-43573248","38209536","-3801600","-11428992","1818720","1776600","216000"],["0","0","0","-4128768","26689536","-63848448","63406080","-10881792","-18910656","4121568","3266280","385200"],["0","0","0","-1916928","13750272","-36615168","41121792","-10223424","-12190032","3557052","2383056","272880"],["0","0","0","-442368","3483648","-10264320","13003200","-4324752","-3798900","1480248","861840","95904"],["0","0","0","-50688","434304","-1406304","2000088","-850860","-565344","299232","154368","16704"],["0","0","0","-2304","21312","-75312","119484","-63000","-31392","23616","10944","1152"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","884736","-4571136","7280640","-1115136","-6394752","3151296","1756872","-615420","-336600","-36000"],["0","0","0","663552","-3926016","7409664","-2495232","-6242400","4152600","1781460","-870048","-416880","-43200"],["0","0","0","165888","-1105920","2433024","-1287360","-1922184","1756620","564840","-402192","-171936","-17280"],["0","0","0","13824","-102528","258912","-189144","-182052","239184","53280","-61056","-23616","-2304"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","589824","-3981312","9621504","-8764416","-435456","4017600","5616","-831060","-226800","-18000"],["0","0","0","0","442368","-3317760","9040896","-9704448","689472","4528224","-361908","-1084104","-278640","-21600"],["0","0","0","0","110592","-912384","2778624","-3473280","682992","1641060","-303264","-469152","-114048","-8640"],["0","0","0","0","9216","-82944","279936","-402624","132516","188568","-63072","-67392","-15552","-1152"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","1105920","-9086976","29021184","-43792128","27484128","1943064","-8370144","513792","1100160","144000"],["0","0","0","921600","-8303616","29509632","-50688000","38445552","-1637100","-11646576","1520064","1738944","216000"],["0","0","0","290304","-2848896","11147616","-21454488","19061316","-2765196","-5730624","1223136","994752","118080"],["0","0","0","41472","-438912","1867104","-3958200","4001616","-946944","-1178496","369792","241920","27648"],["0","0","0","2304","-25920","117936","-270108","301968","-94608","-86400","36288","20736","2304"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-221184","2451456","-10202112","19222272","-13202784","-5305176","8495928","1259280","-1827360","-630720","-57600"],["0","0","0","-110592","1281024","-5723136","11964672","-9999504","-2119932","6492960","325728","-1648512","-520128","-46080"],["0","0","0","-13824","167040","-795744","1826712","-1806732","-73224","1179360","-84672","-368064","-107136","-9216"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","-147456","1400832","-5225472","9262080","-6699456","-1049760","3139452","120096","-629856","-178560","-14400"],["0","0","0","0","-73728","755712","-3068928","6020352","-5086368","-183384","2390256","-91584","-549504","-146304","-11520"],["0","0","0","0","-9216","101376","-445824","962496","-937764","76464","440208","-58752","-119232","-29952","-2304"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["42","-30"],["41","-37"],["12","-15"],["1","-2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-24","-2","10"],["-6","1","4"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-16","16","5"],["0","-4","7","2"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","-1179648","63700992","-836739072","3223756800","-4836533760","2152424448","1052306208","-648351648","-189198720","16430400","5184000"],["0","0","0","-884736","72032256","-1050439680","4895585280","-9003293568","5482109088","1522486656","-1678486608","-337943808","72184320","14860800"],["0","0","0","-221184","32919552","-546140160","3088242432","-6929364384","5537183040","582442560","-1750905792","-193254048","113771664","18184320"],["0","0","0","-18432","7672320","-151712640","1056947040","-2876940576","2934030672","-170280432","-954583200","-2339568","91128240","12312576"],["0","0","0","0","921600","-24247296","214154496","-703681344","896259168","-203123808","-292568328","42576624","41443488","4982400"],["0","0","0","0","46080","-2269440","26283456","-103388976","161205696","-65359800","-50093928","18740448","10877472","1204992"],["0","0","0","0","0","-129024","1912320","-8765568","16281504","-9557856","-4436352","3354624","1539072","161280"],["0","0","0","0","0","-4608","70272","-351072","741816","-554112","-163008","223488","91008","9216"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","-3538944","168394752","-1407246336","4504817664","-6178254336","2584384128","1344720672","-805208400","-239983200","19944000","6480000"],["0","0","0","0","-2654208","200613888","-1932244992","7223569920","-11803484160","6639493248","2041450272","-2078412048","-433530720","88372800","18576000"],["0","0","0","0","-663552","95275008","-1096800768","4838050944","-9385490880","6804835344","930738816","-2172121776","-258006456","139723920","22730400"],["0","0","0","0","-55296","22758912","-333532800","1763214624","-4048008480","3680467056","-74555568","-1193896152","-16713072","112057056","15390720"],["0","0","0","0","0","2764800","-58871808","380984832","-1032551424","1154149488","-204583248","-372537216","46374408","50979168","6228000"],["0","0","0","0","0","138240","-6163200","49819968","-158561424","214112448","-72451152","-66052872","21439440","13377312","1506240"],["0","0","0","0","0","0","-387072","3833856","-14047488","22360320","-11107656","-6240960","3882816","1891584","201600"],["0","0","0","0","0","0","-13824","146304","-585504","1052136","-663408","-255168","259200","111744","11520"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","-1179648","53968896","-368492544","1018220544","-1262670336","482447232","274330368","-157108032","-47818080","3945600","1296000"],["0","0","0","0","0","-884736","65396736","-530436096","1705946112","-2485277568","1262625120","440897760","-404647776","-87160032","17441280","3715200"],["0","0","0","0","0","-221184","31426560","-314463744","1193880960","-2043398592","1324351872","235808352","-424725840","-53609400","27531936","4546080"],["0","0","0","0","0","-18432","7561728","-99623808","453957984","-913303584","736269984","18864720","-236349072","-5772672","22051008","3078144"],["0","0","0","0","0","0","921600","-18302976","102090240","-241546752","238188816","-29088504","-75523968","7856136","10019808","1245600"],["0","0","0","0","0","0","46080","-1992960","13841856","-38423088","45681984","-12326400","-13951512","3845520","2626272","301248"],["0","0","0","0","0","0","0","-129024","1096704","-3515904","4931136","-2029608","-1407168","705600","370944","40320"],["0","0","0","0","0","0","0","-4608","42624","-150624","238968","-126000","-62784","47232","21888","2304"]]},"deriv_order":2}],"step_multiplier":{"coeffs":[["0","0","0","-884736","2654208","-1824768","-774144","570240","259200","27000"],["0","0","0","-663552","2488320","-2239488","-642816","785376","320760","32400"],["0","0","0","-165888","746496","-870912","-129600","355752","132192","12960"],["0","0","0","-13824","72576","-106272","1512","53136","18144","1728"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","-14155776","54853632","-66355200","13160448","19961856","-3836160","-3196800","-378000"],["0","0","0","-20643840","89948160","-123641856","34495488","37446912","-9863424","-6819840","-782100"],["0","0","0","-12386304","60272640","-93892608","34532352","28363392","-10133424","-6018408","-670140"],["0","0","0","-3907584","21113856","-37165824","17349696","11004048","-5377536","-2811384","-304272"],["0","0","0","-681984","4073472","-8080128","4673664","2271960","-1563840","-732960","-77184"],["0","0","0","-62208","409536","-913680","644436","230040","-237168","-101088","-10368"],["0","0","0","-2304","16704","-41904","35676","8352","-14688","-5760","-576"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","4423680","-13123584","6617088","10368000","-6979968","-3197376","1152360","600300","63000"],["0","0","0","4202496","-15132672","10911744","11632896","-10960992","-3914856","2013444","920340","93600"],["0","0","0","1492992","-6303744","6054912","4463424","-6174792","-1641060","1287900","525528","51840"],["0","0","0","235008","-1134720","1371744","661608","-1471860","-255348","358560","132336","12672"],["0","0","0","13824","-74880","109152","29160","-123732","-8280","36720","12384","1152"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","2949120","-12238848","15224832","-1317888","-6997248","418752","1568880","405900","31500"],["0","0","0","0","2801664","-13639680","20247552","-4267008","-9586368","1425888","2512332","616320","46800"],["0","0","0","0","995328","-5557248","9745920","-3390336","-4718736","1260036","1492992","348624","25920"],["0","0","0","0","156672","-986112","2012544","-1008576","-973980","428688","389952","86976","6336"],["0","0","0","0","9216","-64512","150912","-100800","-69084","50400","37728","8064","576"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","4644864","-29288448","62530560","-49856256","711648","14683608","-1340496","-1986480","-252000"],["0","0","0","5050368","-34477056","83865600","-80418816","9869040","23986548","-3931992","-3723192","-450000"],["0","0","0","2207232","-16295040","44166240","-49540824","11344212","14850036","-3794436","-2717280","-314640"],["0","0","0","483840","-3858048","11497824","-14695992","4890960","4336596","-1634040","-963216","-107424"],["0","0","0","52992","-455616","1481616","-2119572","913860","596736","-322848","-165312","-17856"],["0","0","0","2304","-21312","75312","-119484","63000","31392","-23616","-10944","-1152"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-1105920","9824256","-27767808","26198784","5592096","-15843672","-1598976","3441780","1127160","100800"],["0","0","0","-774144","7197696","-22625280","25777152","1265616","-16182900","-101340","4165056","1258704","109440"],["0","0","0","-179712","1742976","-5991264","8017560","-922068","-5200884","592632","1645776","462816","39168"],["0","0","0","-13824","139392","-516960","792792","-221148","-515520","148320","211968","55872","4608"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","-737280","5087232","-12635136","11999232","205632","-5527008","115020","1192428","319680","25200"],["0","0","0","0","-516096","3926016","-10893312","12019968","-1144800","-5622264","564084","1396872","354672","27360"],["0","0","0","0","-119808","995328","-3058560","3875904","-815508","-1829628","366336","536544","129600","9792"],["0","0","0","0","-9216","82944","-279936","402624","-132516","-188568","63072","67392","15552","1152"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["0","0","0","-884736","2654208","-1824768","-774144","570240","259200","27000"],["0","0","0","-663552","2488320","-2239488","-642816","785376","320760","32400"],["0","0","0","-165888","746496","-870912","-129600","355752","132192","12960"],["0","0","0","-13824","72576","-106272","1512","53136","18144","1728"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["1"]]},"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 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":{"from_index":1,"justification":"the parent theorem (ThreeTermRecurrence) 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 (ThreeTermRecurrence) 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":[["4","7","2"],["5","16","11","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-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":"three_term_recurrence","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 simple roots from n = 0 on; P_(n-1) strictly interlaces P_n for n >= 1; every root lies in (-inf, 0)"},"hypotheses":[{"evidence":"f(n) a_n = 1 != 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of f(n) a_n = 1 at n = 2 + u have one sign)","name":"leading_coefficient_nonzero","sign_decision":{"certificate":{"condition":"nonzero","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 for every n >= 2","status":{"kind":"verified"}},{"evidence":"Q_0 has degree 2, Q_1 degree 3; simple real roots and strict interlacing checked exactly","name":"seeds_interlace","statement":"Q_0 and Q_1 have simple real roots, degrees e and e + 1, and Q_0 strictly interlaces Q_1","status":{"kind":"verified"}},{"evidence":"beta_2 = 1 (exact)","name":"first_coefficient_positive","statement":"beta_2 = c_2 L_0 / (a_2 L_1) > 0","status":{"kind":"verified"}},{"evidence":"beta_n = 1 > 0 for every integer n in [3, +inf) (exact; Taylor shift: the coefficients of beta_n = 1 at n = 3 + u have one sign)","name":"recurrence_coefficient_positive","sign_decision":{"certificate":{"condition":"positive","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1"]},"numerator":["1"],"range":{"first":"3","last":null}},"decision":"holds"},"statement":"beta_n = c_n / (a_n a_(n-1)) > 0 for every n >= 3","status":{"kind":"verified"}},{"evidence":"seeds checked exactly; positive-ratio induction at t = 0 with g(n) = (n + 4)/(n + 3) (the exact ratio r_n): g(n) > 0 for n >= 2, r_2 >= g(2) exactly, and (t - alpha_n) - beta_n/g(n-1) - g(n) >= 0 for every integer n in [3, +inf) (exact; Taylor shift: the coefficients of (t - alpha_n) - beta_n/g(n-1) - g(n) at n = 3 + u have one sign)","name":"root_upper_bound","sign_decision":{"certificate":{"condition":"nonnegative","denominator":["3","1"],"method":{"kind":"taylor_shift","shifted_denominator":["6","1"],"shifted_numerator":[]},"numerator":[],"range":{"first":"3","last":null}},"decision":"holds"},"statement":"every root of P_n is < 0 for every n >= 0 (region (-inf, 0) for P)","status":{"kind":"verified"}}],"lean_replay":"not_attempted","normal_form":"P_n = (a_n x + b_n) P_(n-1) - c_n P_(n-2) for n >= 2, with a_n = 1, b_n = 2, c_n = 1","recurrence":{"first_index":0,"initial_polynomials":[["4","7","2"],["5","16","11","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"reference":"three-term recurrence Q_n = (a_n y + b_n) Q_(n-1) - c_n Q_(n-2) with a_n != 0 and beta_n = c_n / (a_n a_(n-1)) > 0: simple real roots and strict interlacing of consecutive rows (zero separation for orthogonal polynomials: G. Szeg\u0151, Orthogonal Polynomials, \u00a73.3; Favard, C. R. Acad. Sci. Paris 200 (1935)); root regions by a positive-ratio (chain-sequence) induction","requested_root_region":{"upper":{"closed":false,"value":"0"}},"schema":"polytool.recurrence-real-rootedness-theorem.v1","status":"proved","theorem":"three_term_recurrence"},"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: 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":"P_n = (a_n x + b_n) P_(n-1) - c_n P_(n-2) for n >= 2, with a_n = 1, b_n = 2, c_n = 1: every P_n, n >= 0, is nonzero and real-rooted, with simple roots from n = 0 on; P_(n-1) strictly interlaces P_n for n >= 1; every root lies in (-inf, 0)","route":"three_term_recurrence","success":true,"variant":"three_term_recurrence"}],"conditional_on":[],"interlacing":{"from_index":1,"justification":{"premises":["every hypothesis of the theorem is verified exactly for every index: P_n = (a_n x + b_n) P_(n-1) - c_n P_(n-2) for n >= 2, with a_n = 1, b_n = 2, c_n = 1","every P_n, n >= 0, is nonzero and real-rooted, with simple roots from n = 0 on; P_(n-1) strictly interlaces P_n for n >= 1; every root lies in (-inf, 0)"],"theorem":"three_term_recurrence: three-term recurrence Q_n = (a_n y + b_n) Q_(n-1) - c_n Q_(n-2) with a_n != 0 and beta_n = c_n / (a_n a_(n-1)) > 0: simple real roots and strict interlacing of consecutive rows (zero separation for orthogonal polynomials: G. Szeg\u0151, Orthogonal Polynomials, \u00a73.3; Favard, C. R. Acad. Sci. Paris 200 (1935)); root regions by a positive-ratio (chain-sequence) induction"},"kind":"strict","orientation":"previous_interlaces_next"},"route":"three_term_recurrence","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"}