{"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":[["13","33","18"],["34","132","153","54"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["-1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","3"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"basis_map_A013610 of 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":[["30","2322","12366","2430","-11664"],["90","1161","5346","-6237","-12636"],["0","45","81","-4050","-4374"],["0","0","-81","-567","-486"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["50","900","6516","15120","-10206","-19440"],["0","90","891","1134","-18387","-18468"],["0","0","-45","-783","-6156","-5346"],["0","0","0","-81","-567","-486"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","25","435","2097","1377","-6318","-3888"],["0","0","0","-135","-2106","-6075","-2916"],["0","0","0","-45","-432","-1053","-486"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["-60","-1404","-3024","4860"],["-60","-594","-1134","5994"],["0","0","162","2430"],["0","0","54","324"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-60","-1404","-3024","4860"],["0","-60","-594","-1134","5994"],["0","0","0","162","2430"],["0","0","0","54","324"]]},"deriv_order":1,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["13","66","54"]],"recurrence":{"denominator":{"coeffs":[["0","-810","-1782","972"],["-60","-594","-1296","2106"],["0","0","0","1458"],["0","0","54","324"]]},"terms":[{"coeff":{"coeffs":[["60","-1206","-7182","-5184","2916"],["-90","-1071","-4941","-162","5346"],["0","-45","-324","2349","2916"],["0","0","81","567","486"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-25","-435","-2187","-3051","1296","1458"],["0","0","45","1242","3969","1944"],["0","0","45","432","1053","486"]]},"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":[["13","33","18"],["34","132","153","54"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["-1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","3"]]},"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":[["-135","162","1944"],["18","378","1620"],["9","108","324"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["3","-63","-594","-648"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-5","-78","-405","-756","-324"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["54"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["-81000","-4908600","-111653640","-1185074064","-5994182088","-13741883280","-8608399416","13335626160","16793535600","4782969000"],["-243000","-12174300","-225246420","-1945940112","-8285309532","-14851689552","2546429076","40111749504","37083952980","9725370300"],["-243000","-9622800","-141557220","-1008898092","-3409541748","-2464547796","15818754708","41166837036","31969364796","7875955620"],["-81000","-2357100","-27672840","-148829724","-148724748","2245042980","10862181648","19387676268","13509230220","3175891416"],["0","0","364500","12465900","155626920","931399560","2849704740","4311757980","2806008480","637729200"],["0","0","72900","1837080","18528264","95108256","260996580","367048584","229582512","51018336"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","-81000","-4908600","-111653640","-1185074064","-5994182088","-13741883280","-8608399416","13335626160","16793535600","4782969000"],["0","-243000","-12174300","-225246420","-1945940112","-8285309532","-14851689552","2546429076","40111749504","37083952980","9725370300"],["0","-243000","-9622800","-141557220","-1008898092","-3409541748","-2464547796","15818754708","41166837036","31969364796","7875955620"],["0","-81000","-2357100","-27672840","-148829724","-148724748","2245042980","10862181648","19387676268","13509230220","3175891416"],["0","0","0","364500","12465900","155626920","931399560","2849704740","4311757980","2806008480","637729200"],["0","0","0","72900","1837080","18528264","95108256","260996580","367048584","229582512","51018336"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["19683000","1098311400","23723526240","250823145888","1383081579792","4149244739376","6772224938976","5764816876320","2402007031800","387420489000"],["59049000","2763493200","49487785920","437176121184","2106419547600","5746909440384","8799438519936","7202921731488","2928898896840","464904586800"],["59049000","2232052200","32587962120","245283404904","1050225201144","2632048708824","3800164529880","2997084902904","1190155742208","185961834720"],["19683000","566870400","6823702440","44581522608","171919037736","399014405856","545602839768","415314764208","161166923424","24794911296"]]},"step_quotients":[[{"coeff":{"coeffs":[["19683000","1393556400","41615373240","685754460288","6853522657392","42954734940192","168592769774640","406093812196032","576474455782872","451484341061040","178755813624600","27894275208000"],["72171000","4597948800","123915507480","1852767718416","16904679044976","97334516044224","354911222663280","805577943871584","1093980069402264","831811419187776","323000210089080","49744790787600"],["101695500","5832072900","142459255440","1942534480608","16242014633256","86371759777464","294174709948656","631873749049776","823082749477164","608336433358884","231795228250656","35239767679440"],["68890500","3578369400","79631119440","991906991568","7621259332104","37590463019808","120103336162656","244955127421008","306733198596948","220591027708776","82511266065264","12385058192352"],["22963500","1084533300","21861120780","248039103636","1752737059044","8040368585052","24172302655332","46929248256060","56584742567616","39626400736224","14554612930752","2157157282752"],["3280500","133844400","2389122540","24478881048","158758432812","677829612096","1920476844756","3554511242040","4131107720928","2818354917312","1016591363136","148769467776"]]},"deriv_order":0},{"coeff":{"coeffs":[["1093500","38053800","-179902620","-26060449464","-489927663432","-4426818499440","-22688325938808","-69819332581872","-130877586055188","-147460503083832","-96051870436140","-33085709760600","-4649045868000"],["3280500","84636900","-1124292960","-64555201152","-970543063368","-7541007489576","-34632598462704","-98358887703600","-173997429085260","-188216621965980","-119195337327696","-40260737216880","-5578855041600"],["3280500","55112400","-1443157560","-49653595512","-613070337600","-4168210805784","-17355481313400","-45822258778824","-76816873624500","-79948092110040","-49273687472976","-16327449088416","-2231542016640"],["1093500","8529300","-498767220","-11956005324","-124323890364","-750685921668","-2861293224348","-7065650521188","-11265384281328","-11302347065760","-6785540724672","-2206747105344","-297538935552"]]},"deriv_order":1},{"coeff":{"coeffs":[["-1822500","-130126500","-3930695100","-66004578540","-683784113256","-4601866661784","-20647388425464","-62303298567768","-125728968641076","-166448182134420","-139915446013836","-71122653370620","-19835929036800","-2324522934000"],["-5467500","-341172000","-9016782300","-133514512920","-1236717059688","-7562958128640","-31331393258904","-88591988478096","-169766452971612","-215969187368448","-176275805934348","-87708899345688","-24082057596240","-2789427520800"],["-5467500","-291964500","-6684346800","-87350004720","-727554066408","-4069949490648","-15659899671024","-41681852966160","-76090589347788","-93209064981300","-73954955425536","-36039403568736","-9744400139328","-1115771008320"],["-1822500","-80919000","-1598259600","-18511467840","-139546013976","-718567753392","-2581349237424","-6493511769408","-11324559173796","-13382479415736","-10332590535072","-4934187347904","-1314130298688","-148769467776"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["45927000","1952553600","36128540160","426190172832","3819700301040","26466833185056","132401459110464","447142706176608","968736839960952","1276429636062432","952174183588992","365229043390080","55788550416000"],["55768500","2393452800","54202258080","816868749456","8410836106152","58655551316688","274472933626368","850417015542768","1701743809184964","2105214009829488","1502522034715008","559298814103872","83682825624000"],["26244000","1769501700","49481881020","769443663204","7450324523100","47320176255660","201265594519284","572682613619052","1067960392800372","1251076839262272","859156073862048","311448880789056","45746611341120"],["19683000","1039262400","23971532040","318890109168","2715030032328","15497584835040","60326593139448","159601400274672","280711455752448","314349885410688","209021102225280","74087194952448","10711401679872"],["3280500","153527400","3192188940","38813616288","305631719100","1630380208968","5987454517332","15077372310576","25458175173168","27605001242880","17926720867008","6248317646592","892616806656"]]},"deriv_order":0},{"coeff":{"coeffs":[["-4374000","-552436200","-20884450320","-388104040224","-4235156782848","-29482756608528","-136315075665024","-425194158864384","-892862689526352","-1240503531463368","-1104045081519600","-597867298624800","-178151437661760","-22315420166400"],["-25150500","-1655996400","-43611229440","-634703056848","-5789678394888","-35152067159856","-146121922247616","-419385950893296","-825537790069236","-1091919681148320","-937202189651424","-494360941419648","-144529537944384","-17852336133120"],["-20776500","-955937700","-19626706620","-237086222724","-1870612090020","-10119442304556","-38341599603444","-102155551100172","-189553997494008","-239484405742560","-198590709540096","-102130239628224","-29307585151872","-3570467226624"]]},"deriv_order":1},{"coeff":{"coeffs":[["-1822500","-124659000","-3687938100","-62538402240","-679268045736","-4994420162256","-25569714010248","-92193449343840","-233772794613396","-411522635066040","-490696976715012","-381787911650592","-183445151223456","-49093924366080","-5578855041600"],["-3645000","-216513000","-5624089200","-84970723680","-834436063152","-5623515926064","-26719731076608","-90427500661536","-217454471429832","-366501734045352","-422139563542224","-319846090747968","-150653881034496","-39721447896192","-4463084033280"],["-1822500","-91854000","-2083773600","-28101025440","-250614821016","-1555843837248","-6892755757776","-21981607193952","-50285629790244","-81329834458512","-90627467029488","-66929730558336","-30919254386112","-8033551259904","-892616806656"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["108","-810"],["36","-999"],["-27","-405"],["-9","-54"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-48","162","270"],["-3","81","108"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["5","93","279","135"],["5","48","117","54"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["-81000","-4787100","-115444440","-1450882044","-10115644824","-38781729828","-73262802888","-35105575284","73177299936","83287433520","22958251200"],["-162000","-8116200","-165351780","-1759843908","-10476657288","-33501568248","-41594351796","47617822188","183300378192","149955644088","37498476960"],["-81000","-3329100","-56249640","-499624524","-2352459672","-3941875044","13522221000","78554774268","140912644032","97547058432","22805196192"],["0","0","291600","12815820","231577056","2147966424","10912255200","30311268876","43306064208","27371337264","6122200320"],["0","0","72900","2711880","40573224","317447424","1402295652","3499007544","4634165520","2806008480","612220032"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","-81000","-4665600","-103488840","-1149294744","-6995180736","-23407023600","-38196199944","-11729965752","42868156824","43365585600","11479125600"],["0","-162000","-7508700","-135973080","-1277347968","-6694293276","-18536740812","-17255534976","35748264600","101384062452","77420324880","18749238480"],["0","-81000","-2843100","-42107040","-329213484","-1315795428","-1259948196","10875881016","46914902892","75849385284","50048987616","11402598096"],["0","0","0","291600","11722320","184337856","1492128864","6750481680","17127989136","22941245088","13979024064","3061100160"],["0","0","0","72900","2274480","29550744","206277840","831646116","1933028064","2431874016","1428513408","306110016"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["19683000","1098311400","23723526240","250823145888","1383081579792","4149244739376","6772224938976","5764816876320","2402007031800","387420489000"],["59049000","2763493200","49487785920","437176121184","2106419547600","5746909440384","8799438519936","7202921731488","2928898896840","464904586800"],["59049000","2232052200","32587962120","245283404904","1050225201144","2632048708824","3800164529880","2997084902904","1190155742208","185961834720"],["19683000","566870400","6823702440","44581522608","171919037736","399014405856","545602839768","415314764208","161166923424","24794911296"]]},"step_quotients":[[{"coeff":{"coeffs":[["39366000","1369936800","1317973680","-494741810304","-7768408967712","-49790936872512","-160723829175840","-272903813684352","-237318294741840","-100109454357600","-16271660538000"],["101695500","1413239400","-76949113860","-2279062762272","-24456170802600","-130915983730320","-380862273225960","-607160798710560","-509082403440996","-210080051561880","-33666840494100"],["49207500","-3779136000","-205933387500","-3548665391040","-29930455261512","-139190367045312","-370380071420568","-557667859938624","-451777230950724","-182515342049856","-28847329610940"],["-72171000","-7294519800","-202344389280","-2613621169296","-18534723383232","-76888101598848","-189323917553232","-270618319777392","-212231010116808","-83999993864328","-13097911892112"],["-85293000","-4562519400","-93413156040","-996023887848","-6184438438392","-23331207990744","-53668853346456","-73159337230200","-55643913433440","-21592235253600","-3322518113664"],["-29524500","-1204599600","-20439220860","-189698927832","-1060345963548","-3693064288032","-8000663565060","-10443823262136","-7717416140880","-2938196988576","-446308403328"],["-3280500","-114161400","-1704154140","-14253956208","-73234695564","-238421438712","-489948212484","-614821967136","-442175918112","-165299408640","-24794911296"]]},"deriv_order":0},{"coeff":{"coeffs":[["-18589500","-948720600","-17325370260","-122444478792","-11474874072","4060897987536","21957182165592","54075176128944","71078688319572","50796852648840","18557441423100","2711943423000"],["-56862000","-2375738100","-33520542660","-147001776912","671154713136","9457239183624","40909244040360","91159639292304","113301265497120","78272541541836","27979507715580","4029173085600"],["-59049000","-1907282700","-18805925520","-13915251144","977728145688","7671882276000","27951096879720","56987315502408","67204540825200","44933028314220","15723073125576","2231542016640"],["-21870000","-482233500","-2100176100","32289174180","460769975820","2628539072460","8321109733476","15653911393836","17565759762516","11378109294720","3898999801296","545488048512"],["-1093500","-1968300","510577020","8892543204","70968631140","324874134828","912048415380","1593360028908","1705224107880","1071002418480","359526213792","49589822592"]]},"deriv_order":1},{"coeff":{"coeffs":[["3645000","254785500","7405400700","116516667780","1088869937292","6302160414360","23108734033560","54019170750600","79682732989920","72321762830796","38803175243820","11248108197300","1355971711500"],["12757500","785133000","20028764700","277360238880","2307692079432","12124272299184","41175313165656","90753303755232","128162505004524","112786885878984","59216274715788","16901864533440","2014586542800"],["16402500","875893500","19462550400","237603728160","1775365816824","8543670846984","27060661106928","56501863280784","76612315606308","65473546080348","33665290812144","9465457387248","1115771008320"],["9112500","415530000","8017542000","86872888800","588380769720","2614882455936","7771920729840","15437791345248","20151930232692","16749651327984","8441289801216","2338986632256","272744024256"],["1822500","69984000","1178355600","11441334240","70898008536","293179702176","822271024368","1559885623200","1965245434596","1591006808160","786549686112","214889231232","24794911296"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["-111537000","-4275147600","-64023287760","-584545419072","-4779576280656","-32825299419072","-148761049750560","-401155492362912","-613905818121864","-503148671231472","-204836960944080","-32543321076000"],["-167305500","-5546669400","-93885548040","-1284029480448","-13153628166552","-86753517231168","-350628743539440","-853079713516944","-1211023931614380","-945792593294184","-373352476203432","-58113073350000"],["-68890500","-3381539400","-96784853940","-1578564711468","-15033001238604","-87061623339564","-313048209963276","-695698777902708","-925471441618272","-692656694827452","-265956417288720","-40632660886320"],["-36085500","-2751683400","-72840484440","-992558892528","-8011638884592","-40631844592944","-131903226795672","-271477417537296","-341692646029236","-246435590249640","-92330050938480","-13872752870112"],["-26244000","-1218377700","-24250243320","-272517984684","-1911495491856","-8718198197148","-26092779500088","-50483759498100","-60715850288544","-42444755653536","-15571204293888","-2305926750528"],["-3280500","-133844400","-2389122540","-24478881048","-158758432812","-677829612096","-1920476844756","-3554511242040","-4131107720928","-2818354917312","-1016591363136","-148769467776"]]},"deriv_order":0},{"coeff":{"coeffs":[["-7654500","265064400","23414503140","523721642328","5782765410360","36967767222816","145981098885672","364616134610544","574790181079212","559552961944656","322754843779380","100589855763960","13017328430400"],["21870000","2404606500","76448772000","1170601547760","10307203244208","56533286324232","200230719459984","462358822851936","689052880740960","645006040923060","362078023412880","110715477664464","14133099438720"],["50301000","2823198300","62801760780","760844239236","5671023208524","27502095133404","88811692564788","191344836746988","270948057660252","244516050866808","133758215228880","40155358843872","5058161904384"],["20776500","831278700","14639034420","149252016204","975099992796","4268842347780","12728545516764","25784277999588","34848329496480","30394428763680","16224136958016","4785417880128","595077871104"]]},"deriv_order":1},{"coeff":{"coeffs":[["3645000","243850500","6936289200","110509416180","1096023133152","7122852704664","31091186178432","91833961393800","182317786298280","238437911257236","198674047991952","100358953152516","27863281568880","3254332107600"],["9112500","535815000","13473013500","191747849400","1721753103960","10276257789072","41771326372920","116379890455536","220493512536804","278108564022648","225579109551372","111735168391512","30578324355792","3533274859680"],["7290000","372883500","8282606400","105861472560","867100080384","4788517244040","18241248908448","48175364735568","87415148521584","106591544397036","84287545960608","40973590916640","11058530438016","1264540476096"],["1822500","80919000","1598259600","18511467840","139546013976","718567753392","2581349237424","6493511769408","11324559173796","13382479415736","10332590535072","4934187347904","1314130298688","148769467776"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["72900","2711880","33356124","155259504","300205116","219662280","53144100"],["145800","4111560","37581408","147071376","257453640","179981352","42515280"],["72900","1399680","10130184","34327152","55033668","36846576","8503056"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-3","-3"]]},"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":[["13","33","18"],["34","132","153","54"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["-1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","3"]]},"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 = 3 != 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of f(n) a_n = 3 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":["3"]},"numerator":["3"],"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/9 (exact)","name":"first_coefficient_positive","statement":"beta_2 = c_2 L_0 / (a_2 L_1) > 0","status":{"kind":"verified"}},{"evidence":"beta_n = 1/9 > 0 for every integer n in [3, +inf) (exact; Taylor shift: the coefficients of beta_n = 1/9 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/9"]},"numerator":["1/9"],"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) = 1/2 ((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/18"]},"numerator":["5/18"],"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 = 3, b_n = 3, c_n = 1","recurrence":{"first_index":0,"initial_polynomials":[["13","33","18"],["34","132","153","54"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["-1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","3"]]},"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 = 3, 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 = 3, 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"}