Circle case gives a linear deficiency bound

Proved

Esgk.circle_factor_linear_bound

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

discrete-geometrydistinct-distances

If $N \le 3$ and $2n \le N 2s$ then $n \le 3s$ . A degree-2 carrier factor holds few points, so the deficiency is linear in this branch.

Preamble

import Mathlib

Formal statement

namespace Esgk

/-- Circle branch (§16.1, (16.1)): a degree-2 factor carries at most 3
points, so `n * 2 ≤ N * (2s)` with `N ≤ 3` forces `n ≤ 3s`. -/
theorem circle_factor_linear_bound (n s N : ℕ) (hN3 : N ≤ 3)
    (hcov : n * 2 ≤ N * (2 * s)) : n ≤ 3 * s  := by sorry

end Esgk

Source

Circle linear-bound proof; Lean source artifact: esgk-on3 lean/Esgk/AdditiveExcessArithmetic.lean (Esgk.circle_factor_linear_bound)

View graph