The separation → angle crux for the Euclidean growth inequality

The Euclidean (L²) growth inequality behind the Euclidean five-distance theorem g₂ ≤ 5 (Haynes–Marklof) rests on a single geometric fact about the best-approximation remainder vectors r(qₙ), r(qₙ₊₁), … in a doubling window: each has Euclidean norm ≤ δₙ, and (separation lemma, SimApprox.window_separation) any two are at distance ≥ δₙ. This file proves the crux that converts that metric separation into an angular separation:

‖u‖, ‖v‖ ≤ δ and ‖u − v‖ ≥ δ ⟹ angle u v ≥ π/3,

and the strict form angle u v > π/3 when one of the vectors is strictly shorter than δ (which holds for all but the first remainder vector, since the defects strictly decrease). The verified algebraic heart is a² + b² − ab ≤ δ² for a, b ≤ δ (equality iff a = b = δ).

Where this sits in the route to g₂ ≤ 5. Pairwise angles > π/3 cap the number of remainder vectors in a window, hence the index gap n − m, hence the gap count:

• A 6-sector pigeonhole gives ≤ 6 vectors (K = 6, g₂ ≤ 7) — the contact-number bound.
• The angular gap-sum (6 × (>60°) > 360°) with the strict bound gives ≤ 5 (K = 5, g₂ ≤ 6).
• The sharp ≤ 4 (K = 4, g₂ ≤ 5) is Romanov's theorem (M.V. Romanov, Moscow Univ. Math. Bull. 61 (2006)): it needs the strict length-monotonicity together with the arithmetic difference-of-denominators structure, packaged as a convex-position argument plus a synthetic hexagon separation lemma — a strictly finer (and figure-dependent) input than the angle bound here.

This file isolates the fully-proven angular crux; the packing count on top of it is the remaining geometric step (sharp form = Romanov). Axiom-clean; elementary.

theorem ThreeGap.EuclideanAngle.sq_add_sq_sub_mul_le {a b δ : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (haδ : a ≤ δ) (hbδ : b ≤ δ) : a ^ 2 + b ^ 2 - a * b ≤ δ ^ 2

The algebraic heart. For 0 ≤ a, b ≤ δ, a² + b² − ab ≤ δ² (equality iff a = b = δ). Proof: a² ≤ aδ, b² ≤ bδ, and aδ + bδ − ab ≤ δ² since (δ − a)(δ − b) ≥ 0.

theorem ThreeGap.EuclideanAngle.sq_add_sq_sub_mul_lt {a b δ : ℝ} (ha : 0 < a) (hb : 0 < b) (haδ : a ≤ δ) (hbδ : b ≤ δ) (hstrict : a < δ ∨ b < δ) : a ^ 2 + b ^ 2 - a * b < δ ^ 2

Strict algebraic heart. For positive a, b ≤ δ, if moreover a < δ or b < δ, the inequality is strict. (Positivity is needed: (a, b) = (0, δ) gives equality δ².)

theorem ThreeGap.EuclideanAngle.inner_le_half_mul_norm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u v : E} {δ : ℝ} (hu : ‖u‖ ≤ δ) (hv : ‖v‖ ≤ δ) (hsep : δ ≤ ‖u - v‖) : inner ℝ u v ≤ ‖u‖ * ‖v‖ / 2

Separation ⟹ inner-product bound. If ‖u‖, ‖v‖ ≤ δ and the vectors are δ-separated (δ ≤ ‖u − v‖), then ⟪u, v⟫ ≤ ‖u‖ ‖v‖ / 2. (Law of cosines + the algebraic heart.)

theorem ThreeGap.EuclideanAngle.angle_ge_pi_div_three {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u v : E} {δ : ℝ} (hu0 : 0 < ‖u‖) (hv0 : 0 < ‖v‖) (hu : ‖u‖ ≤ δ) (hv : ‖v‖ ≤ δ) (hsep : δ ≤ ‖u - v‖) : Real.pi / 3 ≤ InnerProductGeometry.angle u v

The angular crux (non-strict). δ-separated vectors of norm ≤ δ subtend an angle ≥ π/3. This is the contact-number input: pairwise ≥ 60° ⟹ at most 6 such vectors in the plane.

theorem ThreeGap.EuclideanAngle.angle_gt_pi_div_three {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u v : E} {δ : ℝ} (hu0 : 0 < ‖u‖) (hv0 : 0 < ‖v‖) (hu : ‖u‖ ≤ δ) (hv : ‖v‖ ≤ δ) (hsep : δ ≤ ‖u - v‖) (hstrict : ‖u‖ < δ ∨ ‖v‖ < δ) : Real.pi / 3 < InnerProductGeometry.angle u v

The angular crux (strict). If in addition one vector is strictly shorter than δ — which holds for every remainder vector after the first, since the defects strictly decrease — the angle is strictly > π/3. This strictness is what upgrades the count from ≤ 6 to ≤ 5 (6 × (>60°) > 360°); the sharp ≤ 4 is Romanov's finer argument.

theorem ThreeGap.EuclideanAngle.norm_sub_lt_max_of_angle_lt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u v : E} (hu : u ≠ 0) (hv : v ≠ 0) (hang : InnerProductGeometry.angle u v < Real.pi / 3) : ‖u - v‖ < max ‖u‖ ‖v‖

Haynes–Marklof Proposition 2 (the cone-partition route to the sharp Euclidean five-distance bound g₂ ≤ 5, Haynes–Marklof, IMRN 2022, arXiv:2009.08444). If the angle between nonzero u, v is < π/3, then ‖u − v‖ < max ‖u‖ ‖v‖. This is the clean two-vector statement that replaces Romanov's growth lemma and the angular↔magnitude coupling: within any < π/3 cone of directions, two distinct nearest-neighbour distances cannot both occur.

theorem ThreeGap.EuclideanAngle.angle_ge_pi_div_three_of_norm_sub_gt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u w : E} (hu : u ≠ 0) (hw : w ≠ 0) (hnorm : ‖u‖ ≤ ‖w‖) (hsub : ‖w‖ < ‖u - w‖) : Real.pi / 3 ≤ InnerProductGeometry.angle u w

The record-angle bound (the contrapositive form Haynes–Marklof Theorem 8 consumes). If u is shorter than w but their difference is longer than w (‖w‖ < ‖u − w‖), then the angle between them is ≥ π/3. For the record vectors v₁,…,v_{K-1} (increasing norms, ‖vᵢ − vⱼ‖ > ‖vⱼ‖), this gives the pairwise ≥ π/3 separation feeding the 5-on-a-circle count.