2607.20422v1 / README.md

all files

# Reproduction of “The sharp exponent for the minimal distance problem”

This directory contains a complete Lean 4/mathlib proof of Theorem 1.1 of
arXiv:2607.20422v1. The development is in `SharpDistance.lean`.

## Result and verification

The final theorem is:

```lean
theorem SharpDistance.sharp_exponent_for_minimal_distance
    (ε : ℝ) (hε : 0 < ε) :
    ∃ n₀ : ℕ, ∀ n ≥ n₀, ∃ C : PLConfiguration n,
      C.Separated ((n : ℝ) ^ (-((2 : ℝ) / 3 + ε)))
```

Thus, for every positive `ε` and every sufficiently large integer `n`, the
proof constructs exactly `n` point–line pairs in the unit square, with each
point on its assigned line, and with

```text
dist(point i, line j) ≥ n^(-(2/3 + ε))     whenever i ≠ j.
```

Check it offline from this directory with:

```sh
lake env lean SharpDistance.lean
```

The command succeeds. The file contains no `sorry`, `admit`, custom `axiom`,
or additional hypothesis. The only logical foundations used are Lean and
mathlib's ordinary classical machinery. An axiom audit of the final theorem
reports only `propext`, `Classical.choice`, and `Quot.sound`.

## Why the formal statement is the paper's statement

The geometric definitions deliberately restate the paper rather than replace
it by a convenient combinatorial proxy.

* `Point` is `EuclideanSpace ℝ (Fin 2)`, i.e. the ordinary Euclidean plane.
* `RealLine` consists of a base point, a nonzero direction, and has carrier
  `{base + t • direction | t : ℝ}`.
* `pointLineDist p ℓ` is mathlib's `Metric.infDist p ℓ.carrier`, the standard
  distance from a point to a subset.
* `InUnitSquare p` is the four coordinate inequalities
  `0 ≤ p₀ ≤ 1` and `0 ≤ p₁ ≤ 1`.
* `PLConfiguration n` contains maps from `Fin n` to points and real lines,
  together with proofs that every point lies in the unit square and on its
  assigned line.
* `C.Separated δ` is literally
  `∀ i j, i ≠ j → δ ≤ pointLineDist (C.points i) (C.lines j)`.

The sanity lemmas `RealLine.base_mem`, `RealLine.carrier_nonempty`, and
`pointLineDist_self` establish incidence and zero self-distance. The lemma
`pointLineDist_ge_inner_div_norm` proves the standard normal-vector estimate
for this metric definition directly from Cauchy–Schwarz. Consequently no
custom or weakened notion of line distance occurs in the final theorem.

For `n ≥ n₀`, the asserted lower bound is positive. It follows from
separation and incidence that different indices cannot accidentally encode
the same point or the same line, even though distinctness does not need to be
added separately to the paper's statement. This is formalized by
`PLConfiguration.points_injective_of_separated` and
`PLConfiguration.lines_injective_of_separated`.

## Formal construction

The proof follows the paper's trace-zero number-field construction, with an
explicit integral-basis box used to make the counting step elementary.

### 1. Trace-zero box

Fix a totally real number field `K` of degree `d`. From the integral basis of
`𝓞 K`, the proof selects a pivot basis vector with nonzero integral trace.
For every other basis index `i`, it defines

```text
gᵢ = Tr(b_pivot) bᵢ - Tr(bᵢ) b_pivot.
```

The file proves:

* `Tr(gᵢ) = 0`;
* the `gᵢ` are linearly independent for the coefficient ranges used;
* their index set has cardinality `d - 1`.

For an integer parameter `m`, coefficients of a trace-zero element `a₀`
range through `0,…,m²`, while coefficients of an arbitrary integer `w`
range through `0,…,m`. This gives exactly

```text
(m² + 1)^(d - 1) (m + 1)^d
```

sources, and at least `m^(3d-2)` sources.

Each source is mapped to

```text
a = 2a₀,   y = 2w,   x = a₀ + 2w².
```

The polynomial identity `2x - y² = a` is proved as
`sourceQ_identity`. Injectivity of `(x,y)` is also proved.

### 2. No unwanted algebraic incidences

For sources `s,t`, the determinant controlling the distance from the point
for `t` to the tangent-direction line for `s` is

```text
D(s,t) = x_s - x_t + y_s (y_t - y_s)
       = a₀_s - a₀_t - 2(w_t - w_s)².
```

Both identities are formalized. If `D(s,t)=0`, taking the field trace makes
the trace-zero terms vanish and gives

```text
Tr((w_t - w_s)²) = 0.
```

For a totally real field, the trace of a square is the sum of the squares of
all real embeddings. The development proves from mathlib's
`trace_eq_sum_embeddings` that this vanishes exactly when the element
vanishes. Therefore `w_t=w_s`, then `a₀_t=a₀_s`, and injectivity of the two
coefficient boxes gives `s=t`. This proves `sourceD_ne_zero`.

### 3. Quantitative separation from the norm

The algebraic integer `D(s,t)` has nonzero rational norm, hence absolute norm
at least one. All conjugates other than the chosen real embedding are bounded
by the house. The file develops the needed house estimates for the explicit
boxes and obtains

```text
1 ≤ |σ(D(s,t))| (H m²)^(d-1)
```

for a field-dependent constant `H`.

The embedded coordinates are translated and anisotropically scaled into
`[0,1]²`. Lines are scaled at the same time. An explicit normal vector is
proved orthogonal to each line direction, and its norm is bounded. Combining
the normal-vector distance estimate with the norm estimate gives separation
at least

```text
(C_K m^(2d))⁻¹
```

for a positive field-dependent constant `C_K`.

### 4. Exactly every sufficiently large cardinality

The source box contains at least `m^(3d-2)` elements. For a requested `n`,
the proof takes

```text
m = ceil(n^(1/(3d-2))).
```

It verifies `n ≤ m^(3d-2)`, embeds `Fin n` into the source box, and restricts
the construction along this embedding. It also proves
`m ≤ 2 n^(1/(3d-2))`. Therefore, for every exponent

```text
α > 2d/(3d-2),
```

the fixed-field construction eventually has separation at least `n^(-α)`.
This is `eventually_configuration_of_fixed_field`.

This ceiling-and-restriction argument is included explicitly so that the
result holds for every `n ≥ n₀`, not merely for the sequence of full box
cardinalities.

### 5. Degrees tending to infinity

No existence of number fields is assumed. For each `k`, the development takes
the maximal real subfield of the cyclotomic field

```text
ℚ(ζ_(2^(k+2))).
```

Using mathlib's cyclotomic degree formula, Euler totient formula for prime
powers, CM-field quadratic-extension result, and the tower law for
finranks, `realCyclotomicField_finrank` proves that this totally real field
has degree exactly `2^k`.

Finally,

```text
2d/(3d-2) = 2/3 + 4/(9d-6)
```

tends down to `2/3`. The Archimedean argument selecting a sufficiently large
power-of-two degree is fully proved in
`exists_cyclotomic_degree_for_exponent`. Applying the fixed-field theorem
with `α = 2/3 + ε` proves the central theorem.

## Relationship to the paper

The development formalizes Theorem 1.1 itself, not Corollary 1.2. The
corollary also uses the previously published upper bound
`Δ_PL(n) ≤ n^(-2/3+o(1))`; that external result is contextual rather than an
ingredient of the paper's new central theorem.

The proof uses the maximal real cyclotomic option explicitly mentioned in
the paper. It replaces the paper's geometry-of-numbers presentation of the
trace-zero slice by an explicit rank-`d-1` sub-box generated from an integral
basis. The cardinality exponent, trace-zero property, non-square-difference
argument, norm bound, and final Euclidean exponent are unchanged. This
variant avoids importing any unformalized lattice-counting theorem while
proving the same statement without hypotheses.

## Completion report

Status: reproduced.

Declared hypotheses beyond the theorem's `ε > 0`: none.

External mathematical theorems used as assumptions: none. Relevant
number-field, cyclotomic, norm/house, Euclidean, and real-asymptotic results
are invoked as proved mathlib theorems.