$\ell$-sum-free sets modulo $m$

This bundle introduces the residue-level notion of sum-freeness on which the whole modular Schur development rests.

Fix a modulus $m \ge 2$ and a number of summands $\ell \ge 2$, and work in the cyclic group $\mathbb{Z}/m$. A finite subset $C \subseteq \mathbb{Z}/m$ is $\ell$-sum-free modulo $m$ when no $\ell$ of its elements, repetitions allowed, sum to an element of $C$:

the sum and the inequality both taken in $\mathbb{Z}/m$.

For $\ell = 2$ this is the classical sum-free condition behind the Schur numbers; letting $\ell$ vary gives the modular generalisation studied here. Every later definition and theorem in this mission is phrased in terms of this single predicate, so it is the shared vocabulary of the whole tree.

Formalization Note The $\ell$-tuple is a function $f : \mathrm{Fin}\ \ell \to \mathbb{Z}/m$ taking values in $C$, which builds in repetitions allowed automatically, and the sum is the Finset sum over $\mathrm{Fin}\ \ell$.