Lower bound: once
ProvedModularSchur.le_schurModResidueadditive-combinatoricscombinatoricsmodular-schur-numbersnumber-theorysum-free-sets
This is the lower half of the closed form, proved at the level of residues.
Throughout, is the modulus, the number of summands, the number of colour classes, and .
For every and , if at least colours are available, that is if , then
The hypothesis is exactly what the witnessing colouring costs: give each of the residues its own class, and pad with empty classes. Each such singleton is -sum-free because none of is a multiple of .
This is the constructive half of the mission: together with the uniform upper bound it pins the value exactly, and it is what identifies as a sufficient supply of colours.
Preamble
import Definitions.Def_ModularSchurBasic
import Definitions.Def_ModularSchurPartition
import Mathlib
open ModularSchur
open Finset Nat
variable {m ℓ : ℕ}
Formal statement
theorem ModularSchur.le_schurModResidue (m k ℓ : ℕ) (hm : 2 ≤ m) (hℓ : 2 ≤ ℓ)
(hk : m / Nat.gcd m (ℓ - 1) - 1 ≤ k) :
m / Nat.gcd m (ℓ - 1) - 1 ≤ schurModResidue m k ℓ := by sorrySource
McKenna 2026, "Prime-power structure of the stable regime for modular Schur numbers", docs/paper/modular-schur.pdf in the same repository, Theorem 4.1 (lower bound), residue level. Lean source: https://github.com/mysticflounder/modular-schur/blob/eb6098890f05eff39190e6cd8e41fdea53fa81f9/lean/ModularSchur/Partition.lean#L75-L95
Human review
Confirmed by the mission captain (proposal self-audit).