The Euclidean growth inequality 2 qₙ ≤ qₙ₊₅ (K = 5) via the planar packing count

This is the core of the Euclidean route to g₂ ≤ 6: the best-simultaneous-approximation denominators in the Euclidean (L²) norm on 𝕋² at least double every 5 steps. Combined with Chevallier's count this gives the Euclidean five-distance bound g₂ ≤ 6 (the sharp g₂ ≤ 5 needs Romanov's K = 4).

The mechanism (Lagarias/Ermakov, with the contact number 6 replaced by the strict planar packing count 5): if the denominators failed to double in a window of length 5, the six remainder vectors r(qₙ), …, r(qₙ₊₅) would all have Euclidean norm ≤ δₙ and be pairwise ≥ δₙ apart (the best-approximation separation: their index differences lie in (0, qₙ), so hbest forces the defect up). The metric→angle crux (EuclideanAngle) turns that into pairwise angles strictly > π/3 (strict because the defects strictly decrease, so all but the first vector is shorter than δₙ), and the planar packing count (EuclideanPacking.not_six_separated) says at most 5 such vectors fit — contradiction.

Stated, like EuclideanGrowth.euclidean_growth_additive, over an abstract best-approximation sequence (q, p) with the defining hypotheses; discharging those for the actual record denominators is the remaining instantiation step. Axiom-clean.

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

rem negates under simultaneous negation of denominator and translate.

theorem ThreeGap.SimApprox.deltaN_neg {n : ℕ} (N : (Fin n → ℝ) → ℝ) (hN0 : ∀ (x : Fin n → ℝ), 0 ≤ N x) (hNneg : ∀ (x : Fin n → ℝ), N (-x) = N x) (α : Fin n → ℝ) (q : ℤ) : deltaN N α (-q) = deltaN N α q

The defect for a symmetric norm is even in the denominator: δ_{−q} = δ_q.

theorem ThreeGap.SimApprox.euclNorm_neg {n : ℕ} (x : Fin n → ℝ) : euclNorm n (-x) = euclNorm n x

The Euclidean norm is symmetric.

theorem ThreeGap.SimApprox.euclidean_growth_five (α : Fin 2 → ℝ) (q : ℕ → ℤ) (p : ℕ → Fin 2 → ℤ) (hmono : StrictMono q) (hattain : ∀ (k : ℕ), euclNorm 2 (rem α (q k) (p k)) ≤ deltaN (euclNorm 2) α (q k)) (hdec : ∀ (i j : ℕ), i ≤ j → deltaN (euclNorm 2) α (q j) ≤ deltaN (euclNorm 2) α (q i)) (hdecstrict : ∀ (k : ℕ), deltaN (euclNorm 2) α (q (k + 1)) < deltaN (euclNorm 2) α (q k)) (hbest : ∀ (k : ℕ) (m : ℤ), 0 < m → m < q k → deltaN (euclNorm 2) α (q k) < deltaN (euclNorm 2) α m) (hpos : ∀ (k : ℕ), 0 < deltaN (euclNorm 2) α (q k)) (N : ℕ) : 2 * q N ≤ q (N + 5)

The Euclidean growth inequality, K = 5 (planar packing). For a best-L²-approximation sequence (q, p) of α : Fin 2 → ℝ with the record/monotonicity hypotheses, the denominators at least double every five steps: 2 qₙ ≤ qₙ₊₅.