The any-norm growth inequality via the mod-2 pigeonhole (Lagarias II, Theorem 6)

The canonical growth inequality for best simultaneous Diophantine approximations, valid for every norm on ℝ^d (Lagarias, Best simultaneous Diophantine approximations II, Pacific J. Math. 102 (1982), Thm 6; restated in the Chevallier survey 2011, p. 5):

q_{n + 2^{d+1}} ≥ 2 q_{n+1} + q_n.

The proof is a mod-2 pigeonhole: among the 2^{d+1} + 1 best-approximation vectors (P_{n+k}, q_{n+k}), two agree mod 2 (there are only 2^{d+1} parity classes in (ℤ/2)^{d+1}); their half-difference (P, q) is an integer vector with 0 < q < q_{n+1} and remainder norm ≤ ½(δ_{q_{n+1}} + δ_{q_n}) < δ_{q_n}, contradicting the best-approximation/record property.

To get genuine any-norm generality we abstract the norm as a function N with the three norm properties (hN_nonneg, hN_tri, hN_smul) and the approximation defect as δ (a lower bound on N (rem …), with the best-approximation record structure). The norm-free remainder algebra (SimApprox.rem, rem_sub, rem_two_smul) is reused verbatim. Instantiating N at the Euclidean norm gives the Euclidean growth inequality (q_{n+8} ≥ 2q_{n+1}+q_n for d = 2), the input for the five-distance theorem.

Axiom-clean.

theorem ThreeGap.SimApprox.growth_additive_modTwo {d : ℕ} (N : (Fin d → ℝ) → ℝ) (hN_tri : ∀ (x y : Fin d → ℝ), N (x + y) ≤ N x + N y) (hN_smul : ∀ (c : ℝ) (x : Fin d → ℝ), N (c • x) = |c| * N x) (α : Fin d → ℝ) (q : ℕ → ℤ) (p : ℕ → Fin d → ℤ) (δ : ℤ → ℝ) (hmono : StrictMono q) (hδ_le : ∀ (m : ℤ) (P : Fin d → ℤ), δ m ≤ N (rem α m P)) (hattain : ∀ (k : ℕ), N (rem α (q k) (p k)) ≤ δ (q k)) (hdec : ∀ (k : ℕ), δ (q (k + 1)) < δ (q k)) (hbest : ∀ (k : ℕ) (m : ℤ), 0 < m → m < q (k + 1) → δ (q k) ≤ δ m) (n : ℕ) : 2 * q (n + 1) + q n ≤ q (n + 2 ^ (d + 1))

The any-norm growth inequality (mod-2 pigeonhole). For an abstract norm N and a best-approximation sequence (q, p) with defect δ (record minima), the denominators satisfy 2 q_{n+1} + q_n ≤ q_{n + 2^{d+1}}. Hypotheses: N is a norm (nonneg, triangle tri, homogeneity smul); δ m ≤ N (rem α m P) for every integer translate (hδ_le); the chosen remainders nearly attain the defect (hattain); defects strictly decrease along the sequence (hdec); and each q k is a record (hbest: every positive denominator below q (k+1) has defect ≥ δ (q k)).

theorem ThreeGap.SimApprox.supNorm_growth_additive {d : ℕ} (α : Fin d → ℝ) (q : ℕ → ℤ) (p : ℕ → Fin d → ℤ) (hmono : StrictMono q) (hattain : ∀ (k : ℕ), ‖rem α (q k) (p k)‖ ≤ delta α (q k)) (hdec : ∀ (k : ℕ), delta α (q (k + 1)) < delta α (q k)) (hbest : ∀ (k : ℕ) (m : ℤ), 0 < m → m < q (k + 1) → delta α (q k) ≤ delta α m) (n : ℕ) : 2 * q (n + 1) + q n ≤ q (n + 2 ^ (d + 1))

The sup-norm additive growth inequality as the concrete instance of the abstract mod-2 theorem at the sup norm ‖·‖ on Fin d → ℝ (with δ = SimApprox.delta): 2 q_{n+1} + q_n ≤ q_{n + 2^{d+1}}. This is the additive (Lagarias II Thm 6) form; the supNorm_growth_doubling companion gives the doubling form with the better constant 2^d via the orthant pigeonhole.