The sup-norm growth inequality via the orthant pigeonhole (fully proven)

For best simultaneous Diophantine approximation in the sup norm on ℝ^d, the denominators at least double every 2^d steps:

2 q_N ≤ q_{N + 2^d}.

This is the elementary half of Shutov's L^∞ growth inequality (the full q_{N+2^d} ≥ q_{N+1}+q_N is Lagarias 1980; the doubling form here already suffices for the gap bound, via ChevallierGapBound.gap_count_doubling). The proof is the orthant pigeonhole of the Chevallier survey (§2.4.1, attributed to Lagarias):

• Among the 2^d + 1 remainder vectors ε_N, …, ε_{N+2^d}, two share an orthant (a sign pattern in {≥0, <0}^d), since there are only 2^d orthants — Fintype.exists_ne_map_eq_of_card_lt.
• Two vectors in the same orthant, each of sup-norm ≤ r_N = δ_{q_N}, have difference of sup-norm ≤ r_N (coordinatewise, same sign ⟹ |a−b| ≤ max(|a|,|b|)).
• That difference is the remainder of m = q_{N+k₂} − q_{N+k₁} (SimApprox.delta_diff_le), so δ_m ≤ r_N; the best-approximation/record property then forces m ≥ q_N, giving the doubling.

No convex geometry, no kissing number — purely the pigeonhole. Axiom-clean.

theorem ThreeGap.SimApprox.abs_sub_le_of_same_sign {a b r : ℝ} (hsign : 0 ≤ a ↔ 0 ≤ b) (ha : |a| ≤ r) (hb : |b| ≤ r) : |a - b| ≤ r

Pointwise: two reals of the same sign (0 ≤ a ↔ 0 ≤ b) with |a|, |b| ≤ r satisfy |a − b| ≤ r. (If both ≥ 0 or both ≤ 0, the difference cannot exceed the larger magnitude.)

theorem ThreeGap.SimApprox.norm_sub_le_of_sameOrthant {d : ℕ} {u v : Fin d → ℝ} {r : ℝ} (hsign : ∀ (k : Fin d), 0 ≤ u k ↔ 0 ≤ v k) (hu : ‖u‖ ≤ r) (hv : ‖v‖ ≤ r) : ‖u - v‖ ≤ r

Same-orthant sup-norm bound. If u, v : Fin d → ℝ lie in the same orthant (0 ≤ u k ↔ 0 ≤ v k for every k) and each has sup-norm ≤ r, then ‖u − v‖ ≤ r.

theorem ThreeGap.SimApprox.supNorm_growth_doubling {d : ℕ} (α : Fin d → ℝ) (q : ℕ → ℤ) (p : ℕ → Fin d → ℤ) (hmono : StrictMono q) (hattain : ∀ (k : ℕ), ‖rem α (q k) (p k)‖ = delta α (q k)) (hdec : ∀ (i j : ℕ), i ≤ j → delta α (q j) ≤ delta α (q i)) (hbsad : ∀ (k : ℕ) (m : ℤ), 0 < m → m < q k → delta α (q k) < delta α m) (N : ℕ) : 2 * q N ≤ q (N + 2 ^ d)

The sup-norm growth inequality, doubling form (orthant pigeonhole). Suppose q enumerates best-approximation denominators of α in the sup norm, with remainders p attaining the defect (hattain), defects non-increasing along the sequence (hdec), and each q k a record minimum (hbsad: every smaller positive denominator has strictly larger defect). Then

2 q_N ≤ q_{N + 2^d}.

This feeds ChevallierGapBound.gap_count_doubling with K = 2^d to give g_∞ ≤ 2^d + 1.

theorem ThreeGap.SimApprox.gap_count_supNorm {d : ℕ} (α : Fin d → ℝ) (q : ℕ → ℤ) (p : ℕ → Fin d → ℤ) (hmono : StrictMono q) (hattain : ∀ (k : ℕ), ‖rem α (q k) (p k)‖ = delta α (q k)) (hdec : ∀ (i j : ℕ), i ≤ j → delta α (q j) ≤ delta α (q i)) (hbsad : ∀ (k : ℕ) (m : ℤ), 0 < m → m < q k → delta α (q k) < delta α m) {N : ℤ} {m n g : ℕ} (hnN : q n ≤ N) (hNm : N < 2 * q (m + 1)) (hg : g = n - m ∨ g = n - m + 1) : g ≤ 2 ^ d + 1

g_∞ ≤ 2^d + 1 from the orthant pigeonhole + Chevallier's Lemma. Assembling supNorm_growth_doubling (the fully-proven sup-norm growth, K = 2^d) with the doubling gap-count reduction, the number of distinct nearest-neighbour distances of a sup-norm best-approximation sequence is at most 2^d + 1. The only remaining hypothesis is Chevallier's Lemma (hg: the g = n − m / n − m + 1 index dictionary) — the growth geometry is now entirely elementary (orthant pigeonhole), with no kissing number or convex-geometry input.