Toward arithmetic sharpness of g₂ ≤ 5: five distances are attained (dynamics-free route) #
nnDistE_count_le_five proves the upper bound (≤ 5 distinct nearest-neighbour distances).
Sharpness — that 5 distinct distances are actually attained — is, in Haynes–Marklof, a
homogeneous-dynamics (equidistribution) statement. This file develops an elementary, dynamics-free
route to a concrete witness, discovered by unfolding the repo's own definitions.
The structural bypass #
nnDistE α N q = inf_{1 ≤ d ≤ max(q, N−q)} deltaN (euclNorm 2) α d (= gapVal (deltaE α) N q,
already in the repo). This prefix-minimum is non-increasing in the cutoff D = max(q, N−q), which
ranges over [⌈N/2⌉, N] as q ranges over {0,…,N}. It drops exactly at the best-approximation
records (whose defects strictly decrease). Hence
number of distinct distances
= 1 + #{record denominators in (⌈N/2⌉, N]}.
So sharpness ↔ four record denominators in the doubling window (⌈N/2⌉, N] — the extremal case
of
the proven growth 2qₙ ≤ q_{n+4} (euclidean_growth_four). No dynamics.
The concrete witness (verified numerically; integer/modular, exactly certifiable) #
α* = (3/29, 8/29), N = 11. Because ℤ² is a product and the norm is Euclidean,
deltaN (euclNorm 2) α* d = √(r(3d)² + r(8d)²) / 29, where r(m) is the balanced residue of m
mod 29 (in [−14,14]) — coordinatewise, no 2-D lattice search. The squared scaled defects
K_d = r(3d)² + r(8d)² for d = 1,…,11 are
[73, 205, 106, 153, 317, 221, 68, 61, 200, 50, 17],
with record minima at d = 1, 7, 8, 10, 11 (values 73 > 68 > 61 > 50 > 17). The records inside
(⌈11/2⌉, 11] = (6, 11] are 7, 8, 10, 11 — four — giving the five distinct distances
√73, √68, √61, √50, √17 all over 29, realized at q = 5, 4, 3, 1, 0 (cutoffs D = 6,7,8,10,11).
Remaining atoms (each elementary, no research gap) #
- R4.
deltaN α* d = √(r(3d)²+r(8d)²)/29and the four strict drops, via per-coordinate integer facts: upper bound bydeltaN_leat the roundingp; lower bound byle_ciInf+|m − 29k| ≥ |r(m)|. All comparisons are between integersK_d. - R5. rational → irrational: each strict drop
deltaN α a < deltaN α bis Lipschitz inα(deltaN · disd-Lipschitz,dist(·,ℤ²)being 1-Lipschitz), with explicit integer slack atα*; perturb one coordinate to an irrational inside that slack. Thencount ≥ 5(this file'sfive_le_card_image_of_strictAnti_chain) andcount ≤ 5(nnDistE_count_le_five) give= 5.
five_le_card_image_of_strictAnti_chain below is the foundational R3 step (axiom-clean).
Per-coordinate integer minimum (R4 crux). If r is the balanced residue of a mod m
(m ∣ a − r and 2|r| ≤ m), then r² is the minimum of (a − m·k)² over all integers k — the
nearest multiple of m to a is at distance |r|. This is the coordinatewise core of the defect
lower bound deltaN α* d ≥ √(r(3d)²+r(8d)²)/29: since ℤ² is a product and the norm Euclidean, the
nearest lattice point is coordinatewise nearest.
The rational witness α* = (3/29, 8/29).
Equations
- ThreeGap.EuclideanRecords.astar = ![3 / 29, 8 / 29]
Instances For
euclNorm 2 of an explicit plane vector is √(x₀² + x₁²).
Defect by attainment + lower bound. If some translate realizes value c and c bounds all
translates below, the defect equals c.
The witness defect is coordinatewise-exact (R4b). With α* = (3/29, 8/29), balanced
residues 3d ≡ r₀, 8d ≡ r₁ (mod 29) give deltaN α* d = √(r₀² + r₁²)/29. Upper bound at the
rounding (n₀,n₁); lower bound coordinatewise via sq_residue_le.
The eleven witness defects deltaN α* d = √(K_d)/29, d = 1,…,11, with
K_d = [73,205,106,153,317,221,68,61,200,50,17] — verified by deltaN_astar at the balanced
residues of 3d, 8d mod 29.
The record chain deltaN α* 1 > deltaN α* 7 > deltaN α* 8 > deltaN α* 10 > deltaN α* 11
(√73 > √68 > √61 > √50 > √17, all over 29) — the four record drops giving five distances.
Five strictly-decreasing sample values force ≥ 5 distinct images. If f takes five values
f q₀ > f q₁ > f q₂ > f q₃ > f q₄ at points of Finset.range (N+1), then the image of
Finset.range (N+1) under f has at least five elements. The combinatorial heart of arithmetic
sharpness: exhibiting five strictly-decreasing nearest-neighbour distances.
nnDistE as a prefix-minimum of the defect. nnDistE α 11 q is the infimum of
deltaN (euclNorm 2) α d over d ∈ [1, max(q, 11−q)] (via the repo's gapVal_eq_nnDistC).
A strictly larger prefix has a strictly smaller infimum once a new element m beats the whole
shorter prefix.
card ≥ 5 from the four record drops (R4b-finish). If the defect drops strictly below the
whole preceding prefix at d = 7, 8, 10, 11, then the five nnDistE α 11 q at q = 5,4,3,1,0 are
strictly decreasing, so the image has ≥ 5 elements.
The witness realizes ≥ 5 distinct distances (R4b complete, rational α*). The orbit of
α* = (3/29, 8/29) to N = 11 has at least five distinct Euclidean nearest-neighbour distances —
the four record drops of card_ge_five discharged by the dstar defect values.
R5: rational → irrational upgrade by Lipschitz-openness #
deltaN · d is |d|-Lipschitz in α. (Both are distances to the lattice; perturbing α
by
α − β moves d·α by d·(α−β).)
The gap inequality 29·(c·s) < √Kn − √Km holds once s is small (1276·s·√317 < 1), for any
coefficient c ≤ 22 and integer gap Km + 1 ≤ Kn ≤ 317.
Transport an inequality from α* to the perturbed witness.
Bundles transport + gap_ok for the perturbed witness: a defect comparison transports from
α* once s is small.
Arithmetic sharpness of g₂ ≤ 5 (R5 / final). There is a Kronecker vector α with an
irrational coordinate and an N ≥ 2 for which the orbit {0, α, …, Nα} on 𝕋² realizes exactly
five distinct Euclidean nearest-neighbour distances — so the bound nnDistE_count_le_five is
sharp.
The witness is α = (3/29 + s, 8/29) for a small irrational s: card ≥ 5 transports from the
rational α* (Lipschitz), card ≤ 5 is the five-distance theorem itself.