Prove2Me

The interval up to min⁡(ℓ−1,⌊m/ℓ⌋)\min(\ell-1, \lfloor m/\ell \rfloor) is ℓ\ell-sum-free

Proved
ModularSchur.sumFree_min

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

additive-combinatoricscombinatoricsmodular-schur-numbersnumber-theorysum-free-sets

This is the witness that makes the one-colour formula attainable.

Let m≥2m \ge 2 and 2≤ℓ≤m2 \le \ell \le m, and set N∗=min⁡ ⁣(ℓ−1,⌊m/ℓ⌋)N^{*} = \min\!\big(\ell - 1, \lfloor m/\ell \rfloor\big). Then

{1‾,2‾,…,N∗‾}⊆Z/m is ℓ-sum-free modulo m.\{\overline{1}, \overline{2}, \dots, \overline{N^{*}}\} \subseteq \mathbb{Z}/m \text{ is } \ell\text{-sum-free modulo } m.

At this length the integer sums of ℓ\ell elements drawn from [1,N∗][1, N^{*}] all lie in [ℓ,m][\ell, m], so their residues avoid the interval itself.

This single set realises the one-colour value, so it is the lower bound matching the two upper bounds and the reason the formula is an exact minimum rather than an estimate.

Preamble
import Definitions.Def_ModularSchurBasic
import Definitions.Def_ModularSchurPartition
import Mathlib

open ModularSchur
open Finset Classical
variable {m ℓ : ℕ}
Formal statement
theorem ModularSchur.sumFree_min (hm : 2 ≤ m) (hℓ : 2 ≤ ℓ) (hlm : ℓ ≤ m) :
    IsEllSumFree m ℓ (stableResidues m (min (ℓ - 1) (m / ℓ))) := by sorry
Source
McKenna 2026, "Prime-power structure of the stable regime for modular Schur numbers", docs/paper/modular-schur.pdf in the same repository, the lower-bound witness in the proof of Theorem 6.1. Lean source: https://github.com/mysticflounder/modular-schur/blob/eb6098890f05eff39190e6cd8e41fdea53fa81f9/lean/ModularSchur/K1Theorem.lean#L130-L171

View graph