Simultaneous Dirichlet approximation ⟹ RecordsContinue (makes g_∞ ≤ 2^d+1 unconditional)

The higher-dimensional three-distance bound g_∞ ≤ 2^d+1 (DeltaCost, TorusReduction) was proved under the hypothesis RecordsContinue (deltaCost α) — the best simultaneous approximations of α improve without bound. This file discharges that hypothesis from a clean, standard irrationality condition (some coordinate α k is irrational), via the elementary box pigeonhole form of Dirichlet's simultaneous approximation theorem — no homogeneous dynamics, no measure theory.

• exists_delta_lt (Dirichlet): for every ε > 0 there is a denominator q ≥ 1 with the defect delta α q < ε. Proof: among the Q^d + 1 points {i • α mod ℤᵈ : 0 ≤ i ≤ Q^d} two share one of the Q^d sub-boxes of side 1/Q (Fintype pigeonhole); their index difference q has all coordinates within 1/Q of an integer, so delta α q < 1/Q ≤ ε.
• delta_pos: delta α q > 0 for q ≥ 1 when some α k is irrational (q α k ∉ ℤ).
• recordsContinue_deltaCost: assembling the two — for every q ≥ 1 there is q' > q with delta α q' < delta α q. (If not, delta α would be bounded below by a positive constant on all of ℕ₊, contradicting Dirichlet.) This is exactly RecordsContinue (deltaCost α).

Hence the L^∞ higher-dimensional three-distance theorem holds for every α with an irrational coordinate, with no remaining hypothesis (nnDist_count_unconditional, nnDist_count_plane_unconditional). Axiom-clean.

Dirichlet via the box pigeonhole

noncomputable def ThreeGap.SimDirichlet.box {d : ℕ} (α : Fin d → ℝ) (Q : ℕ) (hQ : 1 ≤ Q) (i : ℕ) : Fin d → Fin Q

The box index of the point i • α in direction k, at resolution Q: ⌊{i αₖ}·Q⌋ ∈ {0,…,Q−1}, packaged as Fin Q.

Equations

• ThreeGap.SimDirichlet.box α Q hQ i k = ⟨⌊Int.fract (↑i * α k) * ↑Q⌋.toNat, ⋯⟩

theorem ThreeGap.SimDirichlet.exists_delta_lt_inv {d : ℕ} (α : Fin d → ℝ) (Q : ℕ) (hQ : 1 ≤ Q) : ∃ (q : ℕ), 1 ≤ q ∧ SimApprox.delta α ↑q < 1 / ↑Q

Dirichlet's simultaneous approximation theorem (inverse-resolution form). For Q ≥ 1 there is a denominator 1 ≤ q with delta α q < 1/Q.

theorem ThreeGap.SimDirichlet.exists_delta_lt {d : ℕ} (α : Fin d → ℝ) {ε : ℝ} (hε : 0 < ε) : ∃ (q : ℕ), 1 ≤ q ∧ SimApprox.delta α ↑q < ε

Dirichlet's theorem (ε form). For every ε > 0 there is q ≥ 1 with delta α q < ε.

Positivity from irrationality

theorem ThreeGap.SimDirichlet.delta_pos {d : ℕ} (α : Fin d → ℝ) {k₀ : Fin d} (hirr : Irrational (α k₀)) {q : ℕ} (hq : 1 ≤ q) : 0 < SimApprox.delta α ↑q

If some coordinate α k is irrational, the defect is strictly positive at every q ≥ 1 (then q αₖ ∉ ℤ, so its distance to the nearest integer is positive).

Assembly: RecordsContinue

theorem ThreeGap.SimDirichlet.recordsContinue_deltaCost {d : ℕ} (α : Fin d → ℝ) {k₀ : Fin d} (hirr : Irrational (α k₀)) : Chevallier.RecordsContinue (DeltaCost.deltaCost α)

RecordsContinue (deltaCost α) from irrationality. If some coordinate of α is irrational, the best simultaneous approximations improve without bound: every q ≥ 1 is beaten by a larger denominator. (Else delta α would have a positive lower bound on all of ℕ₊, contradicting Dirichlet.)

Unconditional higher-dimensional three-distance bounds

theorem ThreeGap.SimDirichlet.nnDist_count_unconditional {d : ℕ} (α : Fin d → ℝ) {k₀ : Fin d} (hirr : Irrational (α k₀)) {N : ℕ} (hN : 2 ≤ N) : (Finset.image (DeltaCost.nnDist α N) (Finset.range (N + 1))).card ≤ 2 ^ d + 1

g_∞ ≤ 2^d + 1, unconditional. For any α : Fin d → ℝ with an irrational coordinate and any N ≥ 2, the orbit {0, α, …, Nα} on the torus 𝕋ᵈ has at most 2^d + 1 distinct nearest-neighbour distances in the sup-norm metric. No RecordsContinue hypothesis — it is discharged from irrationality via Dirichlet.

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

The L^∞ five-distance theorem on 𝕋², unconditional. For any α : Fin 2 → ℝ with an irrational coordinate and any N ≥ 2, the orbit {0, α, …, Nα} on 𝕋² has at most five distinct nearest-neighbour distances in the sup-norm metric.