middle initial roots 3
ProvedFreiman.middle_initial_roots_3continued-fractionsformalizationlagrange-spectrum
Exact regularity, strict width ratio<19/5 and rational inner endpoint bounds for roots 11–15. 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_3 :
∀ i : Fin 15, 10 ≤ i.val → i.val<15 → 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 11–15