{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"euler_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["3","8"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["-1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","4"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"basis_map_A013611 of Triangle of coefficients of polynomials v(n,x) jointly generated with A207606; see Formula section."},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["-360","-3072","-6144","0","0"],["120","1904","11200","18176","4096"],["0","80","1792","2048","-2048"],["0","0","-192","-1792","-2048"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["50","1000","8064","26880","30208","8192"],["0","120","2224","11456","13056","0"],["0","0","-80","-256","-4608","-6144"],["0","0","0","-192","-1792","-2048"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","25","680","5568","16512","15104","4096"],["0","0","0","160","128","-2560","-2048"],["0","0","0","-80","-1024","-3328","-2048"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["120","384","0","0"],["-80","-1216","-4160","-1024"],["0","0","-576","0"],["0","0","128","1024"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","120","384","0","0"],["0","-80","-1216","-4160","-1024"],["0","0","0","-576","0"],["0","0","0","128","1024"]]},"deriv_order":1,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"denominator":{"coeffs":[["200","1600","3456","0"],["-80","-1216","-2624","2048"],["0","0","-960","-3072"],["0","0","128","1024"]]},"terms":[{"coeff":{"coeffs":[["480","4896","15360","14336","4096"],["-120","-1744","-7040","-8704","-2048"],["0","-80","-2368","-7424","-4096"],["0","0","192","1792","2048"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-25","-680","-5328","-15360","-14336","-4096"],["0","0","-320","-2176","-4096","-2048"],["0","0","80","1024","3328","2048"]]},"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":["1"]}],"shape":"euler_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["3","8"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["-1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","4"]]},"deriv_order":0,"offset":1,"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":[["-288","-768","0"],["-48","-384","0"],["16","256","1024"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["24","224","128","-1024"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-5","-104","-720","-1792","-1024"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["96"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["2592000","33177600","155934720","323813376","281346048","84934656","0","0","0","0"],["-5184000","-114739200","-954685440","-3806134272","-7511408640","-6794772480","-2505572352","-226492416","0","0"],["3456000","108748800","1347471360","8549203968","29658120192","55051812864","49870798848","19780337664","2415919104","0"],["-768000","-31334400","-509153280","-4432625664","-22923313152","-71338819584","-126669029376","-114579996672","-47110422528","-6442450944"],["0","0","-9216000","-235929600","-2276720640","-10286530560","-21988638720","-19629342720","-6039797760","0"],["0","0","1228800","41287680","555220992","3800039424","13904117760","26071793664","21743271936","6442450944"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","2592000","33177600","155934720","323813376","281346048","84934656","0","0","0","0"],["0","-5184000","-114739200","-954685440","-3806134272","-7511408640","-6794772480","-2505572352","-226492416","0","0"],["0","3456000","108748800","1347471360","8549203968","29658120192","55051812864","49870798848","19780337664","2415919104","0"],["0","-768000","-31334400","-509153280","-4432625664","-22923313152","-71338819584","-126669029376","-114579996672","-47110422528","-6442450944"],["0","0","0","-9216000","-235929600","-2276720640","-10286530560","-21988638720","-19629342720","-6039797760","0"],["0","0","0","1228800","41287680","555220992","3800039424","13904117760","26071793664","21743271936","6442450944"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["-2985984000","-42998169600","-235056660480","-605414227968","-752181313536","-440301256704","-97844723712","0","0","0"],["5971968000","133772083200","1158084034560","4971735023616","11190990274560","12915503529984","7240509554688","1565515579392","0","0"],["-3981312000","-121031884800","-1485507133440","-9490938200064","-33976580308992","-68295617150976","-73709691863040","-39659728011264","-8349416423424","0"],["884736000","33973862400","545280491520","4749998948352","24423130202112","75579613249536","137794362015744","139852725092352","72361609003008","14843406974976"]]},"step_quotients":[[{"coeff":{"coeffs":[["995328000","30257971200","275825295360","996793122816","972331941888","-2299351007232","-5642379067392","-4174708211712","-1043677052928","0","0","0"],["-1492992000","-73256140800","-1117633904640","-7536591765504","-23589751357440","-24803637460992","31457078673408","89103928393728","66795331387392","16698832846848","0","0"],["-165888000","32115916800","1025267466240","12178270715904","71320989597696","213032424701952","271937666285568","-42181947555840","-416427144118272","-345109212168192","-89060441849856","0"],["1363968000","37040947200","261197660160","-1766225608704","-38864664133632","-256149030961152","-837100266061824","-1366646782427136","-842749892886528","260378097352704","514571441799168","158329674399744"],["-811008000","-35271475200","-639510773760","-6174032265216","-32921880625152","-81922608857088","42010417299456","841126395248640","2220635530985472","2632230836895744","1474445092847616","316659348799488"],["147456000","8021606400","190914232320","2608135667712","22553510805504","128391604862976","485024751157248","1196942960885760","1854807396581376","1687200592822272","811439581298688","158329674399744"]]},"deriv_order":0},{"coeff":{"coeffs":[["-746496000","-17716838400","-163074539520","-725299494912","-1455440265216","-165112971264","4403012567040","7207894646784","4566087106560","1043677052928","0","0","0"],["1492992000","47377612800","609618493440","4059791622144","14515672449024","23617270185984","-6164217593856","-84863990366208","-124458488561664","-75144747810816","-16698832846848","0","0"],["-995328000","-39547699200","-659092930560","-5957826379776","-31329336950784","-93161766518784","-121849295929344","89451820744704","535580274327552","713875104202752","411904543555584","89060441849856","0"],["221184000","10557849600","216772116480","2495682183168","17553766219776","76399213805568","192698539573248","196742788153344","-278043297841152","-1110781621960704","-1360645639372800","-752065953398784","-158329674399744"]]},"deriv_order":1},{"coeff":{"coeffs":[["155520000","5474304000","81218764800","664401346560","3292449472512","10224773627904","19931785592832","23906727493632","16976059564032","6522981580800","1043677052928","0","0","0"],["-311040000","-13436928000","-250026393600","-2628302929920","-17215320489984","-73128738816000","-203459949232128","-366722024472576","-416459759026176","-284662916186112","-106455059398656","-16698832846848","0","0"],["207360000","10616832000","238347878400","3085676052480","25494495952896","140567535157248","525659906506752","1329601078886400","2233490636537856","2410893992263680","1589172259258368","578892872024064","89060441849856","0"],["-46080000","-2727936000","-71840563200","-1109435351040","-11151089860608","-76560778395648","-366711152836608","-1229973406875648","-2860066503917568","-4506404241014784","-4639183154970624","-2953837988020224","-1048934092898304","-158329674399744"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["-663552000","-25480396800","-408960368640","-3562499211264","-18317347651584","-56684709937152","-103345771511808","-104889543819264","-54271206752256","-11132555231232","0","0","0"],["165888000","15659827200","458965647360","6616069963776","54454325870592","270614044606464","819422381998080","1473063187120128","1482021415157760","762580033339392","155855773237248","0","0"],["460800000","15777792000","165563596800","-428825640960","-25198828978176","-254219013586944","-1329426528731136","-4055081561358336","-7246906908475392","-7234923949719552","-3698482237931520","-752065953398784","0"],["-294912000","-14863564800","-317655613440","-3688957476864","-24241936269312","-76355123281920","57083336589312","1486312087486464","5865928893923328","11464057987006464","11874725579980800","6174857301590016","1266637395197952"],["73728000","4600627200","127543541760","2067724763136","21709298073600","154409845653504","756078795030528","2538570485071872","5715175541833728","8262829882736640","7154522161938432","3324923162394624","633318697598976"]]},"deriv_order":0},{"coeff":{"coeffs":[["-995328000","-43860787200","-835332341760","-9023755124736","-61028947722240","-269224513634304","-783377472946176","-1489251053076480","-1799734104686592","-1317120440795136","-528796373483520","-89060441849856","0","0"],["1050624000","54942105600","1263827681280","16827650408448","143632657022976","822518080339968","3215351567351808","8568893010345984","15307002523680768","17738799048032256","12635450187448320","4987384743591936","831230790598656","0"],["-258048000","-15659827200","-424107048960","-6760553250816","-70449107042304","-504071555383296","-2531743097683968","-8970621702635520","-22232582527647744","-37718797930463232","-42236914547294208","-29449319438352384","-11478901393981440","-1899956092796928"]]},"deriv_order":1},{"coeff":{"coeffs":[["-51840000","-2654208000","-59586969600","-771419013120","-6373623988224","-35141883789312","-131414976626688","-332400269721600","-558372659134464","-602723498065920","-397293064814592","-144723218006016","-22265110462464","0","0"],["69120000","4091904000","107760844800","1664153026560","16726634790912","114841167593472","550066729254912","1844960110313472","4290099755876352","6759606361522176","6958774732455936","4430756982030336","1573401139347456","237494511599616","0"],["-23040000","-1548288000","-46832025600","-842079928320","-10013286334464","-82884748640256","-489598690000896","-2081831314784256","-6349926879461376","-13693468136177664","-20345208541544448","-20033651613892608","-12339818998530048","-4274901208793088","-633318697598976"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0"],["144","0"],["144","0"],["-32","-256"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-48","-96","0"],["-48","-64","256"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-15","-72","-48","0"],["10","128","416","256"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["-864000","-35251200","-538583040","-4002988032","-15615590400","-31602769920","-30576476160","-13023313920","-1811939328","0","0"],["1152000","56217600","1094584320","11060822016","63314657280","208240902144","377945063424","344155226112","141633257472","19327352832","0"],["-384000","-21811200","-510781440","-6449528832","-48672079872","-228224139264","-658411880448","-1102841905152","-960428507136","-384936443904","-51539607552"],["0","0","-3686400","-160727040","-2609381376","-20507000832","-82858475520","-166169935872","-143747186688","-43486543872","0"],["0","0","614400","30474240","607911936","6341787648","37352374272","124268838912","219445985280","177167400960","51539607552"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","-864000","-24883200","-284221440","-1647378432","-5147394048","-8436842496","-6455033856","-1811939328","0","0","0"],["0","1152000","44697600","718571520","6194036736","30952194048","90445971456","148017512448","122758889472","44996493312","4831838208","0"],["0","-384000","-18739200","-385443840","-4394483712","-30558191616","-133534580736","-361882976256","-575743721472","-485499076608","-191662915584","-25769803776"],["0","0","0","-3686400","-123863040","-1665662976","-11400118272","-41712353280","-78215380992","-65229815808","-19327352832","0"],["0","0","0","614400","25559040","442761216","4120903680","22152216576","68652367872","115158810624","90194313216","25769803776"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["-2985984000","-42998169600","-235056660480","-605414227968","-752181313536","-440301256704","-97844723712","0","0","0"],["5971968000","133772083200","1158084034560","4971735023616","11190990274560","12915503529984","7240509554688","1565515579392","0","0"],["-3981312000","-121031884800","-1485507133440","-9490938200064","-33976580308992","-68295617150976","-73709691863040","-39659728011264","-8349416423424","0"],["884736000","33973862400","545280491520","4749998948352","24423130202112","75579613249536","137794362015744","139852725092352","72361609003008","14843406974976"]]},"step_quotients":[[{"coeff":{"coeffs":[["-7962624000","-106699161600","-512155975680","-987620179968","-391378894848","831680151552","913217421312","260919263232","0","0","0"],["5474304000","214194585600","2252785582080","9931239456768","18795359895552","9075098124288","-11953363746816","-14350559477760","-4174708211712","0","0"],["8792064000","110680473600","-429026181120","-11633669701632","-61433236684800","-130043791540224","-88946289672192","39137889484800","70970039599104","22265110462464","0"],["-7593984000","-262117785600","-3165656186880","-16071826341888","-22842062143488","88277684060160","355789990526976","399477055684608","95554432401408","-86586540687360","-39582418599936"],["-884736000","22649241600","1119438766080","14655871254528","89431889412096","272660630077440","350298606403584","-62852551409664","-556627761561600","-460145616224256","-118747255799808"],["1769472000","60869836800","818770083840","5137753964544","10846268817408","-44225815117824","-329048181964800","-822649445941248","-974098582732800","-549206058074112","-118747255799808"],["-294912000","-13683916800","-272357130240","-3037414293504","-20807707262976","-90321551622144","-247477089337344","-414069207072768","-397061136580608","-197912092999680","-39582418599936"]]},"deriv_order":0},{"coeff":{"coeffs":[["2985984000","47974809600","298757652480","882513543168","1134387265536","79498838016","-1174136684544","-1011062145024","-260919263232","0","0","0"],["-4478976000","-120235622400","-1226881105920","-6200399757312","-16236108840960","-19202027028480","-587068342272","19699404374016","16437913583616","4174708211712","0","0"],["995328000","56800051200","1024311951360","8742833750016","40011697225728","98953630580736","114543556558848","9219147300864","-103845866766336","-87668872445952","-22265110462464","0"],["1105920000","27721728000","213280358400","-155147304960","-11531483873280","-72128472809472","-206850993684480","-281116346941440","-103942503530496","137301514518528","145960168587264","39582418599936"],["-442368000","-17576755200","-292930191360","-2647922835456","-13924149755904","-41405229563904","-54155242635264","39756364775424","238035677478912","317277824090112","183068686024704","39582418599936"]]},"deriv_order":1},{"coeff":{"coeffs":[["155520000","497664000","-24286003200","-278373335040","-1329694507008","-3363412377600","-4749545963520","-3750714408960","-1549208125440","-260919263232","0","0","0"],["-622080000","-11943936000","-54145843200","374561832960","5094550536192","23702884319232","57842539167744","79449915654144","61511716306944","25048249270272","4174708211712","0","0"],["829440000","25878528000","316381593600","1810806865920","3385835126784","-15706796064768","-111825647566848","-297708879347712","-419471202189312","-327366702268416","-133590662774784","-22265110462464","0"],["-460800000","-19169280000","-338558976000","-3301126963200","-19274127114240","-67532186714112","-128079951298560","-61016452890624","252289600192512","565441034452992","517045342961664","227598906949632","39582418599936"],["92160000","4718592000","105932390400","1371411578880","11330887090176","62474460069888","233626625114112","590933812838400","992662505127936","1071508441006080","706298781892608","257285720899584","39582418599936"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["-7630848000","-112538419200","-553986293760","-533049901056","4225669005312","15426851438592","20753953062912","12437151547392","2783138807808","0","0","0"],["13768704000","340269465600","3234842542080","14309620973568","23493945065472","-34278268207104","-192955230978048","-279227098202112","-171858821382144","-38963943309312","0","0"],["-6948864000","-251648409600","-3731356385280","-28914890047488","-122165743583232","-250278649528320","-56622500020224","720678332399616","1242787441803264","808347204845568","188016488349696","0"],["110592000","23121100800","774061424640","11501624623104","92753551687680","429140918403072","1108562600263680","1344729564315648","52956946759680","-1437955050700800","-1227054976598016","-316659348799488"],["663552000","27249868800","448596541440","3565896597504","10368369819648","-46468996005888","-527035168456704","-2038069356134400","-4075442927566848","-4319431429718016","-2285884674146304","-474989023199232"],["-147456000","-8021606400","-190914232320","-2608135667712","-22553510805504","-128391604862976","-485024751157248","-1196942960885760","-1854807396581376","-1687200592822272","-811439581298688","-158329674399744"]]},"deriv_order":0},{"coeff":{"coeffs":[["-2239488000","-45851443200","-256714997760","870282952704","16995084926976","87104226852864","229021883301888","338879764758528","282966940975104","124197569298432","22265110462464","0","0"],["4700160000","151511040000","1938987417600","11984138403840","28942786363392","-66221399605248","-658107235565568","-1959496419115008","-3029069708918784","-2583216670113792","-1148508614688768","-207807697649664","0"],["-2912256000","-124364390400","-2266150993920","-22946871508992","-140417446182912","-523494940999680","-1095488854032384","-774326232023040","1760779825053696","4920434793381888","5085103839510528","2483796767145984","474989023199232"],["516096000","27190886400","630687006720","8475610447872","73093330501632","423396466753536","1676314461339648","4530727714553856","8219343338864640","9682849150009344","7011035894513664","2810351720595456","474989023199232"]]},"deriv_order":1},{"coeff":{"coeffs":[["-51840000","-995328000","2123366400","211699630080","2445990690816","14151472644096","47888197484544","98333947330560","121843860111360","88364657147904","34441342746624","5566277615616","0","0"],["172800000","6359040000","91127808000","571185561600","218989854720","-20582951288832","-146979988439040","-519678694785024","-1072533998665728","-1322599745323008","-952993113440256","-369229748502528","-59373627899904","0"],["-161280000","-7888896000","-166507315200","-1976240701440","-14343406092288","-64006756761600","-158948753670144","-99627672010752","626575867379712","2095510248751104","3050010895712256","2374945115996160","959873651048448","158329674399744"],["46080000","2727936000","71840563200","1109435351040","11151089860608","76560778395648","366711152836608","1229973406875648","2860066503917568","4506404241014784","4639183154970624","2953837988020224","1048934092898304","158329674399744"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["2073600","19906560","61046784","63700992","21233664","0","0"],["-2764800","-48660480","-293732352","-736100352","-707788800","-226492416","0"],["921600","23592960","227672064","1028653056","2198863872","1962934272","603979776"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-3","-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 + (1) theta; 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 + (1) theta 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, 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 + (1) theta 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 + (1) theta","kind":"preserver_image","operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"euler_polynomial"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["3","8"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["-1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","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 + (1) theta, 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 = 4 != 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of f(n) a_n = 4 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":["4"]},"numerator":["4"],"range":{"first":"2","last":null}},"decision":"holds"},"statement":"a_n != 0 for every n >= 2","status":{"kind":"verified"}},{"evidence":"Q_0 has degree 0, Q_1 degree 1; 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/32 (exact)","name":"first_coefficient_positive","statement":"beta_2 = c_2 L_0 / (a_2 L_1) > 0","status":{"kind":"verified"}},{"evidence":"beta_n = 1/16 > 0 for every integer n in [3, +inf) (exact; Taylor shift: the coefficients of beta_n = 1/16 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/16"]},"numerator":["1/16"],"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) = 3/8 ((t - alpha_n)/2): 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":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["5/24"]},"numerator":["5/24"],"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 = 4, b_n = 3, c_n = 1","recurrence":{"first_index":0,"initial_polynomials":[["1"],["3","8"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["-1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","4"]]},"deriv_order":0,"offset":1,"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":"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":"P_n = (a_n x + b_n) P_(n-1) - c_n P_(n-2) for n >= 2, with a_n = 4, b_n = 3, 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 = 4, b_n = 3, 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 + (1) theta 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"}