With one colour, validity reduces to $\ell$ -sum-freeness of the whole set

Proved

ModularSchur.k1_partition_iff

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

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

This theorem removes the partition quantifier in the single-colour case.

Let $m$ and $\ell$ be given and let $T \subseteq \mathbb{Z}/m$ be a target set. Then

\big(\exists\, P_0 \text{ a valid } 1\text{-partition of } T\big) \iff T \text{ is } \ell\text{-sum-free modulo } m.

With a single class available there is no freedom: the one class must be $T$ itself, so asking for a valid colouring is asking whether $T$ is already safe.

This is the reduction that turns the $k = 1$ modular Schur number into a question about one explicit set rather than about the existence of a colouring, and every step of the one-colour formula is stated through it.

Preamble

import Definitions.Def_ModularSchurBasic
import Definitions.Def_ModularSchurPartition
import Mathlib

open ModularSchur
open Finset Classical

Formal statement

theorem ModularSchur.k1_partition_iff (m ℓ : ℕ) (T : Finset (ZMod m)) :
    (∃ P : Fin 1 → Finset (ZMod m), IsValidPartition m ℓ 1 T P) ↔
    IsEllSumFree m ℓ T := 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 single-class reduction underlying Section 6. Lean source: https://github.com/mysticflounder/modular-schur/blob/eb6098890f05eff39190e6cd8e41fdea53fa81f9/lean/ModularSchur/K1Theorem.lean#L25-L43

View graph

With one colour, validity reduces to ℓ\ellℓ-sum-freeness of the whole set

With one colour, validity reduces to $\ell$ -sum-freeness of the whole set