The Lagrange spectrum describes the asymptotic quality of rational approximation to irrational real numbers. The Markov spectrum is defined through minima of indefinite binary quadratic forms. Freiman determined the exact starting point of the maximal half-line contained in each spectrum.
This mission aims to formalize his theorem that this half-line is , where
The formalization must establish membership of every real number at least , including the endpoint, and show that no half-line starting below is contained in either spectrum.
The sources are Freiman's Russian monograph and an accompanying detailed reconstruction of its proof, with an English translation, exact computational certificates, and verification scripts. The project follows Freiman's continued fraction construction, incorporating the corrections and supplementary arguments established in the report.
The intended result is a complete Lean 4 proof. Its scope includes the equivalence of the classical and continued fraction definitions of the spectra, the infinite constructions that realize spectral values, and the exact finite calculations used in the argument.
Start with README.md and PROOF_GUIDE.md in the package. The files formalization/MISSION.md and formalization/MILESTONES.md describe the scope and proposed stages of the formalization. For reproducing the report, use the PDF and sources contained in the ZIP.
References to the report in the individual source fields use its printed page numbers.
namespace Freiman
theorem maximal_hall_ray :
(∀ d : ℝ, Set.Ici d ⊆ lagrangeSpectrum ↔ cF ≤ d) ∧
(∀ d : ℝ, Set.Ici d ⊆ markovSpectrum ↔ cF ≤ d) := by
sorry
end Freiman
Let and be the classical Lagrange and Markov spectra, and let
For every real number ,
and
Thus is the maximal half line contained in each spectrum. Its endpoint is included, and no half line starting below is contained in either spectrum.
No open leaves. Every sub-goal is proved or awaiting decomposition.