{"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":[["13","44","32"],["34","176","272","128"]],"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 u(n,x) jointly generated with A207607; see the Formula section."},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["128","-896","-1536"],["-16","-672","-896"],["-12","-112","-128"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-120","-576","-384"],["-5","-64","-208","-128"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["-32","320"],["0","288"],["8","64"]]},"deriv_order":1,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["44","64"]],"recurrence":{"denominator":{"coeffs":[["-24","96"],["-16","160"],["8","64"]]},"terms":[{"coeff":{"coeffs":[["-132","336","768"],["-8","448","640"],["12","112","128"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-5","56","368","256"],["5","64","208","128"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["1"],"operator":{"coefficients":[{"denominator":["1"],"numerator":["0"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["13","44","32"],["34","176","272","128"]],"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":[["-240","384","6144"],["32","896","5120"],["16","256","1024"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["4","-112","-1408","-2048"]]},"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":[["-800","-31680","-253952","2468864","29974528","93962240","98304000","32768000"],["-1600","-36960","225536","9362944","65675264","174678016","172032000","55705600"],["-600","13440","790656","9993216","52131840","121110528","112558080","35389440"],["400","25440","487936","4201472","17920000","37117952","32636928","9961472"],["200","6720","90368","618496","2263040","4243456","3538944","1048576"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["110592000","8228044800","236967690240","3340536643584","24560384606208","98241538424832","213794345189376","242654914805760","134808286003200","28991029248000"],["331776000","20702822400","494319697920","5822440538112","37405222502400","136069395775488","277792042254336","303188183875584","164379135836160","34789235097600"],["331776000","16721510400","325512069120","3266756739072","18649612025856","62318935277568","119968502906880","126154463772672","66795331387392","13915694039040"],["110592000","4246732800","68160061440","593749868544","3052891275264","9447451656192","17224295251968","17481590636544","9045201125376","1855425871872"]]},"step_quotients":[[{"coeff":{"coeffs":[["110592000","10439884800","415684362240","9133080182784","121702981828608","1017037920927744","5322354343280640","17093458736971776","32353582766358528","33784985844449280","17835281193369600","3710851743744000"],["405504000","34445721600","1237757460480","24675706994688","300188669313024","2304586303930368","11204295949025280","33908700229926912","61397646270529536","62245208674271232","32227201206190080","6617685609676800"],["571392000","43691212800","1422985789440","25871247212544","288421255839744","2045021465346048","9286887256621056","26597075680493568","46194025757147136","45522371255205888","23127265017593856","4688042702929920"],["387072000","26807500800","795413053440","13210509901824","135336239824896","890028221792256","3791577264685056","10310746525138944","17214844176433152","16507028197343232","8232524593496064","1647618174222336"],["129024000","8124825600","218364641280","3303457947648","31124625555456","190371556491264","763102475845632","1975364175790080","3175715998531584","2965279780896768","1452179982385152","286972534849536"],["18432000","1002700800","23864279040","326016958464","2819188850688","16048950607872","60628093894656","149617870110720","231850924572672","210900074102784","101429947662336","19791209299968"]]},"deriv_order":0},{"coeff":{"coeffs":[["4608000","213811200","-1347747840","-260310564864","-6525001138176","-78610232770560","-537190786400256","-2204146883100672","-5508950271197184","-8275953155309568","-7187649244692480","-3301111863705600","-618475290624000"],["13824000","475545600","-8422686720","-644823908352","-12925978804224","-133911149543424","-819994954825728","-3105120426393600","-7323967480135680","-10563316371947520","-8919496022556672","-4016997012602880","-742170348748800"],["13824000","309657600","-10811473920","-495975923712","-8165051596800","-74017948041216","-410925190348800","-1446576258023424","-3233405730816000","-4486941596712960","-3687195063877632","-1629063915503616","-296868139499520"],["4608000","47923200","-3736535040","-119425204224","-1655782244352","-13330475384832","-67746750529536","-223057583013888","-474186938056704","-634323719946240","-507768213602304","-220177203462144","-39582418599936"]]},"deriv_order":1},{"coeff":{"coeffs":[["-5760000","-548352000","-22085222400","-494476001280","-6830128889856","-61289017638912","-366650679361536","-1475153259134976","-3969174497918976","-7006201640386560","-7852500518436864","-5322173149347840","-1979120929996800","-309237645312000"],["-17280000","-1437696000","-50662195200","-1000229437440","-12353221951488","-100725707243520","-556374316548096","-2097589751119872","-5359406690598912","-9090659059236864","-9893159739850752","-6563337093513216","-2402776504074240","-371085174374400"],["-17280000","-1230336000","-37557043200","-654386135040","-7267334750208","-54204787851264","-278084217470976","-986899934085120","-2402126017855488","-3923392226918400","-4150587675377664","-2696861504765952","-972243156860928","-148434069749760"],["-5760000","-340992000","-8980070400","-138679418880","-1393886232576","-9570097299456","-45838894104576","-153746675859456","-357508312989696","-563300530126848","-579897894371328","-369229748502528","-131116761612288","-19791209299968"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["258048000","14627635200","360877916160","5676126437376","67829193768960","626654384750592","4179820296536064","18821304752799744","54368597283176448","95516396171034624","95002752442171392","48587418831421440","9895604649984000"],["313344000","17930649600","541411246080","10879298961408","149357328334848","1388785661116416","8664916131053568","35796083879706624","95507283324174336","157535088270114816","149913462644932608","74405051363229696","14843406974976000"],["147456000","13256294400","494260715520","10247677673472","132300826214400","1120398338949120","6353812281360384","24105579379163136","59937339136278528","93619223217045504","85721912231067648","41432896669483008","8114395812986880"],["110592000","7785676800","239444951040","4247072538624","48212761116672","366935833313280","1904467821723648","6718004234551296","15754421078065152","23523089203593216","20854986799841280","9856022231384064","1899956092796928"],["18432000","1150156800","31885885440","516931190784","5427324518400","38602461413376","189019698757632","634642621267968","1428793885458432","2065707470684160","1788630540484608","831230790598656","158329674399744"]]},"deriv_order":0},{"coeff":{"coeffs":[["-18432000","-3103948800","-156456714240","-3876663066624","-56405067300864","-523546732265472","-3227527799635968","-13423078470057984","-37582723702849536","-69621009698783232","-82616702415667200","-59651941780684800","-23699973136711680","-3958241859993600"],["-105984000","-9304473600","-326715310080","-6339871899648","-77108644675584","-624220799238144","-3459724200640512","-13239717457821696","-34748857841614848","-61282010718535680","-70131696342663168","-49324641377845248","-19227159834918912","-3166593487994880"],["-87552000","-5371084800","-147034275840","-2368188186624","-24913363599360","-179698290130944","-907812859281408","-3224978401001472","-7978780610002944","-13440627706429440","-14860724283113472","-10189998888321024","-3898868232093696","-633318697598976"]]},"deriv_order":1},{"coeff":{"coeffs":[["-5760000","-525312000","-20721254400","-468508999680","-6785019150336","-66517160951808","-454059991498752","-2182861427834880","-7380041566519296","-17321970861342720","-27539477404581888","-28569538337439744","-18303157750726656","-6531099068989440","-989560464998400"],["-11520000","-912384000","-31599820800","-636561653760","-8334949220352","-74895643901952","-474481680187392","-2141049115901952","-6864883660357632","-15426933579841536","-23691816993816576","-23934375271858176","-15031423463325696","-5284252883091456","-791648371998720"],["-5760000","-387072000","-11708006400","-210519982080","-2503321583616","-20721187160064","-122399672500224","-520457828696064","-1587481719865344","-3423367034044416","-5086302135386112","-5008412903473152","-3084954749632512","-1068725302198272","-158329674399744"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["192","-1920"],["64","-2368"],["-48","-960"],["-16","-128"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-64","288","640"],["-4","144","256"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["5","124","496","320"],["5","64","208","128"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["-6400","-234240","-2231296","1269760","81625088","287899648","310640640","104857600"],["-8800","-190080","109568","23203840","165158912","433291264","423100416","136314880"],["-800","69120","2096128","21241856","98099200","212074496","190316544","58720256"],["1600","53760","722944","4947968","18104320","33947648","28311552","8388608"]]},"deriv_order":0},{"coeff":{"coeffs":[["-800","-28480","-242432","1226752","28688384","157794304","364183552","335544320","104857600"],["-800","-11680","235648","6605824","59297792","251453440","514490368","448790528","136314880"],["200","17920","466688","5679104","36898816","130973696","241172480","199229440","58720256"],["200","8320","144128","1341440","7211008","22347776","37486592","29360128","8388608"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["110592000","8228044800","236967690240","3340536643584","24560384606208","98241538424832","213794345189376","242654914805760","134808286003200","28991029248000"],["331776000","20702822400","494319697920","5822440538112","37405222502400","136069395775488","277792042254336","303188183875584","164379135836160","34789235097600"],["331776000","16721510400","325512069120","3266756739072","18649612025856","62318935277568","119968502906880","126154463772672","66795331387392","13915694039040"],["110592000","4246732800","68160061440","593749868544","3052891275264","9447451656192","17224295251968","17481590636544","9045201125376","1855425871872"]]},"step_quotients":[[{"coeff":{"coeffs":[["221184000","10262937600","13164871680","-6589117366272","-137949282828288","-1178898461097984","-5073937461411840","-11487173500993536","-13319058657116160","-7491281957683200","-1623497637888000"],["571392000","10587340800","-768623247360","-30353230135296","-434285995622400","-3099693668106240","-12023552236584960","-25556848560046080","-28571326117576704","-15720482246492160","-3359093922201600"],["276480000","-28311552000","-2057011200000","-47262172446720","-531496842559488","-3295605984067584","-11692636549152768","-23473572525637632","-25355177296920576","-13657789842849792","-2878229383741440"],["-405504000","-54647193600","-2021161697280","-34808977686528","-329134551072768","-1820477186113536","-5976821996716032","-11390971602272256","-11911080330657792","-6285796306845696","-1306838289088512"],["-479232000","-34180300800","-933077975040","-13265339940864","-109821567172608","-552412284715008","-1694287691513856","-3079451285913600","-3122913670594560","-1615766696755200","-331502755774464"],["-165888000","-9024307200","-204161679360","-2526466277376","-18829333757952","-87440568090624","-252575282626560","-439605472002048","-433125976965120","-219867965816832","-44530220924928"],["-18432000","-855244800","-17022320640","-189838393344","-1300481703936","-5645096976384","-15467318083584","-25879325442048","-24816321036288","-12369505812480","-2473901162496"]]},"deriv_order":0},{"coeff":{"coeffs":[["-78336000","-5330534400","-129793720320","-1223063764992","-152825757696","72112316350464","519879518060544","1707115013996544","2991871802474496","2850881179484160","1388670300979200","270582939648000"],["-239616000","-13348454400","-251120517120","-1468359770112","8938636443648","167939068133376","968606896619520","2877845252603904","4769120948060160","4392904361508864","2093732132290560","402008938905600"],["-248832000","-10716364800","-140885360640","-138995564544","13021671849984","136235188224000","661797250007040","1799049191620608","2828799678873600","2521784679137280","1176571931000832","222651104624640"],["-92160000","-2709504000","-15733555200","322527559680","6136670453760","46676878295040","197018655916032","494182896500736","739384794021888","638575737569280","291765718351872","54425825574912"],["-4608000","-11059200","3825008640","88825135104","945181163520","5769026076672","21594541916160","50301247684608","71776956579840","60108067307520","26903675142144","4947802324992"]]},"deriv_order":1},{"coeff":{"coeffs":[["11520000","1073664000","41608396800","872889384960","10876418260992","83934031380480","410358581821440","1279010222899200","2515527448657920","3044195778428928","2177757798727680","841706215833600","135291469824000"],["40320000","3308544000","112534732800","2077855580160","23050892869632","161474634842112","731179955257344","2148763145601024","4045999517466624","4747469481050112","3323405965197312","1264781969326080","201004469452800"],["51840000","3691008000","109353369600","1780018053120","17733634228224","113787128512512","480535822467072","1337792856588288","2418596546347008","2755937974616064","1889403358150656","708308826587136","111325552312320"],["28800000","1751040000","45047808000","650811801600","5877171486720","34825775874048","138011643740160","365520104718336","636182165716992","705032840282112","473752072617984","175028507246592","27212912787456"],["5760000","294912000","6620774400","85713223680","708180443136","3904653754368","14601664069632","36933363302400","62041406570496","66969277562880","44143673868288","16080357556224","2473901162496"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["-626688000","-32027443200","-639510773760","-7785148317696","-84874409017344","-777203591675904","-4696280987074560","-16885593057263616","-34454350055079936","-37651074886139904","-20437515978670080","-4329327034368000"],["-940032000","-41553100800","-937796567040","-17101083377664","-233578533224448","-2054060324683776","-11069101115965440","-35908163198779392","-67966520650629120","-70774524097855488","-37251075991928832","-7730941132800000"],["-387072000","-25332940800","-966756925440","-21023790465024","-266951926480896","-2061355343413248","-9882710285746176","-29283623626604544","-51940405310128128","-51832133479563264","-26535682344222720","-5405474040053760"],["-202752000","-20614348800","-727583293440","-13219192111104","-142268493201408","-962038918545408","-4164091455209472","-11427133079420928","-19176879726526464","-18441000431124480","-9212189453844480","-1845530267222016"],["-147456000","-9127526400","-242228920320","-3629474906112","-33943814406144","-206420507099136","-823730569740288","-2124982045900800","-3407566923104256","-3176179854999552","-1553609930047488","-306763744149504"],["-18432000","-1002700800","-23864279040","-326016958464","-2819188850688","-16048950607872","-60628093894656","-149617870110720","-231850924572672","-210900074102784","-101429947662336","-19791209299968"]]},"deriv_order":0},{"coeff":{"coeffs":[["-32256000","1489305600","175410708480","5231309488128","77016575508480","656463504605184","3456389930287104","11510673146118144","24194291928662016","31403894630252544","24152039919452160","10036307778600960","1731730813747200"],["92160000","13510656000","572719104000","11692812533760","137274373177344","1003902644256768","4740856506482688","14596340591886336","29003881937633280","36199793625661440","27094629388124160","11046587165835264","1880164883496960"],["211968000","15862579200","470481960960","7599861006336","75528359903232","488374687236096","2102791677935616","6040620984434688","11404851057524736","13723019658657792","10009249484636160","4006482932662272","672901116198912"],["87552000","4670668800","109668925440","1490836783104","12986669334528","75804935454720","301373375643648","813991395852288","1466849443184640","1705832160952320","1214066995494912","477462924361728","79164837199872"]]},"deriv_order":1},{"coeff":{"coeffs":[["11520000","1027584000","38972620800","827885813760","10947869540352","94864253386752","552108784877568","2174349842841600","5755643394785280","10036421326798848","11150220431720448","7509952180518912","2780046431354880","432932703436800"],["28800000","2257920000","75700224000","1436486860800","17198111784960","136862232477696","741763794862080","2755523040509952","6960824035835904","11706253877182464","12660218190102528","8361244763357184","3050938608648192","470041220874240"],["23040000","1571328000","46537113600","793065553920","8661220982784","63774885150720","323923111575552","1140646609944576","2759634330845184","4486692757045248","4730485569748992","3066091253268480","1103359918473216","168225279049728"],["5760000","340992000","8980070400","138679418880","1393886232576","9570097299456","45838894104576","153746675859456","357508312989696","563300530126848","579897894371328","369229748502528","131116761612288","19791209299968"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["2400","119040","1952256","12115968","31236096","30474240","9830400"],["4800","180480","2199552","11476992","26787840","24969216","7864320"],["2400","61440","592896","2678784","5726208","5111808","1572864"]]},"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 = phi(n, D) = (1) D; 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 = 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":[["13","44","32"],["34","176","272","128"]],"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 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/16 (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":[["13","44","32"],["34","176","272","128"]],"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"}