{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"coefficients":[{"denominator":["1"],"numerator":["0"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_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":2,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["96","192","0"],["156","224","-128"],["48","-80","-256"],["-12","-112","-128"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["30","144","96","0"],["10","8","-160","-128"],["-5","-64","-208","-128"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["0","0"],["-36","0"],["-36","0"],["8","64"]]},"deriv_order":1,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0,1],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["0"],["8"]],"recurrence":{"denominator":{"coeffs":[["-8","-64"],["60","192"],["-60","-192"],["8","64"]]},"terms":[{"coeff":{"coeffs":[["0","0","0"],["-24","-48","0"],["-84","-256","-128"],["12","112","128"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-15","-72","-48","0"],["-20","-136","-256","-128"],["5","64","208","128"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":1,"multiplier":["1"],"operator":{"coefficients":[{"denominator":["1"],"numerator":["0"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_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":[["0","0","0","0","0","0","0","0"],["-8100","-77760","-238464","-248832","-82944","0","0","0"],["2700","112320","908928","2626560","2681856","884736","0","0"],["9000","129600","449280","-663552","-5363712","-6635520","-2359296","0"],["-6000","-153600","-1482240","-6696960","-14315520","-12779520","-3932160","0"],["800","26880","361472","2473984","9052160","16973824","14155776","4194304"]]},"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":[["-43200","-414720","-1271808","-1327104","-442368","0","0","0"],["36000","806400","5483520","14671872","14524416","4718592","0","0"],["24000","268800","-153600","-9928704","-34750464","-37355520","-12582912","0"],["-24000","-614400","-5928960","-26787840","-57262080","-51118080","-15728640","0"],["3200","107520","1445888","9895936","36208640","67895296","56623104","16777216"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0"],["2700","69120","667008","3013632","6441984","5750784","1769472","0","0"],["900","8640","-146304","-2552832","-13925376","-32440320","-30081024","-9437184","0"],["-2400","-80640","-1084416","-7421952","-27156480","-50921472","-42467328","-12582912","0"],["400","16640","288256","2682880","14422016","44695552","74973184","58720256","16777216"]]},"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":[["21600","207360","635904","663552","221184","0","0"],["-28800","-506880","-3059712","-7667712","-7372800","-2359296","0"],["9600","245760","2371584","10715136","22904832","20447232","6291456"]]},"start_base":1}},"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 = phi(n, D) = (1) D; so the candidate rows satisfy the input rule at every base n >= 1 (the exceptional bases checked exactly), and agreement on the 2 identifying rows gives Q_n = lambda(n) T_n(P_(n+0)) for every n >= 0"},"method":"operator_division"},"status":"certified"},"input_first_index":0,"interlacing":{"from_index":1,"justification":"the parent theorem (ThreeTermRecurrence) proves P_(m-1) strictly interlacing P_m for every m >= 1; T = phi(n, D) = (1) D 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.splits_add_C_mul_derivative_all","RealRooted.splits_C_mul_add_derivative","Polynomial.Splits.derivative"],"lift_summary":{"hypotheses":[{"evidence":"the polynomial with ascending coefficients [0, 1] is fixed; exact check: real-rooted = true, coefficients of one sign = true","name":"derivative_polynomial_real_rooted","statement":"the polynomial in D is real-rooted 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 = phi(n, D) = (1) D 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":"phi(n, D) = (1) D","kind":"preserver_image","operator":{"coefficients":[{"denominator":["1"],"numerator":["0"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_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 = phi(n, D) = (1) D, 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 differential operators: if phi is a real polynomial with only real roots, then phi(D) maps every real-rooted polynomial to a real-rooted polynomial or zero (write phi(D) = C D^j prod (1 + c_i D); D preserves real-rootedness by Rolle's theorem and p + c p' is real-rooted for every real c by Rolle's theorem applied to e^(x/c) p; Polya--Schur 1914); when the coefficients of phi have one sign, coefficients of one sign stay of one sign; applied to phi(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 = phi(n, D) = (1) D 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"}