Toward the sharp Euclidean five-distance theorem via Haynes–Marklof Theorem 8

The repo proves g₂ ≤ 6 (gap_count_euclidean) and reduces the sharp g₂ ≤ 5 to the planar packing count FiveDistance.card_le_five_of_pairwise (≤ 5 vectors pairwise > π/3). A literature pass (Haynes–Marklof, A five distance theorem for Kronecker sequences, IMRN 2022, arXiv:2009.08444) established that the upper bound 5 is elementary (their Sections 3–5; dynamics enters only for sharpness), but the step from 6 to 5 is not pure planar packing — six vectors pairwise > π/3 are possible (a regular pentagon plus one), and the boundary pair of the doubling window can fail the angular separation. HM defeat the sixth vector using a height coordinate u = t/N in addition to the planar direction v = rem α t p, together with the antipodal symmetry θ ↦ θ + π (their "largest symmetric subset S"). This file builds that route.

• recVec — the orbit-difference record vector in EuclideanSpace ℝ (Fin 2) (the planar v).
• recVec_neg / norm_recVec_neg — antipodal record symmetry (atom HM-1): the (−t, −p) record is the negation, of equal length. This is the symmetry θ ↦ θ + π underpinning HM's symmetric cone-partition (the basis for distinguishing 5 from 6).

See the module docstring of RomanovK4 and MATHLIB_SUCCESSIVE_MINIMA_SCOPE.md for the alternative (Romanov / lattice-minima) routes; this file pursues the elementary HM Theorem-8 route.

noncomputable def ThreeGap.FiveDistanceHM.recVec (α : Fin 2 → ℝ) (t : ℤ) (p : Fin 2 → ℤ) : EuclideanSpace ℝ (Fin 2)

The orbit-difference record vector rem α t p = t·α − p in EuclideanSpace ℝ (Fin 2) — the planar direction v of a Haynes–Marklof relevant vector.

Equations

• ThreeGap.FiveDistanceHM.recVec α t p = (EuclideanSpace.equiv (Fin 2) ℝ).symm (ThreeGap.SimApprox.rem α t p)

theorem ThreeGap.FiveDistanceHM.recVec_neg (α : Fin 2 → ℝ) (t : ℤ) (p : Fin 2 → ℤ) : recVec α (-t) (-p) = -recVec α t p

Antipodal record symmetry (atom HM-1). The record at the reflected offset (−t, −p) is the negation of the record at (t, p). This realizes the symmetry θ ↦ θ + π on the circle of record directions — the structure Haynes–Marklof's largest symmetric subset S is built from.

theorem ThreeGap.FiveDistanceHM.norm_recVec_neg (α : Fin 2 → ℝ) (t : ℤ) (p : Fin 2 → ℤ) : ‖recVec α (-t) (-p)‖ = ‖recVec α t p‖

The reflected record has the same length: antipodal records are equidistant.

theorem ThreeGap.FiveDistanceHM.angle_recVec_neg (α : Fin 2 → ℝ) (t : ℤ) (p : Fin 2 → ℤ) (h : recVec α t p ≠ 0) : InnerProductGeometry.angle (recVec α t p) (recVec α (-t) (-p)) = Real.pi

A record and its antipode point in exactly opposite directions (angle = π), when nonzero.

Height coordinate (atom HM-2)

noncomputable def ThreeGap.FiveDistanceHM.height (N : ℕ) (t : ℤ) : ℝ

The Haynes–Marklof height coordinate u = t/N of a record at offset t for parameter N — the "time" axis of the SL(3) lattice reformulation, the extra datum (beyond the planar direction recVec) that lets HM separate 5 from 6.

Equations

• ThreeGap.FiveDistanceHM.height N t = ↑t / ↑N

theorem ThreeGap.FiveDistanceHM.height_sub (N : ℕ) (t₁ t₂ : ℤ) : height N (t₁ - t₂) = height N t₁ - height N t₂

Heights subtract along offset differences: u(t₁ − t₂) = u(t₁) − u(t₂). (The record difference at offsets t₁, t₂ lives at height u(t₁) − u(t₂).)

theorem ThreeGap.FiveDistanceHM.height_neg (N : ℕ) (t : ℤ) : height N (-t) = -height N t

The antipodal record has the opposite height.

theorem ThreeGap.FiveDistanceHM.abs_height_le_one (N : ℕ) (t : ℤ) (hN : 0 < N) (ht : |t| ≤ ↑N) : |height N t| ≤ 1

A record offset |t| ≤ N has height in [−1, 1]. (The relevant records live in the unit height-slab |u| ≤ 1; HM's Proposition 3 uses the finer threshold |u| < 1/2.)

Haynes–Marklof Theorem 8 planar core (atoms HM-7)

The decoded structure of HM Theorem 8 (GS¹(M) ≤ 5): the first K−1 relevant vectors satisfy

• (5.2) ‖vᵢ − vⱼ‖ > ‖vⱼ‖ for i < j (Prop 16, from best-approximation minimality), and
• (5.3) ‖vᵢ − vⱼ − vₖ‖ ≥ ‖vₖ‖ for i < j < k (Prop 16). Prop 17 turns these into: (a) pairwise angle > π/3, and (b) no vᵢ lies in the open positive cone of vⱼ, vₖ (i < j < k). The final count: 5 vectors pairwise > π/3 are cyclically ordered, so the shortest lies in the cone of two later ones — contradicting (b). Everything is elementary plane geometry on the difference vectors.

HM Proposition 17(b) — the cone-exclusion estimate (reduced target, verified)

The geometric heart of Prop 17(b): if vᵢ = s·vⱼ + t·vₖ (s,t > 0) lies in the open cone of vⱼ, vₖ, is the shortest (‖vᵢ‖ < ‖vⱼ‖ < ‖vₖ‖), and makes an angle > π/3 with both vⱼ and vₖ, then ‖vᵢ − vⱼ − vₖ‖ < ‖vₖ‖ — contradicting (5.3). Writing b=‖vⱼ‖, c=‖vₖ‖, C=⟪vⱼ,vₖ⟫, the estimate reduces to the a-free polynomial inequality

b²(s−1)² + c²·t·(t−2) + 2C(s−1)(t−1) < 0

under: 0<b<c, s,t>0, 2C + bc < 0 (angle vⱼvₖ > 2π/3, from the cone + both > π/3), s²b² + t²c² + 2stC < b² (‖vᵢ‖ < ‖vⱼ‖), and the two realizability/angle constraints 4(sb²+tC)² < (s²b²+t²c²+2stC)·b², 4(sC+tc²)² < (s²b²+t²c²+2stC)·c² (i.e. |2⟪vᵢ,vⱼ⟫| < ‖vᵢ‖‖vⱼ‖, |2⟪vᵢ,vₖ⟫| < ‖vᵢ‖‖vₖ‖). Verified true (≈3·10⁶-sample search, worst value < −0.015); the constraint set is minimal (dropping either angle constraint yields a counterexample). The remaining task is the SOS/Positivstellensatz certificate: it is not a linear combination of the slacks (least-squares residual ≈ 6.3), so nlinarith does not auto-close it — it needs an SDP-found SOS or a coordinate/trig proof. This is the single hard kernel of HM Theorem 8.

Update (SDP): a degree-6 SOS certificate provably EXISTS (verified feasible by a cvxpy collocation SDP: −G = σ₀ + Σ σₖ·gₖ with σ₀ a sum of squares of degree-3 polynomials and σₖ degree-2 SOS multipliers on the seven constraints gₖ; degree-4 is infeasible, degree-6 feasible). So the estimate is not merely true but provable by Positivstellensatz. The numerical certificate has irrational degree-3 squares in σ₀, so it is not directly hand-translatable to nlinarith; closing it in Lean requires an exact rational SOS (rational SDP rounding) fed as explicit sq_nonneg/slack-product hints, or a coordinate/trig proof. Status: verified-true and provable; the exact Lean certificate is the one mechanical step that remains.

theorem ThreeGap.FiveDistanceHM.angle_add_of_mem_cone {vi vj vk : EuclideanSpace ℝ (Fin 2)} (hi : vi ≠ 0) {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (hcone : vi = s • vj + t • vk) : InnerProductGeometry.angle vj vk = InnerProductGeometry.angle vj vi + InnerProductGeometry.angle vi vk

Cone angle-additivity (atom HM-7d). If vᵢ = s·vⱼ + t·vₖ with s, t ≥ 0 (i.e. vᵢ lies in the closed positive cone of vⱼ, vₖ) and vᵢ ≠ 0, then ∠(vⱼ,vₖ) = ∠(vⱼ,vᵢ) + ∠(vᵢ,vₖ). In particular, if both ∠(vⱼ,vᵢ) > π/3 and ∠(vᵢ,vₖ) > π/3 then ∠(vⱼ,vₖ) > 2π/3 — the angle bound the cone-exclusion estimate (HM-7b) consumes. Direct from Mathlib's InnerProductGeometry.angle_eq_angle_add_add_angle_add_of_mem_span.

theorem ThreeGap.FiveDistanceHM.angle_gt_two_pi_div_three_of_cone {vi vj vk : EuclideanSpace ℝ (Fin 2)} (hi : vi ≠ 0) {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (hcone : vi = s • vj + t • vk) (hij : Real.pi / 3 < InnerProductGeometry.angle vj vi) (hik : Real.pi / 3 < InnerProductGeometry.angle vi vk) : 2 * Real.pi / 3 < InnerProductGeometry.angle vj vk

Cone forces a wide opening (atom HM-7d, corollary). If vᵢ is in the closed positive cone of vⱼ, vₖ and is more than π/3 from each, then ∠(vⱼ,vₖ) > 2π/3. This is the obtuse-angle bound the cone-exclusion estimate (HM-7b: C = ⟪vⱼ,vₖ⟫, 2C + ‖vⱼ‖‖vₖ‖ < 0) consumes.

theorem ThreeGap.FiveDistanceHM.angle_gt_of_norm_sub_ge {v w : EuclideanSpace ℝ (Fin 2)} (hv0 : v ≠ 0) (hlt : ‖v‖ < ‖w‖) (hsep : ‖w‖ ≤ ‖v - w‖) : Real.pi / 3 < InnerProductGeometry.angle v w

HM Proposition 17(a). Two record vectors v, w with ‖v‖ < ‖w‖ and the separation ‖w‖ ≤ ‖v − w‖ (Prop 16, eq. 5.2) make an angle > π/3. (The metric→angle crux with δ = ‖w‖: ‖v‖, ‖w‖ ≤ ‖w‖, ‖w‖ ≤ ‖v − w‖, and ‖v‖ < ‖w‖ strict.)

theorem ThreeGap.FiveDistanceHM.cone_trig_crux (b c βj βk : ℝ) (hb : 0 < b) (hbc : b ≤ c) (hj0 : 0 ≤ βj) (hjπ : βj ≤ Real.pi) (hk0 : 0 ≤ βk) (hkπ : βk ≤ Real.pi) (hsum : βj + βk ≤ Real.pi) : b * (1 - Real.cos βj) ≤ c * (Real.cos βk - Real.cos (βj + βk))

The crux trigonometric inequality of HM Proposition 17(b). For 0 < b ≤ c and angles βⱼ, βₖ ∈ [0,π] with βⱼ + βₖ ≤ π, b·(1 − cos βⱼ) ≤ c·(cos βₖ − cos(βⱼ+βₖ)). By sum-to-product this is 2 sin(βⱼ/2)·(c sin(βⱼ/2+βₖ) − b sin(βⱼ/2)) ≥ 0, and sin(βⱼ/2+βₖ) ≥ sin(βⱼ/2) because βⱼ/2+βₖ ∈ [βⱼ/2, π−βⱼ/2] (using βⱼ+βₖ ≤ π). This replaces HM's claimed SOS kernel: numerically the cone-exclusion estimate needs only the obtuse-cone and ‖v₀‖<‖vⱼ‖ constraints (the two realizability constraints are unnecessary), and the resulting reduced inequality has this clean trigonometric proof.

theorem ThreeGap.FiveDistanceHM.cone_exclusion {vj vk v0 : EuclideanSpace ℝ (Fin 2)} (hj : vj ≠ 0) (hk : vk ≠ 0) (hv0 : v0 ≠ 0) {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (hcone : v0 = s • vj + t • vk) (hlt : ‖v0‖ < ‖vj‖) (hbc : ‖vj‖ < ‖vk‖) (hβj : Real.pi / 3 < InnerProductGeometry.angle v0 vj) (hβk : Real.pi / 3 < InnerProductGeometry.angle v0 vk) : ‖v0 - vj - vk‖ < ‖vk‖

HM Proposition 17(b) — the cone-exclusion estimate (HM-7b, the former hard kernel). If v₀ lies in the closed positive cone of vⱼ, vₖ (v₀ = s·vⱼ + t·vₖ, s,t ≥ 0), is strictly shortest (‖v₀‖ < ‖vⱼ‖ < ‖vₖ‖), and makes an angle > π/3 with both edges, then ‖v₀ − vⱼ − vₖ‖ < ‖vₖ‖ — contradicting the record inequality (5.3). Proof (clean trig, replacing HM's claimed SOS): set r=‖v₀‖, b=‖vⱼ‖, c=‖vₖ‖, βⱼ=∠(v₀,vⱼ), βₖ=∠(v₀,vₖ); cone-additivity gives ∠(vⱼ,vₖ)=βⱼ+βₖ and both->π/3 gives >2π/3 (so 2⟪vⱼ,vₖ⟫ < −bc). Then ‖v₀−vⱼ−vₖ‖² − c² = r² − 2r(b cosβⱼ + c cosβₖ) + (b²+2⟪vⱼ,vₖ⟫), an upward parabola in r that is < 0 at r=0 (obtuse cone) and ≤ 0 at r=b (cone_trig_crux), hence < 0 on r ∈ (0,b) by the interpolation b·F(r) = (b−r)F(0) + r·F(b) − b·r·(b−r).