The symbolic Lagrange spectrum is contained in the symbolic Markov spectrum

Every two-sided positive digit word whose one-sided local values have a finite limit superior realises its own supremum as a Markov value. Concretely, write

for a word $a:\mathbb Z\to\mathbb Z_{>0}$, where $[0;\cdots]$ is the continued fraction value defined earlier. Suppose $t\in\mathbb R$ has the property that the sequence $n\mapsto\lambda_n(a)$ indexed by $n\ge0$ has finite limit superior equal to $t$: for every $\varepsilon>0$ its terms are eventually at most $t+\varepsilon$, and after every index some term exceeds $t-\varepsilon$. Then there is a word $b:\mathbb Z\to\mathbb Z_{>0}$ such that

Equivalently, $t$ belongs to the symbolic Markov spectrum with its supremum already attained at a single position. This is the compactness half of the inclusion $L_{\mathrm{sym}}\subset M_{\mathrm{sym}}$: it recentres the word at positions where the local values approach their limit superior, and passes to a coordinatewise limit.

The argument needs the eventual boundedness of the digits (which the hypothesis supplies, since $a_i<\lambda_i(a)<t+1$ eventually), the continuity of each local value for coordinatewise convergence of words on a finite alphabet, and a diagonal subsequence over the countably many coordinates. The limit word is obtained from stabilised central blocks; no periodicity or boundedness assumption on the original word is imposed.

Formalization Note Lean states this as an inclusion between the two sets of platform definitions symbolicLagrangeSpectrum and symbolicMarkovSpectrum, whose membership conditions are written with HasFiniteLimsup (a real-valued finite limit superior) and with the explicit upper-bound-plus-approximation pair, so no supremum is ever applied to an unbounded set. The continued-fraction tails are cfValue of the two one-sided tails read outwards from the position in question.