The symbolic Lagrange spectrum is contained in the symbolic Markov spectrum
ProvedFreiman.symbolic_lagrange_subset_markovcontinued-fractionslagrange-spectrummarkov-spectrumnumber-theory
Every finite symbolic Lagrange value is a finite symbolic Markov value. This is the inclusion in Theorem 1.3 which is separate from the existing server theorem stating equality of the classical and symbolic Lagrange spectra.
Preamble
import Definitions.Def_Freiman_symbolicMarkovSpectrum
Formal statement
namespace Freiman
theorem symbolic_lagrange_subset_markov :
symbolicLagrangeSpectrum ⊆ symbolicMarkovSpectrum := by
sorry
end FreimanSource
Freiman's Hall ray: Proof report and corrected English text, 8 September 2026, §1.2, Theorem 1.3, printed p. 8.