The sup-norm defect cost: growth of its record denominators is unconditional

This file instantiates the abstract Chevallier machinery with the actual sup-norm approximation defect as the cost function:

r q = delta α q = inf_{p ∈ ℤᵈ} ‖q • α − p‖_∞ (the torus distance of q • α to the origin).

The payoff: the growth hypothesis fed to ChevallierCount.chevallier_gap_count_le — that the record denominators at least double every 2^d steps — holds automatically, with no extra hypothesis beyond RecordsContinue (irrationality). The two ingredients:

• delta_attained. For the sup norm the defect is attained by coordinatewise rounding: delta α q = ‖q • α − round(q • α)‖. (Each coordinate is minimised independently — round_le.) This supplies the hattain hypothesis of SupNormGrowth.supNorm_growth_doubling.
• The record structure of bestDenom supplies hdec (bestDenom_cost_antitone) and the full best-approximation property hbsad (bestDenom_strict_floor: q_k strictly beats every smaller positive denominator).

Combining the two, supNorm_growth_doubling gives 2 q_k ≤ q_{k+2^d} for q_k = bestDenom (delta α), which is exactly the growth input of chevallier_gap_count_le. Hence the combinatorial bound g_∞ ≤ 2^d + 1 holds for the sup-norm defect cost given only RecordsContinue — the growth geometry is now entirely discharged (orthant pigeonhole, already proven). The only remaining input to the geometric three-distance statement is the isometry identification (gapVal = nearest-neighbour distance), handled separately.

Axiom-clean.

noncomputable def ThreeGap.DeltaCost.nearestInt {d : ℕ} (α : Fin d → ℝ) (q : ℤ) : Fin d → ℤ

Coordinatewise nearest integer vector to q • α: round of each coordinate. For the sup norm this is the closest lattice point, so it attains the defect delta α q.

Equations

• ThreeGap.DeltaCost.nearestInt α q k = round (↑q * α k)

theorem ThreeGap.DeltaCost.rem_nearestInt_apply {d : ℕ} (α : Fin d → ℝ) (q : ℤ) (k : Fin d) : SimApprox.rem α q (nearestInt α q) k = ↑q * α k - ↑(round (↑q * α k))

The remainder against the nearest integer vector, coordinatewise.

theorem ThreeGap.DeltaCost.delta_attained {d : ℕ} (α : Fin d → ℝ) (q : ℤ) : ‖SimApprox.rem α q (nearestInt α q)‖ = SimApprox.delta α q

The defect is attained by rounding (sup norm). delta α q = ‖q • α − round(q • α)‖. Each coordinate |qα_k − round(qα_k)| ≤ |qα_k − p_k| (round_le), so the rounded vector minimises the sup norm over all integer translates. This is the hattain hypothesis of the growth lemma.

noncomputable def ThreeGap.DeltaCost.deltaCost {d : ℕ} (α : Fin d → ℝ) : ℕ → ℝ

The defect cost as a function of a natural-number denominator: r q = delta α q.

Equations

• ThreeGap.DeltaCost.deltaCost α q = ThreeGap.SimApprox.delta α ↑q

theorem ThreeGap.DeltaCost.bestDenom_hattain {d : ℕ} (α : Fin d → ℝ) (hr : Chevallier.RecordsContinue (deltaCost α)) (k : ℕ) : ‖SimApprox.rem α (↑(Chevallier.bestDenom (deltaCost α) hr k)) (nearestInt α ↑(Chevallier.bestDenom (deltaCost α) hr k))‖ = SimApprox.delta α ↑(Chevallier.bestDenom (deltaCost α) hr k)

hattain for the record denominators: at each q_k = bestDenom, the defect is attained by the nearest integer vector.

theorem ThreeGap.DeltaCost.bestDenom_hdec {d : ℕ} (α : Fin d → ℝ) (hr : Chevallier.RecordsContinue (deltaCost α)) {i j : ℕ} (h : i ≤ j) : SimApprox.delta α ↑(Chevallier.bestDenom (deltaCost α) hr j) ≤ SimApprox.delta α ↑(Chevallier.bestDenom (deltaCost α) hr i)

hdec for the record denominators: the defects delta α q_i are non-increasing in i.

theorem ThreeGap.DeltaCost.bestDenom_hbsad {d : ℕ} (α : Fin d → ℝ) (hr : Chevallier.RecordsContinue (deltaCost α)) (k : ℕ) (m : ℤ) (hpos : 0 < m) (hlt : m < ↑(Chevallier.bestDenom (deltaCost α) hr k)) : SimApprox.delta α ↑(Chevallier.bestDenom (deltaCost α) hr k) < SimApprox.delta α m

hbsad for the record denominators: each q_k is a strict record minimum over all smaller positive denominators — delta α q_k < delta α m for 0 < m < q_k.

theorem ThreeGap.DeltaCost.bestDenom_supNorm_growth {d : ℕ} (α : Fin d → ℝ) (hr : Chevallier.RecordsContinue (deltaCost α)) (k : ℕ) : 2 * Chevallier.bestDenom (deltaCost α) hr k ≤ Chevallier.bestDenom (deltaCost α) hr (k + 2 ^ d)

The sup-norm growth inequality for the defect record denominators (unconditional). With the defect cost r q = delta α q and RecordsContinue (irrationality), the record denominators q_k = bestDenom (delta α) at least double every 2^d steps:

2 q_k ≤ q_{k + 2^d}.

This discharges the growth hypothesis of ChevallierCount.chevallier_gap_count_le with no extra input — hattain comes from rounding (delta_attained), hdec/hbsad from the record structure (bestDenom_*), and the doubling itself from the orthant pigeonhole (supNorm_growth_doubling).

theorem ThreeGap.DeltaCost.gap_count_supNorm_le {d : ℕ} (α : Fin d → ℝ) (hr : Chevallier.RecordsContinue (deltaCost α)) {N : ℕ} (hN : 2 ≤ N) : (Finset.image (Chevallier.gapVal (deltaCost α) N) (Finset.range (N + 1))).card ≤ 2 ^ d + 1

g_∞ ≤ 2^d + 1 for the sup-norm defect cost (combinatorial form, unconditional growth). For every N ≥ 2, the number of distinct values of the abstract nearest-neighbour distance gapVal (delta α) N q (q ∈ [0,N]) is at most 2^d + 1. The growth is now fully discharged: the only hypothesis is RecordsContinue (the best approximations of α improve without bound, i.e. the appropriate irrationality of α). The remaining step to the geometric three-distance statement is the isometry identification of gapVal with the actual torus nearest-neighbour distance.