The sharp Euclidean five-distance theorem g₂ ≤ 5 — Haynes–Marklof Theorem 8 core #
Grind toward the sharp bound g₂ ≤ 5 (Haynes–Marklof, IMRN 2022, arXiv:2009.08444), the
elementary, dynamics-free route. This file builds the combinatorial core (their Theorem 8): the
5-vectors-on-a-circle argument. Geometric heart here: the 2D signed area (det2) and the
characterisation of the open positive cone {s•x + t•z : s,t > 0} by sign conditions on det2.
This composes with the already-proven EuclideanAngle.norm_sub_lt_max_of_angle_lt (their Prop 2)
and
EuclideanAngle.angle_ge_pi_div_three_of_norm_sub_gt (the record-angle bound).
Cone membership from signed-area signs. If x, z are independent and det2 x y, det2 y z
have the same sign as det2 x z, then y lies in the open positive cone of x, z:
y = s•x + t•z with s, t > 0.
The cosine-difference law from signed areas. ⟪v₀,vᵢ⟫⟪v₀,vⱼ⟫ + det2 v₀ vᵢ · det2 v₀ vⱼ = ‖v₀‖²·⟪vᵢ,vⱼ⟫. Writing (aᵢ,dᵢ) = (⟪v₀,vᵢ⟫, det2 v₀ vᵢ)/(‖v₀‖‖vᵢ‖) as the cosine/sine of the
signed
angle of vᵢ from v₀, this says cos∠(vᵢ,vⱼ) = aᵢaⱼ + dᵢdⱼ — the full planar trigonometry,
derived
from det2 + inner alone (no oangle/kahler).
The sine-difference law from signed areas. ‖v₀‖²·det2 vᵢ vⱼ = det2 v₀ vⱼ · ⟪v₀,vᵢ⟫ − ⟪v₀,vⱼ⟫ · det2 v₀ vᵢ. In the (aᵢ,dᵢ) = (cos,sin) reading, sin∠(vᵢ→vⱼ) = dⱼaᵢ − aⱼdᵢ — so the
sign
of det2 vᵢ vⱼ (which orientation vⱼ is from vᵢ) is read off the v₀-relative coordinates.
The signed area is ‖x‖‖y‖·sin∠. |det2 x y| = ‖x‖ ‖y‖ · sin∠(x,y). With the cosine law
⟪x,y⟫ = ‖x‖‖y‖cos∠ and Lagrange det2² = ‖x‖²‖y‖² − ⟪x,y⟫², this gives det2² = ‖x‖²‖y‖²sin²∠.
So dᵢ := det2(v₀,vᵢ) has magnitude ‖v₀‖‖vᵢ‖·sin βᵢ (βᵢ = ∠(v₀,vᵢ)) — the "sine" coordinate.
Angle composition (same side). If vᵢ, vⱼ are on the same side of v₀ (det2 v₀ vᵢ,
det2 v₀ vⱼ same sign), then ∠(vᵢ,vⱼ) has cosine cos(βᵢ − βⱼ) (βₖ = ∠(v₀,vₖ)).
Angle composition (opposite sides). If vᵢ, vⱼ are on opposite sides of v₀
(det2 v₀ vᵢ, det2 v₀ vⱼ of opposite sign), then ∠(vᵢ,vⱼ) has cosine cos(βᵢ + βⱼ).
Same-side angle is the angle difference. When vᵢ, vⱼ lie on the same side of v₀,
∠(vᵢ,vⱼ) = |βᵢ − βⱼ| exactly (both lie in [0,π], and cosine is injective there). This is the
fact Step A feeds to not_four_in_interval: same-side record vectors pairwise > π/3 apart give
their βᵢ pairwise > π/3 apart in the length-π interval [0,π].
Opposite-side angle is the reduced angle sum. When vᵢ, vⱼ lie on opposite sides of v₀,
∠(vᵢ,vⱼ) = π − |π − (βᵢ + βⱼ)| — i.e. βᵢ + βⱼ if that is ≤ π, else 2π − (βᵢ + βⱼ) (the
reflection of the angle sum back into [0,π]). The flanking-wedge step uses the second branch: a
large angle sum forces a small cross-side angle.
Step B (flanking wedge). If vᵢ, vⱼ are on opposite sides of v₀ with angle sum
βᵢ + βⱼ > 5π/3, then the cross-side angle ∠(vᵢ,vⱼ) < π/3. (The two vectors flank v₀ so widely
that, wrapping past π, they come back within π/3 of each other.) Contrapositive: a cross-side
pair that is ≥ π/3 apart has βᵢ + βⱼ ≤ 5π/3.
The packing core (real-number form) #
At most 3 reals in an interval of length π can be pairwise more than π/3 apart. Four are
impossible: sorting, the three consecutive gaps each exceed π/3 so sum to > π, but the span is
≤ π. This is the real-number heart of "4 vectors in a half-plane can't be pairwise > π/3" (the
arc
has length ≤ π).
At most 2 reals in an interval of length 2π/3 can be pairwise more than π/3 apart. Three
are impossible: sorting, the two consecutive gaps each exceed π/3 so sum to > 2π/3, but the span
is ≤ 2π/3. The 2π/3-length analogue of not_four_in_interval — it bounds the number of vectors
on
one strict side of v₀ (where reference angles live in (π/3, π], of length < 2π/3).
The reduced angle |(↑Δ).toReal| also bounded by the complementary arc 2π − |Δ| (for
|Δ| ≤ 2π): together with abs_toReal_coe_le_abs, the reduced angle is ≤ min(|Δ|, 2π−|Δ|),
the cyclic distance.
At most 5 points on a circle can be pairwise more than π/3 apart (real-number core).
Six reals with pairwise cyclic distance min(|θᵢ−θⱼ|, 2π−|θᵢ−θⱼ|) > π/3 are impossible: sorting,
the five consecutive gaps telescope to θ₅−θ₀ > 5π/3, while the wrap-around gap 2π−(θ₅−θ₀) > π/3
forces θ₅−θ₀ < 5π/3. (The six cyclic gaps each exceed π/3 so sum to > 2π, but the circle has
circumference 2π.) This is the circular analogue of not_four_in_interval.
At most 5 vectors in the plane can be pairwise more than π/3 apart. Six nonzero vectors
of ℝ² cannot be pairwise > π/3 apart: assigning each a circular coordinate
θᵢ = (oangle(w₀, wᵢ)).toReal and using ∠(wᵢ,wⱼ) = |oangle(wᵢ,wⱼ).toReal| with oriented-angle
additivity, the pairwise condition becomes pairwise cyclic distance > π/3 among six circle points
— impossible by not_six_circular. This is the kissing-type packing bound behind the sharp
Euclidean five-distance theorem (g₂ ≤ 5).
At most 5 vectors pairwise > π/3 (finite-set form). A finset of nonzero plane vectors that
are pairwise more than π/3 apart has at most 5 elements — the form the record list consumes (the
K distinct nearest-neighbour distances give K pairwise-> π/3 vectors, so K ≤ 5).
Distinct-value count ≤ 5 from a separated record assignment (HM direct-route interface).
If each value val i (i ∈ s) is assigned a record vector rec (val i) that is nonzero, and
records of distinct values are pairwise more than π/3 apart, then there are at most 5 distinct
values. This is the exact interface for the sharp Euclidean g₂ ≤ 5: the K distinct
nearest-neighbour gaps at a fixed N, assigned their realizing orbit-difference vectors (records),
are pairwise > π/3 by the minimality crux (EuclideanAngle.angle_gt_pi_div_three), so K ≤ 5.
The remaining work is supplying the assignment rec and its two hypotheses — the gaps↔records
correspondence — not the geometry, which card_le_five_of_pairwise now discharges.
Step A: at most 3 vectors can be on one side of v₀ and pairwise > π/3. Four nonzero
vectors all on the same side of v₀ (all det2 v₀ (w i) of one sign) and pairwise more than π/3
apart are impossible: their reference angles βᵢ = ∠(v₀, w i) lie in the length-π interval
[0,π]
and (same side) are pairwise > π/3 apart, contradicting not_four_in_interval.
At most 2 vectors strictly on one side of v₀ and > π/3 from v₀, pairwise > π/3.
Three
nonzero vectors all on the same strict side of v₀ (det2 v₀ (w i) of one sign), each more than
π/3 from v₀, and pairwise more than π/3 apart are impossible: their reference angles
βᵢ = ∠(v₀, w i) lie in the length-2π/3 interval (π/3, π] and are pairwise > π/3 apart,
contradicting not_three_in_interval. This is the per-side ceiling the Theorem-8 cyclic argument
uses
(so the four non-shortest vectors split with ≥ 1 strictly on each side of the shortest).
At most one vector can be antiparallel to v₀. If det2 v₀ wᵢ = 0 and det2 v₀ wⱼ = 0
with
both > π/3 from v₀, then ∠(wᵢ,wⱼ) ≤ π/3 — impossible under pairwise > π/3. (Zero signed area
+
v₀ ≠ 0 ⟹ parallel to v₀; > π/3 from v₀ forces ∠(v₀,·)=π (antiparallel); two antiparallel
vectors point the same way, so ∠(wᵢ,wⱼ)=0.)
At least one vector strictly on the positive side of v₀. Among 4 nonzero vectors each > π/3
from v₀ and pairwise > π/3, some has det2 v₀ (w i) > 0. Otherwise all have det2 ≤ 0; at most
one is antiparallel (det2 = 0, by antiparallel_unique), so ≥ 3 are strictly negative — but
not_three_same_side forbids 3 on one strict side.
At least one vector strictly on the negative side of v₀ (mirror of exists_pos_det2).
v₁ lies in the open cone of a flanking pair. If vⱼ is strictly on the positive side of
v₁ (det2 v₁ vⱼ > 0), vₖ strictly on the negative side (det2 v₁ vₖ < 0), and the through-v₁
arc is less than π (det2 vⱼ vₖ < 0, the orientation that makes vⱼ, v₁, vₖ a positively-spanned
triple), then v₁ = s·vⱼ + t·vₖ with s, t > 0. From mem_openCone_of_det_signs.
Flanking sign from the angle sum. For vⱼ strictly on the positive side of v₀
(det2 v₀ vⱼ > 0) and vₖ strictly on the negative side (det2 v₀ vₖ < 0), the signed area
det2 vⱼ vₖ = −‖vⱼ‖‖vₖ‖·sin(βⱼ+βₖ) (βₘ = ∠(v₀,vₘ)), via the sine-difference law and sin_add. In
particular βⱼ+βₖ < π ⟹ det2 vⱼ vₖ < 0 — the through-v₀ arc is < π, the orientation
v1_mem_openCone_of_flanking needs.
Antiparallel angle. If w is a negative multiple of v₀ (forced when det2 v₀ w = 0 and
∠(v₀,w) > π/3, since then w is parallel but not codirectional), then for any u,
∠(w,u) = π − ∠(v₀,u). The reflected reference vector flips the angle through π.
Haynes–Marklof Theorem 8 — final contradiction step. With the cone property (the shortest
vector v 0 is in no open cone openCone(v j, v k) for higher indices 0 < j, k, j ≠ k), a
flanking pair — v j strictly positive of v 0, v k strictly negative, through-v 0 arc < π
(det2 (v j) (v k) < 0) — is contradictory, since it puts v 0 ∈ openCone(v j, v k). The arc-< π
fact (from det2_neg_of_opp_side_of_sum_lt_pi once the gap argument gives βⱼ+βₖ < π) is the
single
remaining geometric input for g₂ ≤ 5 along this route.
Antiparallel reference angle is π. If det2 v₀ w = 0 (so w is parallel to v₀) and
∠(v₀,w) > π/3 (ruling out codirectional), then ∠(v₀,w) = π. Extracted from
antiparallel_unique's
inner argument; the signed-angle gap argument needs it to pin antiparallel records to ψ = π.
Haynes–Marklof gap-existence (the flanking pair). Among 5 nonzero vectors pairwise more than
π/3 apart, there is a flanking pair for v 0: indices j, k ≠ 0 with v j strictly on the
positive side (det2 (v 0) (v j) > 0), v k strictly on the negative side (det2 (v 0) (v k) < 0),
and reference-angle sum βⱼ + βₖ < π. Proof. Pick the minimal-β vector on each side; if their
sum is < π we are done. Otherwise, place all 4 non-v 0 vectors at signed angles ψ (positive
side
ψ = β, negative/antiparallel side ψ = 2π − β); the assumed sum ≥ π compresses them into an
interval of length π, where they are still pairwise > π/3 (same-side: |βᵢ−βⱼ|; cross-side:
2π−(βᵢ+βⱼ); antiparallel: π−β) — impossible by not_four_in_interval.
Haynes–Marklof Theorem 8. Five nonzero vectors pairwise more than π/3 apart cannot satisfy
the cone property for v 0 (the shortest vector lies in no open cone of two higher-indexed
vectors).
Combines the flanking pair (exists_flanking_pair), the arc-sign bridge
(det2_neg_of_opp_side_of_sum_lt_pi), and the cone contradiction (hm_theorem8_final). This is the
geometric heart of the sharp Euclidean five-distance theorem g₂ ≤ 5.