The sharp exponent for the minimal distance problem
We show that for every fixed ε>0, there exist arbitrarily large families of point-line pairs (x_1,ℓ_1),\ldots,(x_n,ℓ_n) in [0,1]^2, with x_i ∈ ℓ_i for all i, and such that dist(x_i,ℓ_j)≥ n^{-2/3-ε} for all i ≠ j. Combined with a previous result of Cohen, the author, and Zakharov, this solves the minimal distance problem.
The paper proves the minimal-distance construction attains separation n^{-2/3-ε} for every fixed ε > 0; combined with the known upper bound of Cohen, the author, and Zakharov, this establishes 2/3 as the sharp exponent for the minimal distance problem.
Reproduction
✓ reproduced
Attempted: For every ε > 0, there exists n₀ such that every n ≥ n₀ admits n incident point–line pairs in [0,1]² with dist(pᵢ, ℓⱼ) ≥ n^(−(2/3+ε)) whenever i ≠ j. No hypotheses declared — the paper's central theorem, proved outright.
A single self-contained development proving the paper's arithmetic construction end to end — totally-real number fields, trace-form bases, and house bounds included — with zero sorry and no custom axioms. Independent re-verification: elaborates cleanly, kernel-checked; the axiom audit reports only propext, Classical.choice, Quot.sound. Details in the run's README.
trace (327 events) · code (2 files)