Documentation

LeanPool.ThreeGap.EuclideanRecords

Euclidean record denominators ⟹ g₂ ≤ 6 (combinatorial, unconditional) #

Assembles the Euclidean route: with the Euclidean defect cost r q = deltaN(euclNorm 2) α q, the record denominators bestDenom r satisfy every hypothesis of euclidean_growth_five — hattain from deltaN_euclNorm_attained, hdec/hbest from the record structure, hpos from irrationality — so 2 q_k ≤ q_{k+5}. Feeding this K = 5 growth into Chevallier's count (chevallier_gap_count_le) gives the Euclidean five-distance bound g₂ ≤ 6: at most six distinct values of the Euclidean nearest-neighbour distance gapVal (deltaE α) N q.

RecordsContinue (the irrationality input) is discharged exactly as for the sup norm, transferring Dirichlet via deltaN(euclNorm 2) α q ≤ √2 · delta α q (the Euclidean norm is ≤ √2 · the sup norm in the plane). The sharp g₂ ≤ 5 needs Romanov's K = 4; this is the K = 5 bound. Axiom-clean.

source
noncomputable def ThreeGap.EuclideanRecords.deltaE (α : Fin 2 → ℝ) :
ℕ → ℝ

The Euclidean defect cost as a function of a natural denominator.

Equations
Instances For
    source
    theorem ThreeGap.EuclideanRecords.euclNorm_le_sqrt_two_mul (x : Fin 2 → ℝ) :
    SimApprox.euclNorm 2 x ≤ √2 * ‖x‖

    The Euclidean norm is at most √2 · the sup norm in the plane.

    source
    theorem ThreeGap.EuclideanRecords.deltaE_le_sqrt_two_mul (α : Fin 2 → ℝ) (q : ℤ) :
    SimApprox.deltaN (SimApprox.euclNorm 2) α q ≤ √2 * SimApprox.delta α q

    Dirichlet transferred to the Euclidean defect: δ^E_q ≤ √2 · δ_q.

    source
    theorem ThreeGap.EuclideanRecords.exists_deltaE_lt (α : Fin 2 → ℝ) {ε : ℝ} (hε : 0 < ε) :
    ∃ (q : ℕ), 1 ≤ q ∧ deltaE α q < ε

    Euclidean Dirichlet: the defect gets arbitrarily small.

    source
    theorem ThreeGap.EuclideanRecords.deltaE_pos (α : Fin 2 → ℝ) {k₀ : Fin 2} (hirr : Irrational (α k₀)) {q : ℕ} (hq : 1 ≤ q) :
    0 < deltaE α q

    Euclidean positivity: δ^E_q > 0 for q ≥ 1 when some coordinate is irrational.

    source
    theorem ThreeGap.EuclideanRecords.recordsContinue_deltaE (α : Fin 2 → ℝ) {k₀ : Fin 2} (hirr : Irrational (α k₀)) :
    Chevallier.RecordsContinue (deltaE α)

    RecordsContinue (deltaE α) from irrationality.

    source
    theorem ThreeGap.EuclideanRecords.bestDenom_hbest (α : Fin 2 → ℝ) (hr : Chevallier.RecordsContinue (deltaE α)) (k : ℕ) (m : ℤ) (hpos : 0 < m) (hlt : m < ↑(Chevallier.bestDenom (deltaE α) hr k)) :
    SimApprox.deltaN (SimApprox.euclNorm 2) α ↑(Chevallier.bestDenom (deltaE α) hr k) < SimApprox.deltaN (SimApprox.euclNorm 2) α m

    hbest for the Euclidean record denominators (strict best-approximation property).

    source
    theorem ThreeGap.EuclideanRecords.bestDenom_euclidean_growth (α : Fin 2 → ℝ) {k₀ : Fin 2} (hirr : Irrational (α k₀)) (hr : Chevallier.RecordsContinue (deltaE α)) (k : ℕ) :
    2 * Chevallier.bestDenom (deltaE α) hr k ≤ Chevallier.bestDenom (deltaE α) hr (k + 5)

    The Euclidean growth 2 q_k ≤ q_{k+5} for the record denominators (unconditional).

    source
    theorem ThreeGap.EuclideanRecords.gap_count_euclidean (α : Fin 2 → ℝ) {k₀ : Fin 2} (hirr : Irrational (α k₀)) {N : ℕ} (hN : 2 ≤ N) :
    (Finset.image (Chevallier.gapVal (deltaE α) N) (Finset.range (N + 1))).card ≤ 6

    g₂ ≤ 6 (Euclidean five-distance count, combinatorial, unconditional). For any α : Fin 2 → ℝ with an irrational coordinate and N ≥ 2, the number of distinct values of the Euclidean nearest-neighbour distance gapVal (deltaE α) N q is at most 6.