Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Complete one-colour formula for all m≥2m \ge 2m≥2 and ℓ≥2\ell \ge 2ℓ≥2

Proved
ModularSchur.schurModResidue_k1_all

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

additive-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 m≥2m \ge 2m≥2 and every ℓ≥2\ell \ge 2ℓ≥2,

schurModResidue(m,1,ℓ)={min⁡ ⁣(ℓ−1,⌊m/ℓ⌋),ℓ≤m,0,ℓ>m and ℓ≡1(modm),1,ℓ>m and ℓ≢1(modm).\mathrm{schurModResidue}(m,1,\ell) = \begin{cases} \min\!\left(\ell - 1, \left\lfloor m/\ell \right\rfloor\right), & \ell \le m, \\ 0, & \ell > m \text{ and } \ell \equiv 1 \pmod m, \\ 1, & \ell > m \text{ and } \ell \not\equiv 1 \pmod m. \end{cases}schurModResidue(m,1,ℓ)=⎩⎨⎧​min(ℓ−1,⌊m/ℓ⌋),0,1,​ℓ≤m,ℓ>m and ℓ≡1(modm),ℓ>m and ℓ≡1(modm).​

The first branch is the regime treated in the literature; the remaining two cover a modulus smaller than ℓ\ellℓ, 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 sorry
Source
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 2≤ℓ≤m2 \le \ell \le m2≤ℓ≤m (Theorem 6.1) and nowhere treats the regime m<ℓm < \ellm<ℓ; 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
  • Endorsed by Shuze Chen · Sep 20, 2026

  • Endorsed by mysticflounder · Sep 20, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, licensed under Apache 2.0.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTermsJoin SlackJoin Zulip© 2026 Prove2Me