The sharp Euclidean five-distance theorem g₂ ≤ 5

The capstone of the Haynes–Marklof route: the number of distinct Euclidean nearest-neighbour distances among the first N points of a Kronecker sequence on 𝕋² is at most 5 (Haynes–Marklof, IMRN 2022). This sharpens the unconditional g₂ ≤ 6 (nnDistE_count_le). The single sharpening is the record-denominator growth 2 qₙ ≤ qₙ₊₄ (euclidean_growth_four, the K = 4 HM Theorem 8 bound) replacing 2 qₙ ≤ qₙ₊₅; feeding it through Chevallier's count (chevallier_gap_count_le with K = 4) yields ≤ 4 + 1 = 5 distances. Axiom-clean.

theorem ThreeGap.EuclideanRecords.bestDenom_euclidean_growth_four (α : Fin 2 → ℝ) {k₀ : Fin 2} (hirr : Irrational (α k₀)) (hr : Chevallier.RecordsContinue (deltaE α)) (k : ℕ) : 2 * Chevallier.bestDenom (deltaE α) hr k ≤ Chevallier.bestDenom (deltaE α) hr (k + 4)

The sharp Euclidean growth 2 qₖ ≤ qₖ₊₄ for the record denominators (Haynes–Marklof).

theorem ThreeGap.EuclideanRecords.gap_count_euclidean_five (α : Fin 2 → ℝ) {k₀ : Fin 2} (hirr : Irrational (α k₀)) {N : ℕ} (hN : 2 ≤ N) : (Finset.image (Chevallier.gapVal (deltaE α) N) (Finset.range (N + 1))).card ≤ 5

g₂ ≤ 5 (sharp Euclidean five-distance count, gapVal form).

theorem ThreeGap.EuclideanRecords.nnDistE_count_le_five (α : Fin 2 → ℝ) {k₀ : Fin 2} (hirr : Irrational (α k₀)) {N : ℕ} (hN : 2 ≤ N) : (Finset.image (nnDistE α N) (Finset.range (N + 1))).card ≤ 5

The sharp Euclidean five-distance theorem g₂ ≤ 5. For any α : Fin 2 → ℝ with an irrational coordinate and N ≥ 2, the number of distinct values of the Euclidean nearest-neighbour distance nnDistE α N q over q ∈ {0, …, N} is at most 5.