Combinatorics

Motivation

A set of integers is sum-free when no two of its members add up to a third. Schur's theorem (1916) says that for every $k$ there is a largest interval $[1,N]$ that can be split into $k$ sum-free classes, and the resulting Schur numbers $S(k)$ are notoriously hard to compute: $S(5) = 160$ was settled only in 2018, by a SAT computation with a machine-checked proof certificate.

Replacing "adds up to" by "adds up to, modulo $m$" gives a family that behaves very differently. Modular Schur numbers were introduced by Chappelon, Revuelta Marchena and Sanz Domínguez, who settled the moduli $m \in \{1,2,3\}$ and proved the universal bound $S_m(k,\ell) \le m-1$ (Electron. J. Combin. 20(2) (2013) #P61). D'orville, Sim, Wong and Ho then closed $m \in \{4,5,6,7\}$ by residue case analysis and posed the general modulus as an open problem (Integers 25 (2025) #A62, their Problem 1). Each additional modulus had cost a separate case analysis, and the case analysis grew with $m$.

The timeline matters for reading what follows. The 2013 paper supplies the universal cap. The 2025 paper supplies a singleton criterion (its Theorem 4) and a divisibility obstruction (its Corollary 3), and applies the latter only in the coprime case $\gcd(m,\ell-1)=1$ (its Corollary 5). What remained was to optimise that obstruction over every residue rather than only in the coprime case, which is what collapses the whole family to one formula.

Setting

Fix integers $m \ge 2$, $\ell \ge 2$ and $k \ge 1$. A set $S$ of integers is $\ell$-sum-free modulo $m$ when there are no $x_1, \dots, x_\ell \in S$ and $y \in S$, repetitions among the $x_i$ allowed, with

$$x_1 + \cdots + x_\ell \equiv y \pmod m .$$

The repetition clause is not a technicality: a single element can make its whole class unsafe. The modular Schur number $S_m(k,\ell)$ is the greatest $N \ge 0$ such that the interval $[1,N]$ can be partitioned into at most $k$ classes, each $\ell$-sum-free modulo $m$. A partition into such classes is called valid.

Two derived quantities carry the whole story. Write

$$d = \gcd(m, \ell - 1), \qquad n = \frac{m}{d} .$$

Then $dn = m$ exactly, and $d \mid (\ell - 1)$ by construction. All Lean statements in this mission use these same names.

Formalization targets

Goal: the closed form in the many-colours regime

$$S_m(k,\ell) = \frac{m}{\gcd(m,\ell-1)} - 1 = n - 1 \qquad \text{for all } m \ge 2,\ \ell \ge 2,\ k \ge n-1 .$$

Closed form here means something precise: the value is produced from $m$ and $\ell$ by one gcd, one division and one subtraction, with no search over colourings, no recursion, and no case split on $\ell \bmod m$. The statement fixes no constants and no modulus, so it is not invalidated by any later refinement of the threshold in $k$.

The single-colour value

$$S_m(1,\ell) = \min\!\left(\ell - 1, \left\lfloor \frac{m}{\ell} \right\rfloor\right) \qquad (2 \le \ell \le m),$$

together with the complementary regime $m < \ell$, where the value is $0$ if $\ell \equiv 1 \pmod m$ and $1$ otherwise. The two together give a value for every admissible pair $(m,\ell)$ at $k=1$, and the tree carries that combined formula at the residue level and at the integer level.

Significance

What the results give. One expression replaces an open-ended sequence of per-modulus case analyses. The moduli $m \in \{1,2,3\}$ of the 2013 paper and $m \in \{4,5,6,7\}$ of the 2025 paper are specialisations, and every remaining modulus is covered at once in the stated range of $k$.

The mechanism is a single self-defeating value. Take $\ell$ copies of $n$: they sum back to $n$ modulo $m$, so the lone class $\{n\}$ already breaks the rule, while every smaller value is safe. That one observation supplies a matching upper and lower bound.

• The upper bound is uniform in $k$. Adding colours never raises the value past $n-1$, which is what makes the formula stable.
• The lower bound costs $n-1$ colours, one per safe residue. Identifying the least sufficient number of colours is where the subject is still open.

Status of the tree, stated precisely. Everything listed under Formalization targets is both proved and machine-checked.

• 21 theorems and 3 definition bundles, each with a complete Lean proof verified by this platform.
• Axiom-clean: each closure is contained in {propext, Classical.choice, Quot.sound}.
• This mission therefore publishes a finished development rather than an open call on its stated goal.
• What is genuinely open is listed under Difficulty below, and is not part of the verified tree.

Relation to the accompanying paper. The paper states the single-colour value only under $2 \le \ell \le m$. Three results in the tree go beyond it: the complementary regime $m < \ell$, and the combined formula covering every $m \ge 2$ and $\ell \ge 2$, stated once at the residue level and again at the integer level. Two further results, the coset-cardinality bounds, are supporting work of the Lean development and are not numbered results of the paper. Each theorem's source field records which of these it is.

Difficulty

The threshold in $k$ is not $n-1$

The obvious attack on the general modulus is to guess that only singletons can be safe classes. The threshold in $k$ would then be exactly $n-1$, and the problem would close for all $k$ at once. That guess is false.

Take $m = 12$ and $\ell \equiv 11 \pmod{12}$, so $d = 2$ and $n = 6$. The two-element set $\{1,5\}$ is $\ell$-sum-free modulo $12$, and three colours then suffice where the singleton count would demand five.

So the least $k$ at which the closed form takes hold, written $k_0(m,\ell)$, is not $n-1$ in general. What is known about it:

• Prime moduli. $k_0(p,\ell) = p-1$ for every $\ell \ge p-1$ with $\ell \not\equiv 1 \pmod p$.
• Composite moduli. Bracketed above and below, but not determined.

A correction to the published prime-power formula

Theorem 8 of D'orville, Sim, Wong and Ho gives a three-branch formula at prime-power moduli. Its middle branch is false. The correction is stated here in full because it bears directly on the threshold.

• The counterexample. At $p = 2$, $i = 3$, $k = 3$ and $\ell = 8$ that branch gives $S_8(3,8) = 5$, while the correct value is $S_8(3,8) = 7$.
• Where the proof fails. In the supporting Lemma 2(2) of that paper. The pair $a = 2$, $b = 6$ satisfies every hypothesis of that lemma at $p = 2$, $i = 3$, $\ell = 8$, yet $\{2,6\}$ is $8$-sum-free modulo $8$.
• The replacement result.

$$S_{p^i}(k,\ell) = p^i - 1 \qquad \text{for } p \text{ prime},\ i \ge 1,\ \ell \ge 2,\ p \nmid (\ell - 1), \text{ and every } k \ge i(p-1) .$$

It is proved from a valuation-layer colouring that consumes $i(p-1)$ classes, together with the universal cap. The hypothesis $p \nmid (\ell-1)$ forces $d = 1$ and $n = p^i$, so the replacement reaches the goal theorem's value at $k \ge i(p-1)$ in place of $k \ge p^i - 1$, and it contradicts the printed middle branch for infinitely many triples $(p, i, \ell)$.

Status of that correction, stated precisely.

• It is a prose proof in a draft note, listed under Selected references below and readable in full there.
• It is not formalized, and it is not part of this mission's verified tree.
• Nothing in the verified tree depends on it.
• It is recorded here because a reader who compares this mission against the 2025 paper will otherwise meet the contradiction with no explanation. Formalizing it is the subject of a separate mission.

The intermediate regime

For $1 < k < n-1$ the classes must be simultaneously large and $\ell$-sum-free, and no formula is known. The value is empirically eventually periodic in $\ell \bmod m$ for fixed $k$, verified through $m \le 13$.

None of these open directions is weakened by the goal theorem, which deliberately assumes enough colours to avoid the question.

Formalization scope

Two levels of statement

Two levels appear in the tree, and the distinction between them is the first thing to fix.

• At the integer level the objects are the integers $1, \dots, N$ themselves.
• At the residue level they are their classes modulo $m$, which in Lean is the type ZMod m: Mathlib's type of residues modulo $m$, a commutative ring with exactly $m$ elements for $m \ge 1$, carrying the reduction map from $\mathbb{Z}$ and the arithmetic that map preserves.

Working in ZMod m turns "adds up to, modulo $m$" into a plain equation instead of a divisibility side condition, and it makes every colour class a subset of a finite type.

Conventions

The development works residue-by-residue in ZMod m and commits to the following conventions, all of which are silent in the prose and load-bearing in Lean.

• $\ell$-tuples are functions Fin ℓ → ZMod m valued in the class. This builds in "repetitions allowed" rather than leaving it to a side condition.
• Classes are Finsets, so finiteness is structural.
• A valid partition is a structure with four fields: covering, pairwise disjointness, containment in the target set, and $\ell$-sum-freeness of each class.
• Empty classes are permitted. This is what makes "at most $k$" and "exactly $k$" interchangeable once any colouring exists.

The two numbers, and the cap in their definition

Both a residue-level and an integer-level number are defined, and a reduction theorem proves them equal for every $m \ge 2$. Bounds are proved on the residue side and quoted on the integer side.

Both are defined with Nat.findGreatest against the bound $m-1$. That cap is neither an approximation nor a trivialising choice: a separate theorem shows any $N$ admitting a valid partition satisfies $N \le S_m(k,\ell)$ with no hypothesis on $N$, because $N \ge m$ admits no valid partition at all. A reader checking for a vacuous formalization should also note that the goal is an equality, not a bound, so it cannot be satisfied by weakening a hypothesis.

Reusable beyond this mission

• the residue-reduction bridge;
• the singleton criterion;
• the two coset-cardinality bounds, which are pure counting statements about subsets of a cyclic group whose differences lie in a proper subgroup.

Contributions welcome on the open directions named under Difficulty, in particular any lowering of the threshold in $k$ toward $k_0$, and a closed form for $k_0$ at composite moduli.

Selected references

• J. Chappelon, M. P. Revuelta Marchena, M. I. Sanz Domínguez, Modular Schur numbers, Electron. J. Combin. 20(2) (2013) #P61. https://doi.org/10.37236/2374 (also arXiv:1306.5635)
• J. D'orville, K. A. Sim, K. B. Wong, C. K. Ho, Modular generalizations of Schur numbers, Integers 25 (2025) #A62. https://math.colgate.edu/~integers/z62/z62.pdf
• M. J. H. Heule, Schur number five, AAAI 2018. arXiv:1711.08076
• A. McKenna, A correction to a prime-power formula for modular Schur numbers, 2026. Draft note, not submitted for publication. Released in the repository below on 2026-09-20: PDF · Markdown source
• A. McKenna, Prime-power structure of the stable regime for modular Schur numbers, 2026. Lean development and paper: https://github.com/mysticflounder/modular-schur

Motivation

The first three missions in this programme settle the ordinary $3\times3$ magic squares end to end: Mission I proved MacMahon's count $M_{3}(3e)=2e^{2}+2e+1$, Mission II his semi-magic count $H_{3}(t)=3\binom{t+3}{4}+\binom{t+2}{2}$, and Mission III classified the normal squares (Lo Shu uniqueness). All three work with the plain magic condition.

This mission counts the two special classes that are singled out by requiring more than magicness, in the opposite directions one expects:

• the panmagic (pandiagonal) squares, whose broken diagonals must also have the magic sum — a strengthening so strong that for order three the whole family collapses;
• the symmetric magic squares, whose array must equal its transpose — a symmetry that only removes a few conditions and leaves a genuine family.

Writing $P_{3}(t)$ and $S_{3}(t)$ for the two counting functions, the goal is to determine both for every line sum $t$:

$$P_{3}(t)=\begin{cases}1,&3\mid t\\ 0,&3\nmid t\end{cases}, \qquad S_{3}(t)=\begin{cases}\dfrac{2t}{3}+1,&3\mid t\\[2mm] 0,&3\nmid t\end{cases}.$$

Setting

Everything is built on the vocabulary of MagicSquares (Mission I):

• IsPanMagic — semi-magic, and every broken diagonal in both directions has the line sum, indices read modulo $n$;
• IsSymmetric — $M_{ij}=M_{ji}$;
• panMagicCount, symmetricMagicCount — the cardinalities of the two filtered finsets of arrays over Fin (t+1), which is lossless because every entry of a square of line sum $t$ is at most $t$.

The new definition module MagicSquaresSpecial3 records the two explicit shapes that the proofs produce: constSquare3 e (the array all of whose entries are $e$, read over the ambient Fin (3e+1)) and

$$\mathrm{symmMagic3}(e,a)=\begin{pmatrix} a & 2e-a & e\\ 2e-a & e & a\\ e & a & 2e-a\end{pmatrix},$$

together with the parameter set symmParamSet e $=\{0,\dots,2e\}$ and its cardinality symmParamCount e.

Formalization targets

Goal — the complete count

special_three_count: for every natural number $t$, the pair of equalities displayed above. The proof splits on $3\mid t$ and reduces to four child nodes.

The route

1. Panmagic collapses to the constant square (pan_three_card). Writing the array as $a,b,c;d,m,f;g,h,i$, the twelve line equations form a linear system whose only nonnegative solution is $a=b=\dots=i=e$. So $P_{3}(3e)=1$.
2. Symmetry is classified by a corner (symmetric_magic_three_classify). Symmetry identifies three pairs of entries, leaving five free cells and five line equations; the anti-diagonal $2c+m=3e$ forces $c=m=e$, and the rows give $M=\mathrm{symmMagic3}(e, M_{00})$.
3. A bijection onto an interval (symm_three_bij). Sending a symmetric magic square of line sum $3e$ to $M_{00}$ is a bijection onto $\{0,1,\dots,2e\}$; hence $S_{3}(3e)=2e+1$.
4. The divisibility obstruction (pan_three_otherwise, symm_three_otherwise). Both classes consist of magic squares, and an order-three magic square has centre $t/3$ (center_of_order_three), so $3\nmid t$ forces both counts to vanish.

Significance

The results. The three order-three counts behave completely differently in the same parameter: MacMahon's $M_{3}$ is quadratic, the symmetric count is linear, and the panmagic count is constant. That contrast is the point of the order-three study — order three is small enough to be completely understood, and the special classes show how differently the two natural strengthenings of the magic condition act. It is also exactly what is lost at order four, where no closed form is known for any of the three.

Formalizing them. The mathematical content is elementary, but the two classes require genuinely different proof techniques, which is what makes the mission worth formalizing:

• For the panmagic case the six broken diagonals together with the rows and columns give a subtraction-free linear system over $\mathbb{N}$, so the uniqueness step is a single omega call. The only work is exposing the twelve equations, which requires reducing the index arithmetic $i+k$ and $\mathrm{rev}(i)+k$ on Fin 3.
• For the symmetric case the answer is a family, and the admissibility bound $a\le 2e$ is a statement about truncated subtraction: the entry $2e-a$ is computed in $\mathbb{N}$, so the row identity $a+(2e-a)+e=3e$ is satisfiable precisely for $a\le 2e$. Formalizing the bijection therefore needs an honest treatment of that truncation, where the panmagic case needs none.

Difficulty

Truncated subtraction, in the admissibility direction. The classification M = symmMagic3 e (M 0 0) is true for every $M$, without any bound on $M_{00}$; the bound only appears when asking which members of the family are squares of line sum $3e$. Keeping those two statements apart is what makes the bijection proof manageable: classification is a pure omega computation, while admissibility is a one-line argument that $a+(2e-a)=2e$ forces $a\le 2e$.

Finite but not decidable. panMagicCount and symmetricMagicCount are cardinalities of filtered finsets over a function type, so the proofs cannot be decide or norm_num — the platform forbids native_decide in any case. Both counting theorems are therefore stated as Finset.card_bij / card_eq_one arguments over explicit bijections, not as finite evaluations.

Formalization scope

• The in-scope statements are the two closed forms for all $t$, together with the classification of the symmetric family that the bijection is built on.
• Parametrization follows MacMahon; the symmetric shape is the diagonal slice $c=e$ of his two-parameter family, which is why the count drops from quadratic to linear.
• Nothing here re-proves Mission I: the divisibility obstruction is inherited from the already-proved center_of_order_three.
• Reusable beyond this mission: the order-three classification of symmetric magic squares, the observation that panmagic order-three squares are exactly the constant ones, and the technique of discharging twelve-index linear systems over Fin 3 with a single omega.

Selected references

• P. A. MacMahon, Combinatory Analysis, Vol. II, Cambridge University Press, 1916.
• M. Beck, T. Cohen, J. Cuomo and P. Gribelyuk, The number of "magic" squares, cubes and hypercubes, Amer. Math. Monthly 110 (2003), 707--717. https://arxiv.org/abs/math/0201013
• W. S. Andrews, Magic Squares and Cubes, 2nd ed., Dover, 1960.
• H. Behforooz, Symmetric and panmagic squares (survey of the symmetry properties of magic squares), and the standard pandiagonal literature.

Motivation

Additive combinatorics studies what arithmetic structure follows from statistical signals. The Balog–Szemerédi–Gowers theorem is its central regularity statement: a pair of finite sets with large additive energy (many additive quadruples) contains large subsets whose sumset is small. Balog and Szemerédi proved the first version in 1994 using the regularity lemma, which gave a tower-type dependence between the parameters; Gowers obtained a polynomial dependence in 1998. The theorem powers results across the field — from sum-product estimates to the structure of sets with small doubling — and its proof assembles three reusable machines: dependent random choice, the popular-sum graph, and Ruzsa calculus.

Setting

Work in an arbitrary abelian group $G$ (Lean: AddCommGroup G). For finite $X, Y \subseteq G$, the additive energy $E(X,Y)$ counts quadruples $(x,x',y,y')$ with $x + y = x' + y'$; the trivial maximum is $|X|^3$ when $|X| = |Y|$. The sumset $X + Y$ is $\{x + y\}$, and the difference set $X - Y$ is defined pointwise. A set has small doubling when $|X + X|$ is linear in $|X|$. The Lean development uses Finset.addEnergy and Finset.addConvolution from Mathlib.

A bipartite graph here is an edge set $E$ of type Finset (G × G) with $E \subseteq A \times^s B$, not a Mathlib SimpleGraph; solvers should state graph hypotheses that way. Given such an $E$, the partial sumset $A +_E B$ is $\{a + b : (a,b) \in E\}$, following Tao–Vu Definition 2.28.

Target

The mission goal is the two-set (equal-cardinality) form:

$$E(X,Y) \ge \eta |X|^3 \implies \exists X' \subseteq X, Y' \subseteq Y,\ |X'|,|Y'| \ge c|X|,\ |X' - Y'| \le C|X|.$$

This statement is assembled from the sources rather than quoted from them: Tao–Vu Lemma 2.30 supplies the energy-to-graph step, Fox–Sudakov §5.1 (the same theorem as Tao–Vu Theorem 2.29) supplies the graph-level bound, and Ruzsa calculus converts a sumset bound into the difference-set bound above. No cited work states this exact form, and the goal deliberately keeps $c$ and $C$ existential; the explicit-constant variant is proved separately in the mission with $c = \eta/16$.

The four milestones follow the sources' own numbering and are, in dependency order, Fox–Sudakov Lemma 5.1, Fox–Sudakov Lemma 5.2, the Fox–Sudakov §5.1 / Tao–Vu Theorem 2.29 graph bound with explicit constants, and Tao–Vu Lemma 2.30. The first three lie on the goal's proof path; the fourth is the reusable packaging of the energy-to-graph step.

Significance

The result converts a purely statistical hypothesis (many additive quadruples) into genuine algebraic structure (a large subset with a small difference set) with polynomial losses — the step that makes energy methods usable. It is a standard tool behind quantitative Freiman-type arguments.

Formalizing it matters because the constants are the content: the development tracks explicit constants through dependent random choice (graph level $c = \delta/8$ and $C = 2^{13}K^3/\delta^5 + 2^{12}/\delta^5$; energy level $c_0 = \eta/16$ and $C_0 = 2^{13}(4/\eta)^3/(\eta/2)^5 + 2^{12}/(\eta/2)^5$), which paper proofs often leave implicit. Fox–Sudakov state the application for sets of integers; the formalization is over an arbitrary AddCommGroup, with no further hypothesis on the group. Mathlib at the pinned revision (v4.33.1) contains no BSG statement, so this fills a genuine upstream gap.

Difficulty

The hard step is dependent random choice: sampling a random vertex subset of the popular-sum graph must simultaneously keep many vertices and keep the induced subgraph dense, and the two requirements fight each other. The naive first idea — take the densest neighborhood — loses control of the vertex count; the fix is a two-stage Markov-plus-payoff selection whose density analysis needs the exact path-count lower bound, not just an order estimate.

Two places where the formalization departs from Fox–Sudakov are recorded on the affected statements rather than hidden: the length-three path count admits degenerate paths (the source's $a' \ne a$ and $b' \ne b$ terms are dropped, which weakens the conclusion and is sound for the BSG use), and the density parameter is instantiated at a guaranteed lower bound rather than the exact edge density.

Formalization scope

Sets are Finset G in an AddCommGroup G with DecidableEq; energy is Finset.addEnergy; graphs are edge sets Finset (G × G), with the pointwise sumset and difference operations from open scoped Pointwise. Density hypotheses are stated with explicit real constants. The counting lemmas at the bottom of the development (sum_addConvolution_eq_card_product, path3_count_le_triple_rep_count, restricted_sumset_via_multiplicity) are unconditional; the statements that need them carry the nonemptiness, equal-cardinality and density hypotheses that exclude degenerate zero-energy configurations. Welcome contributions: the single-set polynomial Freiman–Ruzsa consequences, and non-abelian variants.

Selected references

• A. Balog and E. Szemerédi, A statistical theorem of set addition, Combinatorica 14 (1994), 263–268.
• W. T. Gowers, A new proof of Szemerédi's theorem for arithmetic progressions of length four, Geom. Funct. Anal. 8 (1998), 529–551.
• J. Fox and B. Sudakov, Dependent random choice, Random Structures & Algorithms 38 (2011), 68–99 (Lemmas 5.1/5.2 and §5.1 BSG application).
• T. Tao and V. Vu, Additive Combinatorics, Cambridge Univ. Press (2006), Definition 2.28 (partial sumsets), Theorem 2.29 (BSG, p. 79) and Lemma 2.30 (energy to partial sumset, p. 80).
• C. Reiher and T. Schoen, Note on the theorem of Balog, Szemerédi, and Gowers, Combinatorica 44 (2024), no. 3, 691–698 (arXiv:2308.10245).
• I. Ruzsa's inequalities via Mathlib's Finset.pluennecke_ruzsa_inequality_nsmul_add; see G. Petridis, New proofs of Plünnecke-type estimates for product sets in groups, Combinatorica 32 (2012), 721–733 (arXiv:1101.3507).
• McKenna, Lean formalization (mathlib-only, axiom-clean), lean-formalizations, modules Combinatorics/Additive/BalogSzemerediGowers and BSGEnergyToGraph.

Motivation

The first two missions in this programme counted order-three squares. Mission I proved MacMahon's magic count $M_{3}(3e)=2e^{2}+2e+1$ and Mission II his semi-magic count $H_{3}(t)=3\binom{t+3}{4}+\binom{t+2}{2}$. What neither does is classify: counting tells you how many squares there are, but not what they look like.

This mission closes that gap for the most classical case of all. A normal magic square of order three is a $3\times3$ array containing each of $1,2,\dots,9$ exactly once, whose rows, columns and two main diagonals all sum to the magic constant $15$. The statement to be proved is the uniqueness of the Lo Shu square:

every normal magic square of order three is one of the eight images of $\begin{pmatrix}4&9&2\\3&5&7\\8&1&6\end{pmatrix}$ under the symmetry group of the square.

In particular there are exactly $8$ of them, and they form a single orbit under the dihedral group $D_{4}$.

Setting

MacMahon's parametrization (already formalized in MagicSquaresParam3) writes every order-three magic square of line sum $3e$ as

$$\mathrm{mkMagic3}(e,a,c)= \begin{pmatrix} a & 3e-a-c & c\\ e+c-a & e & e+a-c\\ 2e-c & a+c-e & 2e-a \end{pmatrix},$$

with $(a,c)$ ranging over the finite admissible set paramSet e. For a normal square the magic constant is $15$, so $e=5$ and the centre entry is $5$.

Normality (IsNormal) means every entry lies in $[1,9]$ and the nine entries are pairwise distinct — equivalently, they are a permutation of $1,\dots,9$.

Formalization targets

Goal — Lo Shu uniqueness

\\#\\{(a,c)\in \\mathrm{paramSet}\\ 5 : \\mathrm{mkMagic3}(5,a,c)\\ \\text{is normal}\\} = 8,

together with the identification of those eight parameter pairs. By the bijection magic_three_param_bij this is exactly the statement that there are eight normal magic squares of order three, i.e. that Lo Shu is unique up to the symmetry group of the square.

The route

1. Normality bounds the parameters. If $\mathrm{mkMagic3}(5,a,c)$ is normal then $1\\le a\\le 9$ and $1\\le c\\le 9$, because $a$ and $c$ are corner entries. This reduces the classification to a finite search over $81$ pairs.
2. Classification (magic_three_normal_classify). Within that range, $\mathrm{mkMagic3}(5,a,c)$ is normal exactly when $(a,c)$ is one of

$$\\{(2,4),(2,6),(4,2),(4,8),(6,2),(6,8),(8,4),(8,6)\\}.$$

The eight surviving pairs are precisely those with $a,c$ distinct corners of the Lo Shu square; the excluded ones are those with $a+c=10$, for which the $(2,1)$ entry $a+c-5$ collides with the centre $5$. 3. Converse (magic_three_normal_converse). Each of the eight pairs really does give a normal square.

Significance

The result itself. The uniqueness of Lo Shu is the oldest non-trivial classification in combinatorics — it is the order-three case of the classification problem for magic squares, and the reason $n=3$ is special: for $n=4$ there are $880$ normal squares (up to symmetry) and for $n\ge 5$ no classification is known. Formalizing it shows that the counting machinery of Missions I and II can be turned around and used as a classification tool: the parametrization plus a finite verification give the complete list, not just the cardinality.

Formalizing it. The whole proof is a finite case check over $81$ parameter pairs, so the mathematical content is small and the formalization difficulty is concentrated in making the finiteness usable. Two things have to be arranged before automation can see the problem:

• IsNormal is stated with a Function.Injective, which is not decidable as stated; it must first be rewritten into an explicit conjunction of entrywise bounds and pairwise inequalities over Fin 3.
• The quantifiers over Fin 3 do not unfold by simp alone; one needs Fin.forall_fin_succ to expand them before norm_num can decide the $81$ resulting ground instances.

Difficulty

Finiteness must be manufactured. Nothing in IsNormal mentions a bound on $a$ or $c$, so the first step is to derive $1\le a,c\le 9$ from the entrywise bounds of normality. Skipping it leaves an infinite search that interval_cases cannot start.

Truncated subtraction. The parametrization is written over $\mathbb{N}$, so entries such as $a+c-5$ and $15-a-c$ truncate at zero. Every ground instance must be evaluated with the truncation in place — which is why the classification is carried out by evaluating the actual entries rather than by manipulating symbolic inequalities.

Formalization scope

• Normal means: entries in $[1,n^{2}]$ and pairwise distinct (IsNormal).
• The classification is over MacMahon parameters, so it inherits the parametrization of MagicSquaresParam3 and the bijection of Mission I.
• Trivializing formalizations are ruled out: the goal is not a declaration that some finite set has eight elements, but a derived classification — normality must be characterized by an explicit list of parameter pairs.
• Reusable beyond this mission: the decidable reformulation of IsNormal for Fin 3 (and the Fin.forall_fin_succ technique for unfolding finite quantifiers), the list of the eight Lo Shu parameters, and the order-three classification itself.

Selected references

• P. A. MacMahon, Combinatory Analysis, Vol. II, Cambridge University Press, 1916.
• M. Beck, T. Cohen, J. Cuomo and P. Gribelyuk, The number of "magic" squares, cubes and hypercubes, Amer. Math. Monthly 110 (2003), 707--717. https://arxiv.org/abs/math/0201013
• W. S. Andrews, Magic Squares and Cubes, 2nd ed., Dover, 1960 (the classical enumeration for $n=4$).

Motivation

Set cover is the standard worked example of the primal-dual method, and Chapter 2 of Buchbinder's thesis uses it that way: it is where the machinery of §2.1 is first turned on a concrete NP-hard problem. Two analyses appear. The greedy algorithm, analysed by dual fitting, buys the set with the best cost-per-newly-covered-element ratio and charges the price to the elements it covers; the resulting element prices form an infeasible dual that becomes feasible after scaling by $H_n$. The primal-dual algorithm instead raises the price of an uncovered element until some set's constraint goes tight, buys that set, and repeats; the resulting dual is feasible, and each bought set is paid for by elements of frequency at most $f$, giving an $f$-approximation.

Both analyses have the same shape, and it is the shape that matters for the rest of the series: the algorithm never sees the optimum. It maintains a dual solution, and the approximation ratio falls out of comparing the primal it built against the dual it accumulated.

Setting

An instance consists of a finite type $E$ of elements, a finite type $S$ indexing available sets, an assignment $s \mapsto A_s \subseteq E$, and a nonnegative cost $c : S \to \mathbb{R}$. Every element is assumed to lie in at least one available set; the source leaves this implicit, and without it no cover exists and the approximation statements are vacuous. The covering LP and its packing dual are

$$(P)\quad \min \sum_{s} c_s x_s \ \text{ s.t. } \sum_{s : e \in A_s} x_s \ \ge\ 1 \ \ (\forall e \in E), \quad x \ge 0,$$ $$(D)\quad \max \sum_{e} y_e \ \text{ s.t. } \sum_{e \in A_s} y_e \ \le\ c_s \ \ (\forall s \in S), \quad y \ge 0.$$

The frequency of an element is the number of sets containing it, and $f$ denotes the maximum frequency over all elements.

The two standing assumptions — nonnegative costs, and every element lying in some available set — are carried by a bundled SetCoverInstance, not passed as loose hypotheses. Every source-facing statement in the mission takes such an instance and reads those facts off its fields, so none of them can be instantiated at data violating either. The two indicator lemmas are the exceptions and are labelled as generalized assisting results: one has no cost function in scope at all, and the other's hypothesis that a given $C$ covers is strictly stronger than coverability of the family.

Costs are permitted to be zero and the ground type is permitted to be empty. No Nonempty E hypothesis appears anywhere; when $E$ is empty, $f = 0$ and the $f$-approximation bound reads $\mathrm{cost}(C) \le 0$, which the certificate's tightness clause forces to be $0 \le 0$ rather than anything false.

Formalization targets

The results are stated about certificates, not about executable algorithms. This is the central modelling decision of the mission and it is deliberate: the mathematical content of the source's proofs is entirely a statement about the invariants the output satisfies, and separating that from the question of whether a particular procedure produces such output keeps each half provable on its own.

A primal-dual certificate is a pair $(C, y)$ where $C \subseteq S$ covers $E$, $y$ is dual-feasible, and every $s \in C$ has a tight dual constraint, $\sum_{e \in A_s} y_e = c_s$.

Goal — the primal-dual $f$-approximation

For any primal-dual certificate $(C,y)$ and any fractional cover $x$,

$$\sum_{s \in C} c_s \ \le\ f \cdot \sum_{s \in S} c_s x_s .$$

Since this holds against every fractional cover, it holds in particular against an optimal one, so the cover $C$ costs at most $f$ times the fractional optimum and a fortiori at most $f$ times the integral optimum.

The double-counting step

The one substantive step of the goal is split out as its own target: for a primal-dual certificate,

$$\sum_{s \in C} c_s \ \le\ f \cdot \sum_{e \in E} y_e .$$

Tightness rewrites the cover's cost as a double sum over chosen sets and their elements; exchanging the order groups it by element, each charged at most $f$ times. With this and weak duality, the goal is two lines.

The greedy bound

A greedy certificate at ratio $\rho$ is a cover $C$ and a nonnegative $y$ with $\sum_{s \in C} c_s = \sum_{e} y_e$ and $\sum_{e \in A_s} y_e \le \rho\, c_s$ for every $s$. For such a certificate and any fractional cover $x$,

$$\sum_{s \in C} c_s \ \le\ \rho \cdot \sum_{s} c_s x_s .$$

Instantiating $\rho = H_n$ is what recovers the source's greedy guarantee; the harmonic bound itself is already in Mathlib.

Set-cover weak duality and LP attainment

Every dual packing is bounded by every fractional cover, $\sum_e y_e \le \sum_s c_s x_s$; the fractional optimum is at most the integral optimum; and both optima are attained, not merely bounded below. Attainment of the fractional optimum is a genuine linear-programming fact and is the hardest supporting item in the mission.

Significance

This is where the series first converts a dual-feasibility invariant into an approximation ratio on a concrete combinatorial problem, and the two certificate predicates are reused verbatim by the online covering missions later in the series. Set cover approximation has, as far as we can determine, no prior formalization in Mathlib or in any public Lean library: there is no set-cover problem statement, no greedy analysis, and no $f$-approximation result to build on.

Difficulty

The two certificate bounds are finite-summation arguments of moderate length — the work is in a double-counting step that reindexes a sum over chosen sets into a sum over elements, weighted by frequency. Attainment of the fractional optimum is different in kind: it needs a compactness or vertex argument about the covering polytope and is the item most likely to need real work. Zero-cost sets are permitted throughout, so any later algorithm definition that divides by a cost must handle that case explicitly.

Formalization scope

Definitions cover §2.2 of the source, excluding §2.2.2 (randomized rounding), which is deferred to a separate mission because its expected-cost and failure-probability analysis is measure-theoretic and shares no infrastructure with the deterministic results.

Two theorems are not in this mission: that the greedy algorithm produces a greedy certificate, and that the primal-dual algorithm produces a primal-dual certificate. Those require defining the algorithms and proving termination and coverage, and are planned as a second wave. Until that wave lands, the source's Theorems 2.4 and 2.6 should not be described as fully formalized — what this mission establishes is the certificate-to-ratio half of each.

Selected references

• Niv Buchbinder, Designing Competitive Online Algorithms via a Primal-Dual Approach, PhD thesis, Tel Aviv University, 2008, §2.2, pp. 10–14. https://www.tau.ac.il/~nivb/download/phd-thsis.pdf
• Vijay V. Vazirani, Approximation Algorithms, Springer, 2001, Chapters 2 and 15 — the standard treatment of the greedy and primal-dual set-cover analyses.

Motivation

This is the second mission in the magic-squares formalization programme, and it takes up the case the first one deliberately left open.

Counting semi-magic squares — arrays of nonnegative integers whose rows and columns all share a common line sum, with the diagonals unconstrained — is the "honest" version of the enumeration problem. For order three the magic count $M_{3}(t)$ (mission I) is only a quasi-polynomial: it vanishes unless $3\mid t$ and equals $2e^{2}+2e+1$ on $t=3e$. The semi-magic count $H_{3}(t)$ has no such periodicity. MacMahon computed it in 1915:

$$H_{3}(t)\;=\;3\binom{t+3}{4}+\binom{t+2}{2}.$$

It is an honest polynomial in $t$ of degree $4=(3-1)^{2}$, and that degree is not an accident: Ehrhart and Stanley proved that for every order $n$ the function $H_{n}(t)$ is a polynomial of degree $(n-1)^{2}$ satisfying the reciprocity law $H_{n}(-n-t)=(-1)^{n-1}H_{n}(t)$. The order-three formula above is the smallest nontrivial instance of that theorem, and the only one small enough that every step of the derivation can still be exhibited explicitly.

So this mission is the natural companion to mission I: same objects, same platform vocabulary, but the counting step is genuinely harder — the parameter space is four-dimensional rather than two, and the parametrization is not injective until it is normalized.

Setting

Fix $n$ and a line sum $t$. A square of order $n$ is an $n\times n$ array $M$ of nonnegative integers.

• $M$ is semi-magic with line sum $t$ if every row and every column sums to $t$. No condition is imposed on the two diagonals, and entries need not be distinct.
• $H_{n}(t)$ is the number of such squares. Every entry is at most $t$, so $H_{n}(t)$ is the cardinality of a finite set.

For $n=3$ the whole family is governed by the six permutation matrices. Split them into the three even ones — the identity and the two $3$-cycles — whose supports are the transversals

$$D=\{00,11,22\},\qquad E=\{01,12,20\},\qquad F=\{02,10,21\},$$

and the three odd ones — the transpositions — with supports

$$A=\{00,12,21\},\qquad B=\{02,11,20\},\qquad C=\{01,10,22\}.$$

Adding them with multiplicities $u,v,w$ (even) and $x,y,z$ (odd) gives

$$M=\begin{pmatrix} u+x & v+z & w+y\\ w+z & u+y & v+x\\ v+y & w+x & u+z\end{pmatrix},$$

whose six line sums all equal $u+v+w+x+y+z$; so this is a semi-magic square of line sum $t$ whenever the multiplicities sum to $t$.

Formalization targets

Goal — MacMahon's semi-magic count

$$H_{3}(t)\;=\;3\binom{t+3}{4}+\binom{t+2}{2}\qquad\text{for every }t\ge 0 .$$

This is the goal because it is the weakest statement that still pins down the answer: it asserts the shape of $H_{3}$ without naming the parametrization, and it survives verbatim as the $n=3$ case of Stanley's theorem that $H_{n}$ is a polynomial of degree $(n-1)^{2}$.

The route

1. Canonical decomposition (sm3_canonical). Every $3\times3$ semi-magic square arises from the display above, and the representation becomes unique after normalizing: put $u=\min D$, $v=\min E$, $w=\min F$, subtract the corresponding even permutation matrices, and the residual odd multiplicities satisfy $\min(x,y,z)=0$. The normalization is necessary — without it the single relation

$$D+E+F=A+B+C\;(=J)$$

identifies distinct $6$-tuples — and it is exactly what makes the count a partition rather than an inclusion–exclusion. 2. Bijection (sm3_bij). The map from normalized coefficient vectors to semi-magic squares is a bijection, so $H_{3}(t)=\mathrm{sm3Count}(t)$. 3. Stars and bars (comps_card). The number of $k$-tuples of nonnegative integers summing to $n$ is $\binom{n+k-1}{n}$; the case $k=5$ is what the count needs. 4. Evaluating the parameter count (sm3_params_card). Partitioning the normalized vectors according to the first zero among $(x,y,z)$ writes $\mathrm{sm3Count}(t)$ as

$$\binom{t+4}{4}+\binom{t+3}{4}+\binom{t+2}{4},$$

which collapses to $3\binom{t+3}{4}+\binom{t+2}{2}$ by two applications of Pascal's identity.

Significance

The result itself. $H_{3}$ is the $n=3$ case of a theorem that launched a subject: Stanley's proof that $H_{n}(t)$ counts lattice points in the Birkhoff polytope $t\cdot B_{n}$ makes $H_{n}$ an Ehrhart polynomial, and the order-three formula is the first nontrivial value of it. Beck, Cohen, Cuomo and Gribelyuk (Amer. Math. Monthly 110 (2003), 707--717) revisited exactly this computation on the way to their quasi-polynomial theorem for the magic counts, and Beck and Zaslavsky later pushed the same technique to the panmagic and symmetric refinements. Getting $H_{3}$ machine-checked therefore validates the whole hierarchy at its base.

Formalizing it. Nothing here is open; the mathematics is a century old. What is missing is the formalized artifact, and the difficulty is concentrated in two places that are formalization difficulties rather than mathematical ones.

First, surjectivity of the permutation-matrix parametrization. The usual proof quotes Birkhoff–von Neumann, which in turn needs Hall's marriage theorem. For order three one can instead do it by hand: subtract the three even transversal minima and show that the residual satisfies $M_{01}=M_{10}$. That last step is a six-case argument in linear arithmetic — if $b=M_{01}>c=M_{10}$ then each of the three ways for the transversal $E$ to have minimum zero forces $c\ge b$ — and it is precisely the kind of step that is invisible on paper and must be made explicit in a proof assistant.

Second, the counting step. The parameter set is a filtered finset of functions Fin 6 → Fin (t+1), while the formula is stated with binomial coefficients over $\mathbb{N}$. Connecting them requires stars-and-bars, proved from scratch (by induction on the number of parts plus the hockey-stick identity), because the available library results count sub-multisets rather than compositions. And the final collapse to MacMahon's form is a chain of Pascal identities that must be applied in the right order to stay inside $\mathbb{N}$, where subtraction is truncated.

Difficulty

Two traps deserve to be named.

Uniqueness needs the normalization. The representation by six multiplicities is not injective: $J=D+E+F=A+B+C$. Any formalization that counts $6$-tuples directly will overcount, and the correction is not a subtraction but a choice of canonical representative. Deciding "first zero among $(x,y,z)$" is what turns the count into a genuine partition.

Truncated subtraction. The decomposition is expressed over $\mathbb{N}$, so every identity — in particular the recovery of the multiplicities from a square — must be stated with the admissibility inequalities as explicit hypotheses. A truncated subtraction is only correct because normalization forbids the truncation, and that side condition has to be discharged rather than assumed.

Formalization scope

• Squares are indexed by Fin n; semiMagicCount n t is the cardinality of a finset of arrays over Fin (t+1) — lossless, since every entry is at most $t$.
• The parametrization and its normalization are defined over $\mathbb{N}$ with truncated subtraction where necessary.
• Trivializing formalizations are ruled out. The goal is not a statement about a hardcoded small $t$, nor about a finset declared to have the right cardinality: the count must be derived, by an explicit bijection followed by an explicit evaluation of a finite sum.
• Reusable beyond this mission: the canonical decomposition of $3\times3$ semi-magic squares (equivalently, the toric description of the order-three Birkhoff polytope with its single relation), the stars-and-bars lemma for compositions into any number of parts, and the order-three counts themselves.

Selected references

• P. A. MacMahon, Combinatory Analysis, Vol. II, Cambridge University Press, 1916 (the $H_3$ formula dates to his 1915 work).
• M. Beck, T. Cohen, J. Cuomo and P. Gribelyuk, The number of "magic" squares, cubes and hypercubes, Amer. Math. Monthly 110 (2003), 707--717. https://arxiv.org/abs/math/0201013
• M. Beck and T. Zaslavsky, Six little squares and how their numbers grow, J. Combin. Theory Ser. A 113 (2006). https://arxiv.org/abs/math/0502370
• R. P. Stanley, Enumerative Combinatorics, Vol. I, 2nd ed., Cambridge University Press, 2012 (Ehrhart theory and reciprocity for $H_n$).

Motivation

Counting magic squares — arrays of nonnegative integers whose rows, columns and two main diagonals all share a common line sum — is one of the oldest problems in enumerative combinatorics, and the testing ground on which the general theory was built. MacMahon computed the order-three count in 1915 by hand; sixty years later Stanley, and then Beck, Cohen, Cuomo and Gribelyuk (Amer. Math. Monthly 110 (2003), 707--717), showed that for general order $n$ the counting functions are quasi-polynomials in the line sum, by identifying them with Ehrhart quasi-polynomials of rational polytopes. The order-three case is the oldest nontrivial instance of that theory and the one where every step can still be checked by hand.

The subject therefore has a curious status: the enumerative answer for $n=3$ has been known for over a century, and the structural facts behind it (a $3\times3$ magic square is determined by two corner entries; opposite cells sum to twice the centre) are folklore — but none of it has a machine-checked proof. This mission formalizes the classical derivation end to end.

Setting

Fix an order $n$ and a type $\alpha$ of entries. A square of order $n$ is an $n\times n$ array $M$ with entries in $\alpha$; its row sums, column sums, and the two diagonal sums (main and anti-diagonal) are the sums of the entries along those lines.

• $M$ is semi-magic with line sum $s$ if every row and every column sums to $s$.
• $M$ is magic with line sum $s$ if in addition both main diagonals sum to $s$.
• $M$ is panmagic (pandiagonal) if every broken diagonal, in both directions, also sums to $s$.

No distinctness of entries is required. Let $H_n(t)$ denote the number of semi-magic and $M_n(t)$ the number of magic squares of order $n$ with nonnegative integer entries and line sum $t$. Every entry of such a square is at most $t$, so these are finite counts.

For $n=3$ the whole family is parametrized. If $M$ has line sum $3e$ then the centre cell equals $e$, and writing $a=M_{00}$ and $c=M_{02}$ the eight line identities force

$$M=\begin{pmatrix} a & 3e-a-c & c\\ e+c-a & e & e+a-c\\ 2e-c & a+c-e & 2e-a \end{pmatrix}.$$

All nine entries are nonnegative exactly when

$$e\le a+c\le 3e,\qquad a\le e+c,\qquad c\le e+a,$$

and substituting $p=a-e$, $q=c-e$ turns these into $|p|+|q|\le e$: the $\ell_1$ ball of radius $e$ in $\mathbb{Z}^2$.

Formalization targets

Goal — MacMahon's count

$$M_{3}(3e)\;=\;2e^{2}+2e+1 ,$$

together with the companion vanishing $M_3(t)=0$ when $3\nmid t$. This is the count of $3\times3$ magic squares of line sum $3e$ with nonnegative integer entries (entries need not be distinct). It is the goal because it is the weakest stable statement: it asserts only the shape of the answer, not the intermediate parametrization, and it survives verbatim as the $n=3$ case of the general quasi-polynomial theorem.

Stronger — the parametrization itself

That the map $M\mapsto(M_{00},M_{02})$ is a bijection from the $3\times3$ magic squares of line sum $3e$ onto the admissible parameter pairs, and that the latter are counted by the $\ell_1$-ball cardinality. This is the route the mission actually takes; the count is its corollary.

Further — semi-magic counts

$H_3(t)$, the analogous count for semi-magic squares, is a genuinely different and harder quasi-polynomial. It is listed as a stretch target, not a milestone.

Significance

The result itself. MacMahon's formula is the base case of the Ehrhart-theory reading of magic-square enumeration; Beck--Cohen--Cuomo--Gribelyuk's quasi-polynomial theorem for general $n$ degenerates to it at $n=3$, so it is the sanity check any generalization must pass. The parametrization behind it is what makes the "how many" question finite-dimensional at all: it reduces a search over $t^9$ arrays to a count of lattice points in a two-dimensional ball. Downstream, the same parametrization governs the classification of normal $3\times3$ magic squares (the Lo Shu square and its symmetries) and the associativity identity $M_{ij}+M_{2-i,2-j}=2M_{11}$.

Formalizing it. The mathematics is classical and proved; nothing here is open. What is missing is the formalized artifact. The order-three structural lemmas — the centre identity, the opposite-cell identity, and the two directions of the parametrization — are already machine-checked on this platform. The remaining work is the counting step: exhibiting a concrete bijection between two finsets whose elements live in different types (arrays over Fin (3e+1) versus pairs of naturals) and evaluating a finite sum. That is where the formalization, not the mathematics, is hard.

Difficulty

The obvious attack — "each magic square is determined by $(a,c)$, so just count the pairs" — fails at exactly one point, and it is not a mathematical point. The counting function $M_3$ is defined as the cardinality of a finset of arrays with entries in Fin (3e+1) (a finite type, so that Finset.univ exists), whereas the parametrization lives over $\mathbb{N}$. Proving the counts agree therefore requires a honest Finset.card_bij in both directions:

• forward, extract $(M_{00},M_{02})$ from an array and show the pair is admissible;
• backward, build mkMagic3 from an admissible pair, coerce every entry into Fin (3e+1) using the bound $M_{ij}\le 2e\le 3e$, and show the round trip is the identity.

Neither direction is deep, but the coercions are unforgiving: a truncated subtraction in mkMagic3 is only correct because admissibility forbids the truncation, and that side condition must be discharged explicitly rather than assumed. The second difficulty is the cardinality of the $\ell_1$ ball: the identification $|p+q|\le e\ \wedge\ |p-q|\le e\ \Longleftrightarrow\ |p|+|q|\le e$ needs the elementary identity $\max(|p+q|,|p-q|)=|p|+|q|$, after which the count is $1+4\sum_{k=1}^e k = 2e^2+2e+1$.

Formalization scope

• Entries are indexed by Fin n; the anti-diagonal uses Fin.rev, and broken diagonals use addition modulo $n$. Counting functions are cardinalities of finsets of arrays over Fin (t+1) — lossless, since every entry is at most $t$ — and return natural numbers.
• mkMagic3 is defined over $\mathbb{N}$ with truncated subtraction. Every row/column/diagonal identity therefore carries the admissibility inequalities as explicit hypotheses; no identity is asserted unconditionally.
• Trivializing formalizations are ruled out: the goal is not a statement about a hardcoded small $e$, nor about a finset declared to have the right cardinality. The count must be derived.
• Reusable beyond this mission: the core vocabulary (Square, IsSemiMagic, IsMagic, IsPanMagic, IsAssociative, IsNormal, magicConstant, and the four counting functions $H_n,M_n,P_n,S_n$), the symmetry/affine toolbox, and the order-three structural lemmas. Contributions are welcome on the semi-magic count $H_3$, on panmagic and associative refinements, and on the extension to general $n$.

Selected references

• P. A. MacMahon, Combinatory Analysis, Vol. II, Cambridge University Press, 1916 (the $M_3$ formula dates to his 1915 work).
• M. Beck, T. Cohen, J. Cuomo and P. Gribelyuk, The number of "magic" squares, cubes and hypercubes, Amer. Math. Monthly 110 (2003), 707--717. https://arxiv.org/abs/math/0201013
• M. Beck and T. Zaslavsky, Six little squares and how their numbers grow, J. Combin. Theory Ser. A 113 (2006). https://arxiv.org/abs/math/0502370
• G. Xin, Constructing all magic squares of order three, Discrete Math. 308 (2008). https://arxiv.org/abs/math/0610771

Motivation

A coset partition of a group $G$ is a finite family of left cosets $a_1G_1, \dots, a_kG_k$ that are pairwise disjoint and cover $G$. In 1974 Herzog and Schönheim asked whether the indices $n_i = [G : G_i]$ of such a partition, with $k > 1$, can be pairwise distinct. They cannot when $G = \mathbb{Z}$ — there a coset partition is an exact covering system of the integers, and Davenport–Rado and Mirsky–Newman showed the largest modulus must repeat — but for general groups the question is still open, even for finite solvable groups.

Progress has come in two styles. Structural: Berger, Felzenbaum and Fraenkel settled finite nilpotent groups in Canad. Math. Bull. 29 (1986) 329–333 and finite pyramidal groups in Fund. Math. 128 (1987) 139–144. Order-bounded: Ginosar and Schnabel (2011) settled every $G$ whose order has at most two prime divisors, and Margolis and Schnabel (2019) verified all $|G| < 1440$.

The paper formalized here, Z.-W. Sun, J. Algebra 273 (2004) 153–175, takes a third route: it constrains the subgroups rather than the group, and simultaneously weakens "partition" to "uniform cover". Its hypothesis — that the $G_i$ be subnormal — costs nothing in the nilpotent case (every subgroup of a nilpotent group is subnormal) yet applies to arbitrary, possibly infinite, ambient groups $G$. It also answers negatively an open question of the same paper, generalizing one of Erdős: the indices of such a cover cannot all be large if each occurs only boundedly often.

Setting

Let $G$ be a group, written multiplicatively. For a finite system

$$\mathcal{A} = \{a_iG_i\}_{i=1}^{k}$$

of left cosets, the covering function counts memberships,

$$w_{\mathcal{A}}(x) \;=\; \bigl|\{\, 1 \le i \le k \;:\; x \in a_iG_i \,\}\bigr| .$$

If $w_{\mathcal{A}}$ is constant, say $w_{\mathcal{A}} \equiv w$, then $\mathcal{A}$ is a uniform cover of $G$ of weight $w$; the case $w = 1$ is exactly a coset partition. A uniform cover is trivial when $G_i = G$ for every $i$, and this is the only degenerate case that must be excluded. Uniform covers are genuinely more general than partitions: one may have no disjoint subcover at all.

A subgroup $H \le G$ is subnormal if some finite chain $H = H_0 \trianglelefteq H_1 \trianglelefteq \cdots \trianglelefteq H_n = G$ reaches $G$, each term normal in the next. Normal subgroups are subnormal; in a nilpotent group every subgroup is; and $\operatorname{Sym}(4)$ shows a subgroup of a solvable group need not be.

Write $n_i = [G : G_i]$ for the indices, always assumed finite, and

$$N \;=\; [\,n_1, \dots, n_k\,]$$

for their least common multiple, whose prime divisors are exactly those of $n_1\cdots n_k$. Let $p_*$ and $p^*$ denote the least and greatest prime divisors of $N$, let $\varphi$ be Euler's totient, and let

$$M \;=\; \max_{1 \le j \le k} \bigl|\{\, 1 \le i \le k : n_i = n_j \,\}\bigr|$$

be the largest multiplicity with which an index is repeated. The Herzog–Schönheim conjecture says $M \ge 2$.

Target

The goal theorem is Theorem 4.3(i) of the source: for a nontrivial uniform cover of any group by cosets of subnormal subgroups of finite index, some index divisible by the largest prime $p^*$ is repeated at least $p_*$ times,

$$\exists\, j, \qquad p^* \mid n_j \quad\text{and}\quad \bigl|\{\, i : n_i = n_j \,\}\bigr| \;\ge\; p_* .$$

In particular $M \ge p_*$. Two weaker consequences are separate targets. Since $p_* \ge 2$, this gives the Herzog–Schönheim conjecture for subnormal uniform covers,

$$\exists\, i \ne j, \qquad [G : G_i] = [G : G_j],$$

and the quantitative step behind it is a Burshtein-type inequality, which after clearing denominators reads

$$p^{*}\prod_{p \mid N}(p-1) \;<\; \bigl|\{\, i : n_i = n_j \,\}\bigr| \prod_{p \mid N} p \qquad\text{for some } j \text{ with } p^* \mid n_j .$$

Significance

The result itself. It is the widest structural class in which Herzog–Schönheim is known, and the only one that does not require $G$ to be finite: subnormality of the $G_i$ is a condition on the subgroups, so $G$ itself is arbitrary. It strictly contains the nilpotent case of Berger–Felzenbaum–Fraenkel, and being quantitative it also yields the Burshtein conjecture in this setting — a bound no purely qualitative statement gives. Because the conclusion is a lower bound on $M$ growing with $p_*$, it answers the paper's open question: one cannot make all the indices of a uniform cover large while keeping every multiplicity bounded.

Formalizing it. Nothing here is open, and the mission is the machine-checked version of a known proof. What it adds is a formal vocabulary for uniform covers — Mathlib has Mathlib/GroupTheory/CosetCover.lean (B. H. Neumann's theorems, $\sum_i 1/[G:H_i] \ge 1$) but no notion of covering multiplicity — and the arithmetic of subnormality, in particular that $[G : \bigcap_i G_i]$ divides $\prod_i [G : G_i]$ when the $G_i$ are subnormal. Mathlib has Subgroup.IsSubnormal with the basic closure properties but nothing about indices of subnormal subgroups, and that divisibility is the whole reason subnormal covers behave. The totient measure this proof runs on is already formalized: Sun's Lemma 3.1 is Berger–Felzenbaum–Fraenkel's equation (14), already proved on the platform as BFFPyramidal.muMeasure_divisorClosure_image_mul, and this mission reuses that definition file rather than duplicating it.

Status disclosure. Complete Lean proofs of the goal and of every milestone below already exist and will be submitted at launch, so this mission is not an open frontier: its value is the verified artifact, the reusable vocabulary, and the fact that the development turned up two places where the published argument needs repair or can be simplified (see Formalization scope). Alternative proofs, sharper variants, and the analytic parts excluded below remain genuinely open contributions.

Difficulty

The reciprocal identity is the first thing anyone writes down and it is not enough: a uniform cover of weight $w$ satisfies $\sum_i 1/n_i = w$, and pairwise distinct $n_i$ can do that.

The real obstruction is that a cover does not descend to a quotient. A part $a_iG_i$ need not lie in one coset of a chosen normal subgroup, so the induction that proves the finite nilpotent case has nothing to induct along once $G$ may be infinite and the $G_i$ are merely subnormal. Sun's replacement is a lower bound for the size of a union of cosets, Theorem 3.1: if $H \le G_i$ for all $i$ and $[G:H] < \infty$, then the number of cosets of $H$ inside $\bigcup_i a_iG_i$ is at least the number of $n < [G:H]$ divisible by some $n_i$. The union is compared not with the $G_i$ but with a purely numerical shadow of itself in $\{0, 1, \dots, [G:H]-1\}$, and it is here that subnormality enters, through the divisibility $[G : \bigcap G_i] \mid \prod [G : G_i]$ (Lemma 2.1) — for arbitrary finite-index subgroups Poincaré gives only the inequality $[G : \bigcap G_i] \le \prod [G:G_i]$, which is too weak.

The second difficulty is arithmetic and is where the source spends its effort. Turning Theorem 3.1 into a bound on multiplicities (Theorem 3.2) requires computing the density of a union $\bigcup_i n_i\mathbb{Z}$, and the identity the paper uses (Lemma 3.4) expresses that density as $\prod_{p \in P}\frac{p-1}{p}$ times an infinite sum of reciprocals over $P$-smooth elements of the union. Along that route the full series is needed: truncating it loses precisely the geometric factors $\bigl(1 - p^{-(1+\delta_p)}\bigr)^{-1}$ that produce the divisor sum $\sum_{d \mid N/g} 1/d$ in the conclusion.

It is worth saying, though, that this analytic detour is avoidable — a solver need not take it. Theorem 3.2 can also be reached by a purely finite argument: bound the density from below by injecting each index $s$ into the divisor $\operatorname{lcm}\{s' : s' \mid x\}/s$, which is sharp in the same cases as the series argument. Lemma 3.4 remains a faithful and separately interesting milestone of the paper, but it is not on the critical path to the goal. The naive version of the finite estimate — bounding the density below by $1/\min_i n_i$ — is genuinely false, as $\{4,6,9,12,18,36\}$ shows, so the injection is the content, not a one-liner.

Formalization scope

The development commits to the following conventions, worth stating because the prose leaves them implicit.

Covers are indexed families rather than sets of cosets: IsUniformCover K a w asserts that for every $x$ the number of indices $i$ with $(a_i)^{-1}x \in K_i$ is exactly w, counted as Nat.card of a subtype so that no decidability hypothesis is needed. Indexing by Fin k keeps multiplicities visible, which matters because every conclusion counts indices, not distinct subgroups. Nontriviality is never folded into the definition; it appears as the explicit hypothesis ∃ i, K i ≠ ⊤, and without it every statement here is false (take $k=1$, $G_1 = G$).

$G$ is an arbitrary group — not assumed finite. Finiteness enters only through Subgroup.FiniteIndex on each $K_i$, which the source assumes implicitly when it writes "the (finite) indices". Indices are Subgroup.index and $[G_i : H]$ is H.relIndex (K i). For a subgroup $H$ that is not assumed normal, G ⧸ H is still the type of left cosets and Nat.card (G ⧸ H) = H.index; Theorem 3.1 is stated with that type, since the $H$ it is applied to is not normal.

Densities are never limits. The density of a union $\bigcup_i n_i\mathbb{Z}$ is taken as the finite ratio $|\{x < N : \exists i,\ n_i \mid x\}| / N$ for an explicit common multiple $N$, which is exactly equal to the asymptotic density and keeps Lemma 3.4 free of any analysis on the left-hand side; the right-hand side genuinely is an infinite sum and is stated with HasSum over $\mathbb{R}$.

Inequalities are cleared of denominators and stated in $\mathbb{N}$ wherever possible, so that $\sum_{d \mid m} 1/d \le c$ appears as $\sum_{d \in m.divisors} d \le c \cdot m$. Readers should check the direction: $\mathbb{N}$ subtraction truncates, so $\prod_{p \mid N}(p-1)$ is only the intended quantity because every $p$ here is prime, hence $\ge 2$.

⚠️ Parts (ii)–(iv) of the source's Theorem 4.3 are out of scope. Those bound the primes dividing the indices, their number, and $\log n_1$ by $e^{\gamma}M\log^2 M + O(M \log M \log\log M)$ and similar, and they rest on Mertens' third theorem, $\prod_{p \le x}(1 - 1/p) \sim e^{-\gamma}/\log x$, which Mathlib does not have. It is worth being precise about what Mathlib does have, since the gap is narrower than it looks: the prime counting function Nat.primeCounting, Chebyshev's $\theta$ and $\psi$ with the machinery around them (Mathlib/NumberTheory/Chebyshev.lean), Euler products (Mathlib/NumberTheory/EulerProduct/), and the constant $\gamma$ itself (Real.eulerMascheroniConstant) are all present — what is missing is Mertens' asymptotic tying them together, and the $\pi(x)$ asymptotics. Supplying that is a substantial number-theory project in its own right, so this mission stops at the arithmetic core, part (i), which is what implies Herzog–Schönheim. Contributions adding the analytic parts are welcome and would complete Theorem 4.3.

Two things the development established that the paper does not state. First, Lemma 2.1 is true in a stronger form: $[G : A \cap B] \mid [G:A]\,[G:B]$ needs only $A$ subnormal, not both, and needs no finiteness hypothesis at all (with Mathlib's convention that an infinite index is $0$). Second, Theorem 4.1's passage from the largest prime $p^*$ to the smallest $p_*$ can be isolated as a self-contained arithmetic inequality, $(p_*-1)\prod_{p\mid N}p \le p^*\prod_{p\mid N}(p-1)$, which is tight at prime powers; it is listed as its own milestone for that reason.

Reusable beyond this mission: the uniform-cover vocabulary, the subnormal index divisibility of Lemma 2.1, and Theorem 3.1's union bound, which applies to any attack on Herzog–Schönheim including the still-open solvable case. The source also leaves Conjecture 4.1 open — that for a nontrivial uniform cover by subnormal subgroups the largest index $n$ is repeated at least $p(n)$ times, $p(n)$ its least prime factor — which would be a natural follow-on target.

Selected references

• Z.-W. Sun, On the Herzog–Schönheim conjecture for uniform covers of groups, Journal of Algebra 273 (2004) 153–175. DOI
• M. Herzog, J. Schönheim, Research problem No. 9, Canadian Mathematical Bulletin 17 (1974) 150.
• M. A. Berger, A. Felzenbaum, A. S. Fraenkel, The Herzog–Schönheim conjecture for finite nilpotent groups, Canadian Mathematical Bulletin 29 (1986) 329–333. DOI
• M. A. Berger, A. Felzenbaum, A. S. Fraenkel, Remark on the multiplicity of a partition of a group into cosets, Fundamenta Mathematicae 128 (1987) 139–144. DOI
• N. Burshtein, On natural exactly covering systems of congruences having moduli occurring at most M times, Discrete Mathematics 14 (1976) 205–214. DOI
• R. J. Simpson, Exact coverings of the integers by arithmetic progressions, Discrete Mathematics 59 (1986) 181–190. DOI
• Z.-W. Sun, Exact m-covers of groups by cosets, European Journal of Combinatorics 22 (2001) 415–429. DOI
• B. H. Neumann, Groups covered by finitely many cosets, Publicationes Mathematicae Debrecen 3 (1954) 227–242.
• L. Margolis, O. Schnabel, The Herzog–Schönheim conjecture for small groups and harmonic subgroups, Beiträge zur Algebra und Geometrie 60 (2019) 399–418. arXiv

Motivation

A coset partition of a group $G$ is a finite family of left cosets $a_1K_1, \dots, a_tK_t$ of subgroups $K_i \le G$ that are pairwise disjoint and cover $G$. Asking which multisets of indices $[G:K_i]$ can occur is a question with two independent origins. For $G = \mathbb{Z}$ the cosets are arithmetic progressions and a coset partition is an exact covering system of the integers; Erdős asked whether the moduli of such a system can be pairwise distinct, and Davenport and Rado, and independently Mirsky and Newman, showed they cannot — the largest modulus must repeat. For general groups, Herzog and Schönheim (1974) asked the same question: in any coset partition with $t > 1$, must two of the indices coincide? That question is still open.

Progress has come by restricting the group. Berger, Felzenbaum and Fraenkel proved the conjecture for finite nilpotent groups in Canad. Math. Bull. 29 (1986) 329–333, and the paper formalized here extends it to a wider class defined by a chain condition. Later work bounds the order instead of the structure: Ginosar and Schnabel (2011) settle every $G$ whose order has at most two prime divisors, and three prime divisors when $6 \nmid |G|$, while Margolis and Schnabel (2019) verify all $|G| < 1440$. The conjecture remains open even for finite solvable groups.

Setting

Let $p(m)$ denote the least prime factor of $m$ and $P(m)$ the greatest, and let $\varphi$ be Euler's totient function.

A finite group $G$ is pyramidal if it admits a chain of subgroups

$$\{1\} = G_n \subseteq G_{n-1} \subseteq \cdots \subseteq G_1 \subseteq G_0 = G$$

in which every step has index equal to the least prime factor of the order of the preceding term:

$$[G_{k-1} : G_k] = p\!\left(|G_{k-1}|\right), \qquad 1 \le k \le n.$$

A subgroup whose index is the smallest prime dividing the order is automatically normal, so the chain is a composition series; consequently every pyramidal group is solvable, and every supersolvable group is pyramidal. Pyramidality is therefore a chain condition sitting between supersolvability and solvability.

Given a coset partition $a_1K_1, \dots, a_tK_t$ of $G$, write

$$l \;=\; \frac{|G|}{\gcd\!\left(|K_1|, \dots, |K_t|\right)} .$$

Target

The goal theorem is the multiplicity lower bound of Berger–Felzenbaum–Fraenkel. If $G$ is pyramidal and the cosets $a_iK_i$, $1 \le i \le t$, partition $G$ with $t > 1$, then at least

$$x \;=\; \left\lfloor \frac{P(l)\,\varphi(l)}{l} \right\rfloor + 1$$

of the subgroups $K_i$ have the same order.

Two consequences are separate targets. Since $x \ge 2$ whenever $l \ge 2$, the bound yields the Herzog–Schönheim conjecture for pyramidal groups:

$$\exists\, i \ne j, \qquad [G : K_i] = [G : K_j],$$

and it likewise settles Burshtein's conjecture in this setting, which concerns the case $\gcd(|K_i|) = 1$ and bounds the primes dividing $|G|$ in terms of the largest multiplicity.

Significance

The bound is quantitative where the Herzog–Schönheim conjecture is qualitative: it does not merely assert that a repetition exists but forces a repetition of prescribed multiplicity, growing with the largest prime factor of $l$. That is what makes it strong enough to also imply Burshtein's conjecture, which no purely qualitative statement does.

The class it covers is also of independent interest. Nilpotent groups are pyramidal, so the result subsumes the authors' earlier theorem, and it reaches groups that are solvable but far from nilpotent. It remains, more than three decades later, among the structural (as opposed to order-bounded) cases in which the conjecture is known.

No part of this development is currently formalized: Mathlib has the ingredients — Sylow theory, Hall subgroups of solvable groups, Euler's totient with Gauss's identity $\sum_{d \mid m}\varphi(d) = m$ — but neither coset partitions as a structure, nor pyramidality, nor any case of Herzog–Schönheim. The mission produces the first machine-checked proof of a structural case of the conjecture, together with a reusable formal vocabulary for coset partitions.

Difficulty

The reciprocal identity $\sum_i [G:K_i]^{-1} = 1$ is immediate and useless on its own: distinct indices can satisfy it, so no counting argument over the indices alone can succeed.

The natural attack — induct along the chain, quotienting by $G_1$ — fails because a coset partition does not descend to a quotient. A part $a_iK_i$ need not lie inside a single coset of $G_1$: if $K_iG_1 = G$ then it meets every coset of $G_1$, and the induced family on $G/G_1$ is a cover with multiplicity rather than a partition. Controlling that dichotomy is the first obstacle, and it is precisely where the definition of pyramidality is used, the index $[G:G_1]$ being the least prime factor of $|G|$ rather than an arbitrary one.

The second obstacle is that the conclusion counts subgroups of equal order, so the induction must carry a lower bound on the size of a union of cosets that is sensitive to the orders $|K_i|$ and not merely to their number. The paper's device is a measure $\mu$ on the naturals with $\mu(\{m\}) = \varphi(m)$, evaluated on the divisor closure of the set of orders; Gauss's identity makes $\mu$ interact correctly with divisibility, and the required inequality is genuinely a statement about the group, not about the multiset of orders. The final step splits off the Sylow $P(|G|)$-subgroup against a Hall complement, which exists only because pyramidal groups are solvable.

Formalization scope

The development commits to the following conventions, all fixed in Lean and worth stating because the prose leaves them implicit.

Coset partitions are indexed families rather than sets of cosets: IsCosetPartition K a asserts that for every $x$ there is a unique index $i$ with $(a_i)^{-1}x \in K_i$. Indexing by Fin t keeps multiplicities visible, which matters since the conclusion counts indices, not distinct subgroups; and uniqueness encodes disjointness and covering simultaneously. Groups are finite via [Finite G], and orders and indices are Nat.card and Subgroup.index.

Pyramidality is stated as the existence of a length $n$ and a chain c : ℕ → Subgroup G with c 0 = ⊤, c n = ⊥, and Subgroup.relIndex (c (k+1)) (c k) = Nat.minFac (Nat.card (c k)) for k < n. Normality of each step is a consequence, not a hypothesis, and is deliberately not assumed. The greatest prime factor is maxPrimeFac m = m.primeFactors.sup id, which is $0$ for $m \in \{0,1\}$; the floor in $x$ is natural-number division, so the goal statement is (maxPrimeFac l * Nat.totient l) / l + 1 ≤ …. Note that the bound is vacuous at $l = 1$ — there $P(1)\varphi(1)/1 = 0$ and $x = 1$ — so $t > 1$ is a necessary hypothesis and is present in every statement that needs it; a formalization omitting it would be trivially true and is ruled out.

A complete development needs, beyond the goal: the coset intersection lemma; the least-prime-index dichotomy; uniqueness of the Sylow $P(|G|)$-subgroup of a pyramidal group; the scaling law $\mu(D(kR)) = k\,\mu(D(R))$ for the divisor-closure measure; the union lower bound; and solvability of pyramidal groups. The coset-partition vocabulary and the union bound are reusable for any other case of Herzog–Schönheim, including the still-open solvable case, and contributions of alternative proofs or sharper variants are welcome.

Selected references

• M. A. Berger, A. Felzenbaum, A. S. Fraenkel, Remark on the multiplicity of a partition of a group into cosets, Fundamenta Mathematicae 128 (1987) 139–144. DOI
• M. A. Berger, A. Felzenbaum, A. S. Fraenkel, The Herzog–Schönheim conjecture for finite nilpotent groups, Canadian Mathematical Bulletin 29 (1986) 329–333. DOI
• M. Herzog, J. Schönheim, Research problem No. 9, Canadian Mathematical Bulletin 17 (1974) 150.
• N. Burshtein, On natural exactly covering systems of congruences having moduli occurring at most M times, Discrete Mathematics 14 (1976) 205–214. DOI
• I. Korec, Š. Znám, On disjoint covering of groups by their cosets, Mathematica Slovaca 27 (1977) 3–7.
• Z.-W. Sun, On the Herzog–Schönheim conjecture for uniform covers of groups, Journal of Algebra 273 (2004) 153–175. DOI
• L. Margolis, O. Schnabel, The Herzog–Schönheim conjecture for small groups and harmonic subgroups, Beiträge zur Algebra und Geometrie 60 (2019) 399–418. arXiv