Arithmetic sharpness of the L∞ five-distance theorem g_∞ ≤ 5 on 𝕋² (dynamics-free)

nnDist_count_plane_unconditional proves the upper bound: any Kronecker orbit on 𝕋² has at most five distinct sup-norm nearest-neighbour distances (the d = 2 case of Shutov's 2^d + 1). This file shows the bound is sharp by an explicit, dynamics-free witness, mirroring the Euclidean EuclideanRecords.sharp_attained but with the L∞ (sup-norm) defect, which is integer-exact: delta α* d = max(|r(4d)|, |r(15d)|)/47 for balanced residues mod 47 — no square roots.

The witness

α* = (4/47, 15/47), N = 13. The scaled sup-norm defects M_d = max(|r(4d)|, |r(15d)|) for d = 1,…,13 are

[15, 17, 12, 16, 20, 23, 19, 21, 11, 9, 23, 8, 7],

with record minima at d = 1, 3, 9, 10, 12, 13 (values 15 > 12 > 11 > 9 > 8 > 7). The four records inside the doubling window (⌈13/2⌉, 13] = (7, 13] are 9, 10, 12, 13 — giving the five distinct distances 12/47 > 11/47 > 9/47 > 8/47 > 7/47, realized at q = 6, 4, 3, 1, 0 (cutoffs D = 7, 9, 10, 12, 13).

Method (cross-field reuse)

The minimax identity min_p max_k |dα_k − p_k| = max_k min_{p_k}|dα_k − p_k| (independent coordinates) makes the sup-norm defect exactly the max of two balanced residues — so every comparison is between integers, and the rational→irrational transport gap is linear (no √-gap): s ∈ (0, 1/1222) suffices. The combinatorial core (five_le_card_image_of_strictAnti_chain, inf_lt_inf) and the integer minimum (sq_residue_le) are reused verbatim from the Euclidean development.

noncomputable def ThreeGap.LinftyRecords.astar : Fin 2 → ℝ

The L∞ rational witness α* = (4/47, 15/47).

Equations

• ThreeGap.LinftyRecords.astar = ![4 / 47, 15 / 47]

theorem ThreeGap.LinftyRecords.abs_residue_le (m r a : ℤ) (hm : 0 < m) (h2r : 2 * |r| ≤ m) (hcong : m ∣ a - r) (k : ℤ) : |↑r| ≤ |↑a - ↑m * ↑k|

Per-coordinate integer minimum (L∞ crux). The balanced residue |r| lower-bounds |a − m·k| for every k — the absolute-value version of sq_residue_le.

theorem ThreeGap.LinftyRecords.delta_astar (d n₀ n₁ r₀ r₁ M : ℤ) (hr0 : 4 * d = r₀ + 47 * n₀) (hr1 : 15 * d = r₁ + 47 * n₁) (hb0 : 2 * |r₀| ≤ 47) (hb1 : 2 * |r₁| ≤ 47) (hM0 : |r₀| ≤ M) (hM1 : |r₁| ≤ M) (hMa : M = |r₀| ∨ M = |r₁|) : SimApprox.delta astar d = ↑M / 47

The witness defect is coordinatewise-exact. With α* = (4/47, 15/47), balanced residues 4d ≡ r₀, 15d ≡ r₁ (mod 47) give delta α* d = M/47, where M = max(|r₀|, |r₁|) (provided as M with |r₀| ≤ M, |r₁| ≤ M, M ∈ {|r₀|, |r₁|}). Upper bound at the rounding (n₀, n₁); lower bound coordinatewise via abs_residue_le and norm_le_pi_norm (the sup norm dominates each coordinate).

theorem ThreeGap.LinftyRecords.dstar1 : SimApprox.delta astar 1 = 15 / 47

The thirteen witness defects delta α* d = M_d/47, d = 1,…,13, with M_d = [15,17,12,16,20,23,19,21,11,9,23,8,7] — from delta_astar at the balanced residues of 4d, 15d mod 47.

theorem ThreeGap.LinftyRecords.dstar2 : SimApprox.delta astar 2 = 17 / 47

theorem ThreeGap.LinftyRecords.dstar3 : SimApprox.delta astar 3 = 12 / 47

theorem ThreeGap.LinftyRecords.dstar4 : SimApprox.delta astar 4 = 16 / 47

theorem ThreeGap.LinftyRecords.dstar5 : SimApprox.delta astar 5 = 20 / 47

theorem ThreeGap.LinftyRecords.dstar6 : SimApprox.delta astar 6 = 23 / 47

theorem ThreeGap.LinftyRecords.dstar7 : SimApprox.delta astar 7 = 19 / 47

theorem ThreeGap.LinftyRecords.dstar8 : SimApprox.delta astar 8 = 21 / 47

theorem ThreeGap.LinftyRecords.dstar9 : SimApprox.delta astar 9 = 11 / 47

theorem ThreeGap.LinftyRecords.dstar10 : SimApprox.delta astar 10 = 9 / 47

theorem ThreeGap.LinftyRecords.dstar11 : SimApprox.delta astar 11 = 23 / 47

theorem ThreeGap.LinftyRecords.dstar12 : SimApprox.delta astar 12 = 8 / 47

theorem ThreeGap.LinftyRecords.dstar13 : SimApprox.delta astar 13 = 7 / 47

nnDist as a prefix-minimum, and card ≥ 5 from the four record drops

theorem ThreeGap.LinftyRecords.nnDist_eq_inf (α : Fin 2 → ℝ) {q : ℕ} (hq : q ≤ 13) (hne : (Finset.Icc 1 (max q (13 - q))).Nonempty) : DeltaCost.nnDist α 13 q = (Finset.Icc 1 (max q (13 - q))).inf' hne fun (n : ℕ) => SimApprox.delta α ↑n

nnDist as a prefix-minimum of the L∞ defect. nnDist α 13 q is the infimum of delta α d over d ∈ [1, max(q, 13−q)] (via the repo's gapVal_eq_nnDist).

theorem ThreeGap.LinftyRecords.card_ge_five (α : Fin 2 → ℝ) (H1 : ∀ n ∈ Finset.Icc 1 7, SimApprox.delta α 9 < SimApprox.delta α ↑n) (H2 : ∀ n ∈ Finset.Icc 1 9, SimApprox.delta α 10 < SimApprox.delta α ↑n) (H3 : ∀ n ∈ Finset.Icc 1 10, SimApprox.delta α 12 < SimApprox.delta α ↑n) (H4 : ∀ n ∈ Finset.Icc 1 12, SimApprox.delta α 13 < SimApprox.delta α ↑n) : 5 ≤ (Finset.image (DeltaCost.nnDist α 13) (Finset.range 14)).card

card ≥ 5 from the four record drops. If the defect drops strictly below the whole preceding prefix at d = 9, 10, 12, 13, then the five nnDist α 13 q at q = 6, 4, 3, 1, 0 are strictly decreasing, so the image has ≥ 5 elements.

Rational → irrational upgrade by Lipschitz-openness

theorem ThreeGap.LinftyRecords.delta_sub_le (α β : Fin 2 → ℝ) (d : ℤ) : SimApprox.delta α d ≤ SimApprox.delta β d + |↑d| * ‖α - β‖

delta · d is |d|-Lipschitz in α. (Both are distances to the lattice; perturbing α by α − β moves d·α by d·(α−β).)

noncomputable def ThreeGap.LinftyRecords.aprt (s : ℝ) : Fin 2 → ℝ

The perturbed witness α* + (s, 0) = (4/47 + s, 15/47).

Equations

• ThreeGap.LinftyRecords.aprt s = ![4 / 47 + s, 15 / 47]

theorem ThreeGap.LinftyRecords.aprt_irrational {s : ℝ} (hs : Irrational s) : Irrational (aprt s 0)

theorem ThreeGap.LinftyRecords.norm_aprt (s : ℝ) (hs : 0 ≤ s) : ‖aprt s - astar‖ = s

theorem ThreeGap.LinftyRecords.norm_aprt' (s : ℝ) (hs : 0 ≤ s) : ‖astar - aprt s‖ = s

theorem ThreeGap.LinftyRecords.transport (s : ℝ) (hs0 : 0 ≤ s) (m n : ℤ) (Mm Mn : ℝ) (hm : SimApprox.delta astar m = Mm / 47) (hn : SimApprox.delta astar n = Mn / 47) (hgap : 47 * ((|↑m| + |↑n|) * s) < Mn - Mm) : SimApprox.delta (aprt s) m < SimApprox.delta (aprt s) n

Transport a defect inequality from α* to the perturbed witness.

theorem ThreeGap.LinftyRecords.Hpair (s : ℝ) (hs0 : 0 ≤ s) (hsmall : 1222 * s < 1) (m n Mm Mn : ℤ) (hm : SimApprox.delta astar m = ↑Mm / 47) (hn : SimApprox.delta astar n = ↑Mn / 47) (hc : |↑m| + |↑n| ≤ 26) (hgapZ : Mm + 1 ≤ Mn) : SimApprox.delta (aprt s) m < SimApprox.delta (aprt s) n

Bundles transport for an integer record gap: once s is small (1222·s < 1), an integer defect drop Mm + 1 ≤ Mn transports from α* to aprt s.

theorem ThreeGap.LinftyRecords.H1_aprt (s : ℝ) (hs0 : 0 ≤ s) (hsmall : 1222 * s < 1) (n : ℕ) : n ∈ Finset.Icc 1 7 → SimApprox.delta (aprt s) 9 < SimApprox.delta (aprt s) ↑n

theorem ThreeGap.LinftyRecords.H2_aprt (s : ℝ) (hs0 : 0 ≤ s) (hsmall : 1222 * s < 1) (n : ℕ) : n ∈ Finset.Icc 1 9 → SimApprox.delta (aprt s) 10 < SimApprox.delta (aprt s) ↑n

theorem ThreeGap.LinftyRecords.H3_aprt (s : ℝ) (hs0 : 0 ≤ s) (hsmall : 1222 * s < 1) (n : ℕ) : n ∈ Finset.Icc 1 10 → SimApprox.delta (aprt s) 12 < SimApprox.delta (aprt s) ↑n

theorem ThreeGap.LinftyRecords.H4_aprt (s : ℝ) (hs0 : 0 ≤ s) (hsmall : 1222 * s < 1) (n : ℕ) : n ∈ Finset.Icc 1 12 → SimApprox.delta (aprt s) 13 < SimApprox.delta (aprt s) ↑n

theorem ThreeGap.LinftyRecords.sharp_attained : ∃ (α : Fin 2 → ℝ), (∃ (k : Fin 2), Irrational (α k)) ∧ ∃ (N : ℕ), 2 ≤ N ∧ (Finset.image (DeltaCost.nnDist α N) (Finset.range (N + 1))).card = 5

Arithmetic sharpness of the L∞ five-distance theorem g_∞ ≤ 5 on 𝕋². There is a Kronecker vector α with an irrational coordinate and an N ≥ 2 for which the orbit {0, α, …, Nα} on 𝕋² realizes exactly five distinct sup-norm nearest-neighbour distances — so the bound nnDist_count_plane_unconditional is sharp. The witness is α = (4/47 + s, 15/47) for a small irrational s: card ≥ 5 transports from the rational α* (Lipschitz), card ≤ 5 is the five-distance theorem itself. Entirely elementary — no homogeneous dynamics.