Planar packing: at most 5 vectors pairwise more than 60° apart

The sharp Euclidean five-distance bound g₂ ≤ 5 needs to cap the number of best-approximation remainder vectors in a doubling window. The metric→angle crux (EuclideanAngle) shows they are pairwise strictly more than π/3 apart; this file supplies the planar packing count:

at most 5 vectors in the plane can be pairwise more than π/3 apart — equivalently, six are impossible.

The proof is the circular gap-sum. Via the oriented angle oangle (valued in ℝ/2πℤ, additive), the pairwise angle is |(φ i − φ j).toReal| for φ i = oangle (v 0) (v i). Sorting the representatives (φ i).toReal ∈ (−π, π] gives six points on the circle whose six consecutive gaps (five interior + one wrap) sum to 2π; each gap exceeds π/3 (the circular distance is ≤ the gap), so 2π = Σ gaps > 6 · π/3 = 2π, a contradiction.

The one analytic input is abs_toReal_coe_le: |(↑x).toReal| ≤ |x| — the circular distance never exceeds the representative distance. Applied to −D and to 2π − D it yields both the interior and the wrap bound with no case analysis.

This is the K = 5 packing count (g₂ ≤ 6); the sharp ≤ 4 (g₂ ≤ 5) is Romanov's finer argument. Axiom-clean; elementary.

theorem ThreeGap.EuclideanPacking.abs_toReal_coe_le (x : ℝ) : |(↑x).toReal| ≤ |x|

The circular distance never exceeds the representative distance: |(↑x).toReal| ≤ |x|. (If |x| ≥ π use |toReal| ≤ π; if |x| < π then x ∈ (−π, π] and (↑x).toReal = x.)

The combinatorial core: six points on the circle

theorem ThreeGap.EuclideanPacking.not_six_circle (φ : Fin 6 → Real.Angle) (h : ∀ (i j : Fin 6), i ≠ j → Real.pi / 3 < |(φ i - φ j).toReal|) : False

Six points of ℝ/2πℤ cannot be pairwise more than π/3 apart (in the toReal circular metric).

The vector form

theorem ThreeGap.EuclideanPacking.not_six_separated {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (v : Fin 6 → E) (hv : ∀ (i : Fin 6), v i ≠ 0) (hsep : ∀ (i j : Fin 6), i ≠ j → Real.pi / 3 < InnerProductGeometry.angle (v i) (v j)) : False

At most 5 vectors pairwise more than π/3 apart (the planar packing count). For an oriented plane E there are no six nonzero vectors that are pairwise strictly more than π/3 apart.