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

Chevallier's count (ChevallierCount) and the unconditional sup-norm growth (DeltaCost) bound the number of distinct values of the abstract quantity gapVal (delta α) N q. This file identifies that quantity with the actual geometric nearest-neighbour distance in the torus 𝕋ᵈ = ℝᵈ/ℤᵈ, closing the gap between the combinatorial bound and the genuine higher-dimensional three-distance statement.

The torus distance between two orbit points iα and jα is, by translation invariance,

d_𝕋(iα, jα) = inf_{p ∈ ℤᵈ} ‖(i−j)•α − p‖_∞ = delta α (i − j),

so the nearest-neighbour distance of the q-th point among {0, α, …, Nα} is min_{0 ≤ j ≤ N, j ≠ q} delta α (q − j). Using the symmetry delta α (−t) = delta α t and the offset bookkeeping (|q − j| ranges over [1, max(q, N−q)]), this equals exactly min_{1 ≤ t ≤ max(q, N−q)} delta α t = gapVal (delta α) N q.

Hence gapVal = nnDist, and the bound gap_count_supNorm_le becomes a bound on the number of distinct actual nearest-neighbour distances: g_∞ ≤ 2^d + 1.

Axiom-clean; elementary.

Symmetry of the defect

theorem ThreeGap.DeltaCost.rem_neg_neg {d : ℕ} (α : Fin d → ℝ) (q : ℤ) (p : Fin d → ℤ) : SimApprox.rem α (-q) (-p) = -SimApprox.rem α q p

Negating both the denominator and the integer translate negates the remainder vector.

theorem ThreeGap.DeltaCost.delta_neg_le {d : ℕ} (α : Fin d → ℝ) (q : ℤ) : SimApprox.delta α (-q) ≤ SimApprox.delta α q

One inequality of the symmetry delta α (−q) ≤ delta α q.

theorem ThreeGap.DeltaCost.delta_neg_eq {d : ℕ} (α : Fin d → ℝ) (q : ℤ) : SimApprox.delta α (-q) = SimApprox.delta α q

The defect is symmetric: delta α (−q) = delta α q. (The torus distance to the origin is unchanged by reflection.)

The torus nearest-neighbour distance

noncomputable def ThreeGap.DeltaCost.nnDist {d : ℕ} (α : Fin d → ℝ) (N q : ℕ) : ℝ

The nearest-neighbour distance of the q-th orbit point qα among {0, α, …, Nα}, using the torus distance d_𝕋(qα, jα) = delta α (q − j): the minimum over the other N points.

Equations

• ThreeGap.DeltaCost.nnDist α N q = if h : ((Finset.range (N + 1)).erase q).Nonempty then ((Finset.range (N + 1)).erase q).inf' h fun (j : ℕ) => ThreeGap.SimApprox.delta α (↑q - ↑j) else 0

theorem ThreeGap.DeltaCost.gapVal_eq_nnDist {d : ℕ} (α : Fin d → ℝ) {N : ℕ} (hN : 2 ≤ N) {q : ℕ} (hq : q ≤ N) : Chevallier.gapVal (deltaCost α) N q = nnDist α N q

The isometry reduction. For q ≤ N (N ≥ 2), the abstract gap value of the defect cost equals the genuine torus nearest-neighbour distance:

gapVal (delta α) N q = nnDist α N q.

Proof: each side is an infimum; the offset map j ↦ |q − j| is a value-preserving correspondence between {0,…,N}\{q} and [1, max(q, N−q)] (using delta α (−t) = delta α t), so the two infima agree.

theorem ThreeGap.DeltaCost.nnDist_count_le {d : ℕ} (α : Fin d → ℝ) (hr : Chevallier.RecordsContinue (deltaCost α)) {N : ℕ} (hN : 2 ≤ N) : (Finset.image (nnDist α N) (Finset.range (N + 1))).card ≤ 2 ^ d + 1

g_∞ ≤ 2^d + 1 for the actual torus nearest-neighbour distances (combinatorial three-distance bound in L^∞). For every N ≥ 2, the number of distinct nearest-neighbour distances {nnDist α N q : 0 ≤ q ≤ N} of the orbit {0, α, …, Nα} on the torus 𝕋ᵈ is at most 2^d + 1. The only hypothesis is RecordsContinue (the best approximations of α improve without bound — the appropriate irrationality). The growth geometry is fully discharged (orthant pigeonhole), and the geometric identification gapVal = nnDist is now proven.

theorem ThreeGap.DeltaCost.nnDist_count_le_plane (α : Fin 2 → ℝ) (hr : Chevallier.RecordsContinue (deltaCost α)) {N : ℕ} (hN : 2 ≤ N) : (Finset.image (nnDist α N) (Finset.range (N + 1))).card ≤ 5

The L^∞ five-distance theorem on 𝕋² (the d = 2 instance of nnDist_count_le). For every N ≥ 2, the orbit {0, α, …, Nα} on the two-dimensional torus has at most five distinct nearest-neighbour distances in the sup-norm metric. This is the sharp g_∞ ≤ 5 bound for d = 2 (2² + 1 = 5), fully discharged modulo RecordsContinue (irrationality): the growth geometry is the orthant pigeonhole and the geometric identification gapVal = nnDist is proven.

NB: this is the sup-norm (L^∞) five-distance theorem. The Euclidean five-distance bound g₂ ≤ 5 (Haynes–Marklof) is a distinct statement requiring Romanov's sharper growth constant K = 4; the contact-number route gives only the Euclidean g₂ ≤ 7.