Documentation

LeanPool.ThreeGap.LinftyThreeTorusNine

The L∞ three-torus bound g_∞ ≤ 2^d+1 is sharp for d = 3: nine distances attained #

The repo's SimDirichlet.nnDist_count_unconditional proves the sup-norm bound g_∞ ≤ 2^d + 1 in all dimensions (Shutov), i.e. ≤ 9 for d = 3. Haynes–Marklof–Ramirez (arXiv:2010.08842, Higher dimensional gap theorems for the maximum metric, IJNT 17 (2021)) prove this bound is sharp for d ≤ 3, and give an explicit d = 3 example realizing exactly nine distinct sup-norm nearest-neighbour distances. This file formalizes that example, giving g_∞(3) ≥ 9; together with the repo's ≤ 9 it shows g_∞(3) = 9 — the bound is attained.

The witness (Haynes–Ramirez, §3) #

L = ℤ³, α = (−157/10000, −742/3125, −23/400) = (−785, −11872, −2875)/50000, N = 73. The scaled sup-norm defects M_m = max_k |r(a_k m)| (a = (−785,−11872,−2875), balanced residues mod 50000) have eight records in the doubling window (⌈73/2⌉, 73] = (37, 73] at m = 50,51,54,55,67,68,71,72, giving the nine distinct distances (over 50000) 11500 > 10750 > 9965 > 8912 > 8125 > 7375 > 7296 > 7088 > 7000, realized at q = 24,23,22,19,18,6,5,2,1.

Same dynamics-free, integer-exact route as LinftyRecords.sharp_attained (d = 2), extended to three coordinates; everything is exact modular arithmetic — no square roots.

noncomputable def ThreeGap.LinftyRecords3.astar :
Fin 3

The L∞ rational witness α* = (−785, −11872, −2875)/50000 on 𝕋³ (Haynes–Ramirez).

Equations
Instances For
    theorem ThreeGap.LinftyRecords3.delta_astar (d n₀ n₁ n₂ r₀ r₁ r₂ M : ) (hr0 : -785 * d = r₀ + 50000 * n₀) (hr1 : -11872 * d = r₁ + 50000 * n₁) (hr2 : -2875 * d = r₂ + 50000 * n₂) (hb0 : 2 * |r₀| 50000) (hb1 : 2 * |r₁| 50000) (hb2 : 2 * |r₂| 50000) (hM0 : |r₀| M) (hM1 : |r₁| M) (hM2 : |r₂| M) (hMa : M = |r₀| M = |r₁| M = |r₂|) :
    SimApprox.delta astar d = M / 50000

    The witness defect is coordinatewise-exact: delta α* d = M/50000 with M = max(|r₀|,|r₁|,|r₂|), the balanced residues of −785d, −11872d, −2875d mod 50000.

    The witness defects delta α* m = M_m/50000 for m = 1,…,72.

    theorem ThreeGap.LinftyRecords3.nine_le_card_image {N : } (f : ) {q₀ q₁ q₂ q₃ q₄ q₅ q₆ q₇ q₈ : } (m₀ : q₀ Finset.range (N + 1)) (m₁ : q₁ Finset.range (N + 1)) (m₂ : q₂ Finset.range (N + 1)) (m₃ : q₃ Finset.range (N + 1)) (m₄ : q₄ Finset.range (N + 1)) (m₅ : q₅ Finset.range (N + 1)) (m₆ : q₆ Finset.range (N + 1)) (m₇ : q₇ Finset.range (N + 1)) (m₈ : q₈ Finset.range (N + 1)) (h01 : f q₁ < f q₀) (h12 : f q₂ < f q₁) (h23 : f q₃ < f q₂) (h34 : f q₄ < f q₃) (h45 : f q₅ < f q₄) (h56 : f q₆ < f q₅) (h67 : f q₇ < f q₆) (h78 : f q₈ < f q₇) :

    Nine strictly-decreasing sample values force ≥ 9 distinct images.

    theorem ThreeGap.LinftyRecords3.nnDist_eq_inf (α : Fin 3) {q : } (hq : q 73) (hne : (Finset.Icc 1 (max q (73 - q))).Nonempty) :
    DeltaCost.nnDist α 73 q = (Finset.Icc 1 (max q (73 - q))).inf' hne fun (n : ) => SimApprox.delta α n

    nnDist as a prefix-minimum of the L∞ defect (d = 3, N = 73).

    theorem ThreeGap.LinftyRecords3.card_ge_nine (α : Fin 3) (H1 : nFinset.Icc 1 49, SimApprox.delta α 50 < SimApprox.delta α n) (H2 : nFinset.Icc 1 50, SimApprox.delta α 51 < SimApprox.delta α n) (H3 : nFinset.Icc 1 51, SimApprox.delta α 54 < SimApprox.delta α n) (H4 : nFinset.Icc 1 54, SimApprox.delta α 55 < SimApprox.delta α n) (H5 : nFinset.Icc 1 55, SimApprox.delta α 67 < SimApprox.delta α n) (H6 : nFinset.Icc 1 67, SimApprox.delta α 68 < SimApprox.delta α n) (H7 : nFinset.Icc 1 68, SimApprox.delta α 71 < SimApprox.delta α n) (H8 : nFinset.Icc 1 71, SimApprox.delta α 72 < SimApprox.delta α n) :

    card ≥ 9 from the eight record drops at m = 50,51,54,55,67,68,71,72, realized at q = 24,23,22,19,18,6,5,2,1 (cutoffs D = 49,50,51,54,55,67,68,71,72).

    Rational → irrational upgrade by Lipschitz-openness #

    noncomputable def ThreeGap.LinftyRecords3.aprt (s : ) :
    Fin 3

    The perturbed witness α* + (s,0,0).

    Equations
    Instances For
      theorem ThreeGap.LinftyRecords3.transport (s : ) (hs0 : 0 s) (m n : ) (Mm Mn : ) (hm : SimApprox.delta astar m = Mm / 50000) (hn : SimApprox.delta astar n = Mn / 50000) (hgap : 50000 * ((|m| + |n|) * s) < Mn - Mm) :
      theorem ThreeGap.LinftyRecords3.Hpair (s : ) (hs0 : 0 s) (hsmall : 7200000 * s < 1) (m n Mm Mn : ) (hm : SimApprox.delta astar m = Mm / 50000) (hn : SimApprox.delta astar n = Mn / 50000) (hc : |m| + |n| 144) (hgapZ : Mm + 1 Mn) :
      theorem ThreeGap.LinftyRecords3.H1_aprt (s : ) (hs0 : 0 s) (hsmall : 7200000 * s < 1) (n : ) :
      theorem ThreeGap.LinftyRecords3.H2_aprt (s : ) (hs0 : 0 s) (hsmall : 7200000 * s < 1) (n : ) :
      theorem ThreeGap.LinftyRecords3.H3_aprt (s : ) (hs0 : 0 s) (hsmall : 7200000 * s < 1) (n : ) :
      theorem ThreeGap.LinftyRecords3.H4_aprt (s : ) (hs0 : 0 s) (hsmall : 7200000 * s < 1) (n : ) :
      theorem ThreeGap.LinftyRecords3.H5_aprt (s : ) (hs0 : 0 s) (hsmall : 7200000 * s < 1) (n : ) :
      theorem ThreeGap.LinftyRecords3.H6_aprt (s : ) (hs0 : 0 s) (hsmall : 7200000 * s < 1) (n : ) :
      theorem ThreeGap.LinftyRecords3.H7_aprt (s : ) (hs0 : 0 s) (hsmall : 7200000 * s < 1) (n : ) :
      theorem ThreeGap.LinftyRecords3.H8_aprt (s : ) (hs0 : 0 s) (hsmall : 7200000 * s < 1) (n : ) :
      theorem ThreeGap.LinftyRecords3.nine_attained :
      ∃ (α : Fin 3), (∃ (k : Fin 3), Irrational (α k)) ∃ (N : ), 2 N 9 (Finset.image (DeltaCost.nnDist α N) (Finset.range (N + 1))).card

      The L∞ three-torus bound g_∞ ≤ 2^d+1 is sharp for d = 3. There is a Kronecker vector α : Fin 3 → ℝ with an irrational coordinate and N ≥ 2 whose orbit on 𝕋³ realizes at least nine distinct sup-norm nearest-neighbour distances; with SimDirichlet.nnDist_count_unconditional (≤ 9) this gives g_∞(3) = 9 — the Shutov bound 2^d+1 is attained (Haynes–Ramirez, d ≤ 3). The witness is α = (−785/50000 + s, −11872/50000, −2875/50000) for a small irrational s; card ≥ 9 transports from the rational α* by the dynamics-free Lipschitz argument.