Nonabsolute branch gives a square-root bound

Proved

Esgk.n14_nonabsolute_branch

by mysticflounder · Sep 16, 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$ . This is the nonabsolute branch (16.3): B\u00e9zout forces a square-root lower bound.

Preamble

import Mathlib

Formal statement

namespace Esgk

theorem n14_nonabsolute_branch (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-branch proof; Lean source artifact: esgk-on3 lean/Esgk/N14FactorSelection.lean; kernel-checked 2026-09-16

View graph