Threshold failure gives a fifth-power deficiency bound

Proved

Esgk.threshold_failure_fifth_power_bound

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$ . Below-threshold points force large deficiency; the published fractional-power form raised to the fifth power keeps everything in naturals.

Preamble

import Mathlib

Formal statement

namespace Esgk

/-- Threshold failure (§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 threshold_failure_fifth_power_bound (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

esgk-on3 lean/Esgk/AdditiveExcessArithmetic.lean (Esgk.threshold_failure_fifth_power_bound)

View graph