Factor selection with point-to-degree ratio

Proved

Esgk.n14_factor_selection

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

discrete-geometrydistinct-distances

If point counts $N_i$ sum to $n \ge 1$ and degrees $d_i$ sum to at most $2s$ , some index satisfies $d_i \le 2s$ and $n d_i \le N_i 2s$ . This is the factor-selection step (15.1) of the $n^{1/4}$ additive bound: some carrier factor has high point-to-degree ratio.

Preamble

import Mathlib

Formal statement

namespace Esgk

theorem n14_factor_selection {ι : Type} [Fintype ι] [DecidableEq ι]
    (N d : ι → ℕ) (n s : ℕ) (hn : 1 ≤ n)
    (hN : ∑ i, N i = n) (hd : ∑ i, d i ≤ 2 * s) :
    ∃ i, d i ≤ 2 * s ∧ n * d i ≤ N i * (2 * s) := by sorry

end Esgk

Source

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

View graph