The sharp Euclidean growth inequality 2 qₙ ≤ qₙ₊₄ (K = 4) via Haynes–Marklof Theorem 8

This sharpens euclidean_growth_five (2 qₙ ≤ qₙ₊₅, the planar packing count) to the sharp 2 qₙ ≤ qₙ₊₄, the input to the sharp Euclidean five-distance theorem g₂ ≤ 5. The five-vector configuration r(qₙ), …, r(qₙ₊₄) is admissible for the bare packing count (5 vectors pairwise > π/3 do fit), so the extra structure of Haynes–Marklof Theorem 8 (FiveDistance.hm_theorem8) is used: the shortest record r(qₙ₊₄) cannot lie in the open cone of two others, because that would force ‖r(qₙ₊₄) − vⱼ − vₖ‖ < ‖vₖ‖ (FiveDistanceHM.cone_exclusion) while the best-approximation property (hbest, the index difference lies in (0, qₖ)) forces ‖r(qₙ₊₄) − vⱼ − vₖ‖ > ‖vₖ‖. Axiom-clean.

theorem ThreeGap.SimApprox.euclidean_growth_four (α : 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 + 4)

The sharp Euclidean growth inequality, K = 4 (Haynes–Marklof Theorem 8). For a best-L²-approximation sequence (q, p) of α : Fin 2 → ℝ with the record/monotonicity hypotheses, the denominators at least double every four steps: 2 qₙ ≤ qₙ₊₄.