Chevallier's Lemma: the gap count is ≤ n − m + 1 (Chevallier 1996, Lemma 1.3)

The combinatorial heart of the higher-dimensional three-distance bounds (g_∞ ≤ 2^d+1, g_2 ≤ 5), following N. Chevallier, Distances dans la suite des multiples d'un point du tore à deux dimensions, Acta Arith. 74 (1996), Lemma 1.3.

For a base point with an isometry, the nearest-neighbour distance of the q-th orbit point among {x_0, …, x_N} is D_q = min_{1 ≤ j ≤ max(q, N−q)} d(x_0, x_j), because (isometry) the distances from x_q are d(x_0, x_{j}) for offsets j, and the offset range is max(q, N−q). The minimum of the "cost" r(j) = d(x_0, x_j) over [1, M] is attained at the record denominator q_{i*} with q_{i*} ≤ M < q_{i*+1}. As q ranges over [0,N], M = max(q, N−q) ∈ [⌈N/2⌉, N], so i* ∈ [m, n] where q_n ≤ N < q_{n+1} and 2q_m ≤ N < 2q_{m+1}. Hence the distinct gap values lie in {r(q_m), …, r(q_n)} — at most n − m + 1 of them. This is exactly the input ChevallierGapBound.gap_count_doubling needs (g_dist = n−m or n−m+1).

This file isolates the count as a pure statement about a cost function r : ℕ → ℝ and its records (ChevallierGapBound.bestDenom); the isometry reduction D_q = min … r is the geometric input.

Axiom-clean.

theorem ThreeGap.Chevallier.bestDenom_cost_strictAnti (r : ℕ → ℝ) (hr : RecordsContinue r) : StrictAnti fun (n : ℕ) => r (bestDenom r hr n)

The record costs r(q_i) are strictly decreasing in i (each record is a strictly better minimum).

theorem ThreeGap.Chevallier.bestDenom_cost_antitone (r : ℕ → ℝ) (hr : RecordsContinue r) {k i : ℕ} (h : k ≤ i) : r (bestDenom r hr i) ≤ r (bestDenom r hr k)

The record costs r(q_i) are non-increasing in i (each record is a new minimum).

theorem ThreeGap.Chevallier.bestDenom_strict_floor (r : ℕ → ℝ) (hr : RecordsContinue r) (k : ℕ) {j : ℕ} (hj1 : 1 ≤ j) (hj2 : j < bestDenom r hr k) : r (bestDenom r hr k) < r j

Strict record floor. Every j ∈ [1, q_k) has cost strictly above the record r(q_k): r(q_k) < r j for 1 ≤ j < q_k. (This is the full best-approximation property: q_k strictly beats every smaller positive denominator, not just those in its own bracket.)

theorem ThreeGap.Chevallier.record_floor (r : ℕ → ℝ) (hr : RecordsContinue r) (i : ℕ) {j : ℕ} (hj1 : 1 ≤ j) (hj2 : j < bestDenom r hr (i + 1)) : r (bestDenom r hr i) ≤ r j

Record floor. Every j ∈ [1, q_{i+1}) has cost ≥ r(q_i): the cost stays above the i-th record until the (i+1)-th. (So min_{1 ≤ j ≤ M} r(j) = r(q_i) when q_i ≤ M < q_{i+1}.)

noncomputable def ThreeGap.Chevallier.gapVal (r : ℕ → ℝ) (N q : ℕ) : ℝ

The nearest-neighbour distance of the q-th point among {x_0,…,x_N}, abstractly: the minimum cost min_{1 ≤ j ≤ max(q, N−q)} r(j) (junk 0 outside the valid range).

Equations

• ThreeGap.Chevallier.gapVal r N q = if h : (Finset.Icc 1 (max q (N - q))).Nonempty then (Finset.Icc 1 (max q (N - q))).inf' h r else 0

theorem ThreeGap.Chevallier.gapVal_eq_record (r : ℕ → ℝ) (hr : RecordsContinue r) {N : ℕ} (hN : 2 ≤ N) {n m : ℕ} (_hn1 : bestDenom r hr n ≤ N) (hn2 : N < bestDenom r hr (n + 1)) (hm1 : 2 * bestDenom r hr m ≤ N) (_hm2 : N < 2 * bestDenom r hr (m + 1)) {q : ℕ} (hq : q ≤ N) : ∃ (i : ℕ), m ≤ i ∧ i ≤ n ∧ gapVal r N q = r (bestDenom r hr i)

The gap value is a record cost in the band [m, n]. For q ∈ [0,N] (N ≥ 2), with n, m the record indices bracketing N and N/2, the nearest-neighbour distance gapVal N q equals r(q_i) for some i ∈ [m, n].

theorem ThreeGap.Chevallier.chevallier_count (r : ℕ → ℝ) (hr : RecordsContinue r) {N : ℕ} (hN : 2 ≤ N) {n m : ℕ} (hn1 : bestDenom r hr n ≤ N) (hn2 : N < bestDenom r hr (n + 1)) (hm1 : 2 * bestDenom r hr m ≤ N) (hm2 : N < 2 * bestDenom r hr (m + 1)) : (Finset.image (gapVal r N) (Finset.range (N + 1))).card ≤ n - m + 1

Chevallier's Lemma, upper bound (g_dist ≤ n − m + 1). For N ≥ 2, the number of distinct nearest-neighbour distances {gapVal N q : 0 ≤ q ≤ N} is at most n − m + 1, where q_n ≤ N < q_{n+1} and 2q_m ≤ N < 2q_{m+1}. This is exactly the gap-count hypothesis fed to ChevallierGapBound.gap_count_doubling to obtain g ≤ K + 1.

theorem ThreeGap.Chevallier.chevallier_gap_count_le (r : ℕ → ℝ) (hr : RecordsContinue r) (K : ℕ) (hgrowth : ∀ (k : ℕ), 2 * bestDenom r hr k ≤ bestDenom r hr (k + K)) {N : ℕ} (hN : 2 ≤ N) : (Finset.image (gapVal r N) (Finset.range (N + 1))).card ≤ K + 1

g_dist ≤ K + 1, abstractly (Chevallier's count + the growth inequality). If the record denominators satisfy the doubling growth 2 q_k ≤ q_{k+K} (Shutov: K = 2^d for L^∞, Romanov: K = 4 for the Euclidean plane), then the number of distinct nearest-neighbour distances is at most K + 1. Proof: chevallier_count gives ≤ n − m + 1, and index_bound_doubling gives n − m ≤ K from the growth. This is the complete combinatorial core of g_∞ ≤ 2^d + 1 and g_2 ≤ 5 — only the geometric isometry reduction (actual nearest-neighbour distance = gapVal) and the growth for the specific cost remain to instantiate.