One colour: for
ProvedModularSchur.schurModResidue_k1additive-combinatoricscombinatoricsmodular-schur-numbersnumber-theorysum-free-sets
This is the exact single-colour modular Schur number in the range the literature posed it for.
For every and every with ,
The two terms are the two ways a single class can fail. The term is the no-wrap regime, where the class is defeated by copies of summing to ; the term is the wrap regime, where some -tuple sums past the modulus and lands back at . Which one binds depends on whether .
This is one of the two regimes of the problem that admit an exact formula, the other being the many-colours regime of the main closed form; the intermediate range has no known formula.
Preamble
import Definitions.Def_ModularSchurBasic
import Definitions.Def_ModularSchurPartition
import Mathlib
open ModularSchur
open Finset Classical
variable {m ℓ : ℕ}
Formal statement
theorem ModularSchur.schurModResidue_k1 (m ℓ : ℕ) (hm : 2 ≤ m) (hℓ : 2 ≤ ℓ) (hlm : ℓ ≤ m) :
schurModResidue m 1 ℓ = min (ℓ - 1) (m / ℓ) := 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 6.1 (the case). Prior art: the paper states "This resolves [DSWH2025, Problem 1, part 3]"; see D'orville, Sim, Wong and Ho, "Modular generalizations of Schur numbers", Integers 25 (2025) #A62, https://math.colgate.edu/~integers/z62/z62.pdf. Lean source: https://github.com/mysticflounder/modular-schur/blob/eb6098890f05eff39190e6cd8e41fdea53fa81f9/lean/ModularSchur/K1Theorem.lean#L173-L200
Human review
Confirmed by the mission captain (proposal self-audit).