The Euclidean approximation defect is attained (the nearest lattice point exists)

euclidean_growth_five consumes the hypothesis hattain — that each remainder norm equals the defect δ_q. For the sup norm this came from coordinatewise rounding (DeltaCost.delta_attained); for the Euclidean norm the nearest lattice point is not coordinatewise, so attainment is a genuine (finite) minimization: among the integer translates with norm ≤ V (an explicit upper bound from rounding) only finitely many p survive (each coordinate is confined to an interval), and the minimum over that finite set realises the infimum.

deltaN_euclNorm_attained: ∃ p, euclNorm n (rem α q p) = δ_q. Axiom-clean.

theorem ThreeGap.SimApprox.euclNorm_eq {n : ℕ} (x : Fin n → ℝ) : euclNorm n x = √(∑ i : Fin n, x i ^ 2)

The Euclidean norm on Fin n → ℝ as a square root of a sum of squares.

theorem ThreeGap.SimApprox.abs_le_euclNorm {n : ℕ} (x : Fin n → ℝ) (k : Fin n) : |x k| ≤ euclNorm n x

Each coordinate is bounded by the Euclidean norm: |x k| ≤ euclNorm n x.

theorem ThreeGap.SimApprox.deltaN_euclNorm_attained {n : ℕ} (α : Fin n → ℝ) (q : ℤ) : ∃ (p : Fin n → ℤ), euclNorm n (rem α q p) = deltaN (euclNorm n) α q

The Euclidean defect is attained. For every denominator q there is an integer translate p with euclNorm n (rem α q p) = δ_q (the nearest lattice point to q • α).