Group Theory

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