Circle branch gives a linear deficiency bound

Proved

Esgk.n14_circle_branch

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

discrete-geometrydistinct-distances

If $N \le 3$ and $2n \le N 2s$ then $n \le 3s$ . This is the circle branch (16.1) of the $n^{1/4}$ bound: a degree-2 factor carries few points.

Preamble

import Mathlib

Formal statement

namespace Esgk

theorem n14_circle_branch (n s N : ℕ) (hN3 : N ≤ 3)
    (hcov : n * 2 ≤ N * (2 * s)) : n ≤ 3 * s := by sorry

end Esgk

Source

Circle-branch proof; Lean source artifact: esgk-on3 lean/Esgk/N14FactorSelection.lean; kernel-checked 2026-09-16