The Euclidean isometry reduction: gapVal is the Euclidean nearest-neighbour distance

The combinatorial bound gap_count_euclidean (g₂ ≤ 6) counts distinct values of gapVal (deltaE α) N q. This file identifies that quantity with the genuine Euclidean torus nearest-neighbour distance, completing the Euclidean five-distance bound g₂ ≤ 6 as a statement about the actual orbit {0, α, …, Nα} on 𝕋².

The isometry reduction (TorusReduction.gapVal_eq_nnDist) used only the symmetry of the cost, so it is stated here generically for any symmetric c : ℤ → ℝ and instantiated at the Euclidean defect c = deltaN (euclNorm 2) α (symmetric by deltaN_neg). Axiom-clean.

noncomputable def ThreeGap.EuclideanRecords.nnDistC (c : ℤ → ℝ) (N q : ℕ) : ℝ

The nearest-neighbour distance for a symmetric cost c, abstractly: the minimum of c (q − j) over the other points j ∈ {0,…,N} ∖ {q}.

Equations

• ThreeGap.EuclideanRecords.nnDistC c N q = if h : ((Finset.range (N + 1)).erase q).Nonempty then ((Finset.range (N + 1)).erase q).inf' h fun (j : ℕ) => c (↑q - ↑j) else 0

theorem ThreeGap.EuclideanRecords.gapVal_eq_nnDistC (c : ℤ → ℝ) (hsymm : ∀ (t : ℤ), c (-t) = c t) {N : ℕ} (hN : 2 ≤ N) {q : ℕ} (hq : q ≤ N) : Chevallier.gapVal (fun (n : ℕ) => c ↑n) N q = nnDistC c N q

Generic isometry reduction. For a symmetric cost c, the gap value equals the nearest-neighbour distance, via the value-preserving offset bijection j ↦ |q − j|.

noncomputable def ThreeGap.EuclideanRecords.nnDistE (α : Fin 2 → ℝ) (N q : ℕ) : ℝ

The Euclidean torus nearest-neighbour distance of qα among {0, α, …, Nα}, via d_𝕋(iα, jα) = deltaN (euclNorm 2) α (i − j).

Equations

• ThreeGap.EuclideanRecords.nnDistE α N q = ThreeGap.EuclideanRecords.nnDistC (ThreeGap.SimApprox.deltaN (ThreeGap.SimApprox.euclNorm 2) α) N q

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

g₂ ≤ 6 for the actual Euclidean nearest-neighbour distances on 𝕋² (unconditional). For any α : Fin 2 → ℝ with an irrational coordinate and N ≥ 2, the orbit {0, α, …, Nα} has at most six distinct nearest-neighbour distances in the Euclidean metric. (The sharp ≤ 5 needs Romanov's K = 4.)