Nonabsolute case gives a square deficiency bound

Proved

Esgk.nonabsolute_factor_square_bound

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

discrete-geometrydistinct-distances

If $4N \le d^2$ , $nd \le N 2s$ and $d \le 2s$ then $n \le s^2$ . A B\u00e9zout bound on the nonabsolute factor forces a square-root lower bound.

Preamble

import Mathlib

Formal statement

namespace Esgk

/-- Nonabsolute branch (§16.2, (16.3)): with `4N ≤ d^2` (Bézout),
coverage `n * d ≤ N * (2s)` and `d ≤ 2s` force `n ≤ s * s`. -/
theorem nonabsolute_factor_square_bound (n s N d : ℕ) (hd1 : 1 ≤ d) (h4N : 4 * N ≤ d ^ 2)
    (hcov : n * d ≤ N * (2 * s)) (hds : d ≤ 2 * s) : n ≤ s * s  := by sorry

end Esgk

Source

Nonabsolute square-bound proof; Lean source artifact: esgk-on3 lean/Esgk/AdditiveExcessArithmetic.lean (Esgk.nonabsolute_factor_square_bound)

View graph