Complete one-colour formula for all and
ProvedModularSchur.schurModResidue_k1_alladditive-combinatoricscombinatoricsmodular-schur-numbersnumber-theorysum-free-sets
This theorem states the single-colour modular Schur number for every admissible pair, with no restriction relating the modulus and the number of summands.
For every and every ,
The first branch is the regime treated in the literature; the remaining two cover a modulus smaller than , where the answer degenerates to whether the all-ones tuple is already fatal.
This is the single statement a consumer can quote for the one-colour case without checking which regime a given pair falls into, and it closes the single-colour question completely.
Preamble
import Definitions.Def_ModularSchurPartition
import Mathlib
open ModularSchur
open Finset Classical
variable {m ℓ : ℕ}
Formal statement
theorem ModularSchur.schurModResidue_k1_all (m ℓ : ℕ) (hm : 2 ≤ m) (hℓ : 2 ≤ ℓ) :
schurModResidue m 1 ℓ =
if ℓ ≤ m then min (ℓ - 1) (m / ℓ) else if ℓ % m = 1 then 0 else 1 := by sorrySource
Not stated in McKenna 2026, "Prime-power structure of the stable regime for modular Schur numbers", docs/paper/modular-schur.pdf in the same repository -- this is a result of the Lean development only. Prior art: The paper states the one-colour formula only under the hypothesis (Theorem 6.1) and nowhere treats the regime ; this statement is a result of the Lean development going beyond the paper. Lean source: https://github.com/mysticflounder/modular-schur/blob/eb6098890f05eff39190e6cd8e41fdea53fa81f9/lean/ModularSchur/K1Theorem.lean#L315-L323
Human review
Confirmed by the mission captain (proposal self-audit).