middle initial roots 1
ProvedFreiman.middle_initial_roots_1continued-fractionsformalizationlagrange-spectrum
Exact regularity, strict width ratio<19/5 and rational inner endpoint bounds for roots 1–5. The roots are the physical p.51 cores converted to outward left-word order; all constants are exact rationals.
Preamble
import Definitions.Def_Freiman_middleRoots
Formal statement
namespace Freiman
theorem middle_initial_roots_1 :
∀ i : Fin 15, 0 ≤ i.val → i.val<5 → middleRootCertificate i := by
sorry
end FreimanSource
Freiman's Hall ray: Proof report and corrected English text, 8 September 2026, Part III, active source staging/m2b/m2b_body.tex, m2b:sec:initial, roots table rows 1–5