middle small digit centers
ProvedFreiman.middle_small_digit_centerscontinued-fractionsformalizationlagrange-spectrum
Every root completion avoids 314 and 413. At a digit 3 each tail is ≤beta by first-deviation comparison; centers≤2 have value<4. This proves the closed sqrt21 bound for all small-digit positions.
Preamble
import Definitions.Def_Freiman_middleRoots
Formal statement
namespace Freiman
theorem middle_small_digit_centers :
∀ (r : Fin 15) (a : ℤ→ℕ+) (i : ℤ), middleCompatible (middleRoot r) a → (a i:ℕ) ≤ 3 → localValue a i ≤ Real.sqrt 21 := 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:centers