Threshold-failure branch gives a fifth-power deficiency bound

Proved

Esgk.n14_threshold_failure

by mysticflounder · Sep 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

discrete-geometrydistinct-distances

If $N^2 < C^2 d^5$ with $s \ge 1$ , $nd \le N 2s$ and $d \le 2s$ , then $n^2 < 32 C^2 s^5$ . This is the threshold-failure case (16.4) of the $n^{1/4}$ bound, with the published $s > n^{2/5}/2C^{2/5}$ raised to the fifth power to stay in naturals: below the $d^{5/2}$ threshold the deficiency is large.

Preamble

import Mathlib

Formal statement

namespace Esgk

/-- Threshold failure (N14 §16.3, (16.4)): below the `d^(5/2)` threshold,
i.e. `N^2 < C^2 * d^5`, coverage `n * d ≤ N * (2s)` with `d ≤ 2s` forces
`n^2 < 32 * C^2 * s^5` (the `rpow` form `s > n^(2/5)/(2C^(2/5))`
raised to the fifth power). -/
theorem n14_threshold_failure (n s N d C : ℕ) (hs : 1 ≤ s)
    (hcov : n * d ≤ N * (2 * s)) (hN : N ^ 2 < C ^ 2 * d ^ 5)
    (hds : d ≤ 2 * s) : n ^ 2 < 32 * C ^ 2 * s ^ 5  := by sorry

end Esgk

Source

Threshold-failure arithmetic lemma for planar distinct-distance bounds; the Lean proof was kernel-checked on 16 September 2026.

View graph