Every p-Extension of A5 Satisfies the Herzog–Schönheim Conjecture
A lifting principle for normal p-subgroups, resting on one finite computation
R004 · Proved modulo one finite computation
The setting
A coset partition of a finite group \(G\) is an exact cover
\[G = D_1 \;\sqcup\; D_2 \;\sqcup\; \cdots \;\sqcup\; D_k, \qquad D_i = x_iH_i,\]
by pairwise disjoint cosets of subgroups \(H_i \le G\). It has pairwise distinct sizes when the \(|D_i| = |H_i|\) are all different, and it is nontrivial when \(k \ge 2\). A group with no such partition is called HS, after the Herzog–Schönheim conjecture, which asserts that every finite group is HS. The conjecture is open; it is known for supersolvable groups, for groups of order below 1440, for groups of order \(p^aq^b\), and for all finite simple groups and all symmetric groups.
This page is about a family that none of those results reaches: groups \(G\) carrying a normal \(p\)-subgroup \(V\) with
\[G / V \;\cong\; A_5 ,\]
the alternating group of order 60. Here \(p\) is a prime and \(V\) is a \(p\)-group, so \(|V|\) is a power of \(p\), and \(V\) is required to be normal in \(G\). Nothing else is assumed: the extension need not split, \(V\) need not be abelian, and \(p\) may divide \(60\) — the cases \(p = 2, 3, 5\) are the interesting ones, and for \(p \ge 7\) the subgroup \(V\) is a normal Sylow \(p\)-subgroup.
The smallest members of the family are \(A_5 \times C_5^2\) of order 1500, \(A_5 \times C_3^3\) of order 1620, and \(A_5 \times C_2^5\) of order 1920. The last of these is the smallest case outside every published criterion: the earlier bound \(|G| < 1440\) stops just below it, and the index criterion of the next paragraph provably cannot reach it.
The theorem is proved modulo one finite computation, and that is not a formality. Everything else on this page is a complete human proof. The single input is a statement about four explicit \(0/1\) systems attached to \(A_5\) — for each of the subgroup orders \(4, 6, 10, 12\), one system is infeasible. Three of the four carry refutations that a machine has checked independently of the solver (drat-trim, zero RAT lemmas in each core). The fourth, size 12, has been decided by three solvers but has no machine-checked refutation, and no human proof exists for either of the two large anchors. Treat the theorem as conditional on that, and read the section The finite input before citing it.
What is new. The lifting principle (Theorem 3.7 below) passes from a linear-independence property of a quotient to the conjecture for the whole group; it assumes nothing about splitting, about abelianness of the kernel, or about coprimality. The published state of the art for simple quotients cannot do this: the index criterion \(\mathcal J(G) < 2\) of [1] gives \(\mathcal J(A_5) = 103/60 < 2\), but already for \(A_5 \times C_2\) the index set grows and \(\mathcal J = 55/24 = 2.2917 > 2\), with the bound rising as more cyclic factors are adjoined. The single property of \(A_5\) used here is linear independence, and it holds for every prime.
What is not new. Sun’s theorem [2] already covers the configurations in which the core \(H_G\) of the covering subgroups is not contained in \(V\): then \(H_GV/V\) is a nontrivial normal subgroup of the simple group \(G/V \cong A_5\), so \(H_GV = G\) and \(G/H_G \cong V/(V \cap H_G)\) is a \(p\)-group, which his theorem settles. Nor is anything needed when \(V \le H_G\), since then \(V\) lies in every covering subgroup, the partition descends to \(A_5\), and [1] settles that. The case this theorem adds is the one left over — \(H_G \le V\) with \(V\) not contained in the covering subgroups — where \(A_5\) is a quotient of \(G/H_G\), so Sun’s theorem does not apply and the partition does not descend either. That case is not empty: for a counterexample with trivial core it is the only case there is. Nor is this a lifting theorem for arbitrary kernels: the argument needs \(V\) to be a \(p\)-group, and it ascends the conjecture itself, not the linear-independence property.
No precedent located. A lifting lemma of this shape was announced for prime-index normal subgroups by Burkhart, who withdrew the paper because of exactly the case such a lemma must handle; the withdrawal note says the case where a subgroup maps to a full copy of \(\mathbb{Z}_p\) under the quotient “is not trivial and must be considered more carefully”. Here the kernel is a \(p\)-group and the hypothesis on the quotient is linear independence, which is what removes that obstruction. Searches of arXiv, zbMATH Open, OpenAlex, Semantic Scholar and the open web found no published lifting theorem of this form.
Linear independence, and private points
Two properties of a quotient group carry the argument. Fix a prime \(p\) and a finite group \(Q\).
Linear independence, \(LI_p\). For every family \(D_1, \dots, D_t\) of distinct cosets of \(Q\) with pairwise distinct sizes, the indicator functions \(\mathbf{1}_{D_1}, \dots, \mathbf{1}_{D_t}\) are linearly independent over the field \(\mathbb{F}_p\); equivalently, no relation \(\sum_j c_j \mathbf{1}_{D_j} = 0\) with coefficients in \(\mathbb{F}_p\) has a nonzero coefficient.
Private points, PP. A point \(g \in Q\) is private to a member \(D\) of a family of cosets if \(g \in D\) and \(g\) lies in no other member. \(Q\) has property PP if every nonempty family of cosets with pairwise distinct sizes has a member with a private point.
Private points are the stronger notion, and they give linear independence over every field: if \(\sum_j c_j\mathbf{1}_{D_j} = 0\) and \(D_{j_0}\) has a private point \(x\), evaluating at \(x\) forces \(c_{j_0} = 0\). So PP implies \(LI_p\) for every prime \(p\) at once — which is why the finite computation below is done once, not once per prime.
The lifting principle
Theorem 1 (Lifting a normal p-subgroup) Let \(G\) be a finite group and \(V \trianglelefteq G\) a normal \(p\)-subgroup. If \(LI_p(G/V)\) holds, then \(G\) is HS.
The proof is short, and its one delicate step is easy to miss, so it is worth setting out. Assume for contradiction a partition \(G = \bigsqcup_{i=1}^{k} D_i\), \(k \ge 2\), with pairwise distinct sizes; write \(Q = G/V\), let \(|V| = p^d\), and put
\[e_i = \log_p [V : V \cap H_i] \in \{0, 1, \dots, d\}, \qquad E = \max_i e_i .\]
- Each \(V\)-coset splits into cosets of subgroups of \(V\). If \(F\) is a coset of \(V\) meeting \(D_i = x_iH_i\), then \(F \cap D_i\) is a coset of \(V \cap H_i\), of size \(|V|/p^{e_i}\). The pieces partition \(F\), so \[\sum_{i \,:\, F \cap D_i \neq \varnothing} p^{\,d-e_i} = p^d .\]
- Read that identity in the quotient. Dividing by \(p^d\) and evaluating at the image \(q \in Q\) of \(F\) gives \(\sum_{i \,:\, q \in \bar D_i} p^{-e_i} = 1\) in \(\mathbb{Q}\), where \(\bar D_i\) is the image of \(D_i\).
- Reduce modulo \(p\). Multiply by \(p^E\) and read the identity in \(\mathbb{F}_p[Q]\). Terms with \(e_i < E\) vanish modulo \(p\), and \(p^E \equiv 0 \pmod p\), leaving the relation \[\sum_{i \,:\, e_i = E} \mathbf{1}_{\bar D_i} \;=\; 0 .\]
- The blocks in the relation are distinct cosets of distinct sizes. For blocks in the top layer, \(|\bar D_i| = |D_i|/p^{\,d-E}\) with the same factor for every one of them, so pairwise distinct \(|D_i|\) give pairwise distinct \(|\bar D_i|\); distinct sizes force the cosets to be distinct subsets of \(Q\). This is the step the natural sketch of the argument omits, and without it the relation is not a relation among distinct basis elements.
- The relation is nonzero. The maximum \(E\) is attained, so the sum is nonempty, and every coefficient is \(1\).
- Contradiction. Steps 3–5 exhibit a nontrivial \(\mathbb{F}_p\)-linear relation among indicators of distinct-size cosets of \(Q\), contradicting \(LI_p(Q)\).
The remaining case is \(E = 0\), where \(V \le H_i\) for every \(i\): the partition then descends to a partition of \(Q\) with the same number of pairwise distinct sizes, and adding \(\mathbf{1}_Q\) to the family gives a nontrivial relation among distinct-size cosets of \(Q\), again contradicting \(LI_p(Q)\).
\(LI_p(A_5)\) for every prime
The second half is arithmetic. To show \(LI_p(A_5)\) for all \(p\), it suffices to prove PP\((A_5)\), and a capacity bound reduces that to a finite check.
The capacity bound. Let \(\mathcal{F}\) be a family of cosets of a finite group \(Q\) with pairwise distinct sizes, and let \(D \in \mathcal{F}\) have the largest size \(S\). If \(D\) has no private point, then every point of \(D\) lies in another member of the family, and at most one member has each size, so
\[S \;\le\; \sum_{m < S} c_Q(S, m), \qquad c_Q(S,m) = \max\{|K \cap L| : K, L \le Q,\ |K| = S,\ |L| = m\}.\]
For \(Q = A_5\) every ingredient is small: the subgroup orders are \(1, 2, 3, 4, 5, 6, 10, 12, 60\), each order is a single conjugacy class, and the capacity sums come out as
\[0,\; 1,\; 2,\; 4,\; 4,\; 9,\; 13,\; 16,\; 43 \quad\text{for } S = 1, 2, 3, 4, 5, 6, 10, 12, 60 .\]
The sum is below \(S\) for \(S \in \{1,2,3,5,60\}\), so a family with no private point can only have largest size \(S \in \{4, 6, 10, 12\}\). That leaves four orders, one conjugacy class each, and one \(0/1\) feasibility question per order.
The four anchored systems. For a fixed order \(S\) and a fixed subgroup \(H \le A_5\) of order \(S\), let \(\mathcal{C}_S\) be the cosets of size at most \(S\) — there are \(785\), \(957\), \(993\) and \(1018\) of them for \(S = 4, 6, 10, 12\). A family \(\mathcal{F} \subseteq \mathcal{C}_S\) that contains \(H\), repeats no size and has no private point exists exactly when the \(0/1\) system with variables \(x_D\) (\(D \in \mathcal{C}_S\)) and \(u_g\) (\(g \in A_5\))
\[x_H = 1, \qquad \sum_{|D| = m} x_D \le 1 \ \ \text{for each } m \le S, \qquad 2u_g \le \sum_{D \ni g} x_D \ \le\ r_S\, u_g \ \ \text{for each } g \in A_5\]
is feasible, where \(r_S\) counts the sizes at most \(S\). The right-hand inequality says a used point is covered at least twice; the left-hand one forbids a point from being covered once, which is exactly what “no private point” means. Both directions are load-bearing — reversing the second makes all four systems feasible.
The finite input
Theorem 2 (What is assumed) Cert-PP(\(A_5\)). For each \(S \in \{4, 6, 10, 12\}\) and each subgroup \(H \le A_5\) of order \(S\), the system above is infeasible.
With Cert-PP(\(A_5\)) granted, PP\((A_5)\) follows, hence \(LI_p(A_5)\) for every prime \(p\), hence the lifting theorem applies to every normal \(p\)-subgroup extension of \(A_5\).
The evidence for each anchor is as follows. “Infeasible” under the mixed-integer solver HiGHS means no \(0/1\) solution was found by a complete branch-and-bound search; the SAT solvers are complete by construction, and for three of the four anchors their refutations were converted into DRAT proofs and checked by drat-trim.
| anchor \(S\) | cosets | HiGHS | Kissat 4.0.4 | Glucose 4.1 | drat-trim |
|---|---|---|---|---|---|
| 4 | 785 | infeasible | UNSAT, 1 s | UNSAT, 0.3 s | verified, 0 RAT lemmas |
| 6 | 957 | infeasible | UNSAT, 4 s | UNSAT, 37 s | verified, 0 RAT lemmas |
| 10 | 993 | infeasible | UNSAT, 142 s | UNSAT, 487 s | verified, 1.5 GB proof, 515 s |
| 12 | 1018 | infeasible | UNSAT, 250 s | no verdict in 45 min | pending |
Two things should be said plainly about this table. First, the infeasibility is integral: the linear relaxation of each system is feasible — take \(x_H = 1\), \(u_g = 1/2\) on \(H\), and everything else \(0\) — so no Farkas-type duality certificate can exist, and any proof must use integrality. Second, anchor 12 has no machine-checked refutation. Its CNF was built and two solvers returned UNSAT, but the proof-logging runs were stopped after 20 and 45 minutes. What would close it is a DRAT proof for that anchor, or a smaller encoding with the same models, or a human argument for \(S = 10\) and \(S = 12\).
The theorem, and the groups it covers
Theorem 3 (Extensions of A5 by a p-group) Let \(p\) be a prime and let \(G\) be a finite group with a normal \(p\)-subgroup \(V \trianglelefteq G\) such that \(G/V \cong A_5\). Then \(G\) is HS.
The family is infinite and contains groups no published criterion reaches:
- \(A_5 \times C_p^k\) for every prime \(p\) and every \(k \ge 1\) with \(|V| = p^k\), so \(C_p^k \times A_5\) and in particular \(A_5 \times C_2^5\) of order 1920, the smallest case outside the \(|G| < 1440\) bound;
- \(\mathbb{F}_p^d \rtimes_\varphi A_5\) for any homomorphism \(\varphi : A_5 \to \mathrm{GL}_d(\mathbb{F}_p)\) — genuinely nonsplit extensions, from order 1920 upward;
- \(SL(2,5) \times C_2^{d-1}\) for \(d \ge 1\), where \(V = Z(SL(2,5)) \times C_2^{d-1} \cong C_2^d\) has no complement in \(G\), of order \(60\cdot 2^d\);
- extensions with non-abelian kernel, such as \(A_5 \times D_8\) with \(V = D_8\);
- for \(p \ge 7\), where \(p \nmid 60\), every such extension splits as \(V \rtimes A_5\) by Schur–Zassenhaus.
The smallest genuinely new order is 1500, for \(A_5 \times C_5^2\).
What it does not settle
- Kernels that are not \(p\)-groups. \(G = A_5 \times A_5\) and extensions by a cyclic group of order 6 are outside the theorem; \(A_5^r\) is handled by a different argument, on the R003 page.
- Arbitrary quotients. The hypothesis is \(LI_p\) of the quotient, which is strictly stronger than the quotient being HS. The result does not extend to “normal \(p\)-subgroup with HS quotient”.
- Ascending linear independence. The theorem ascends the conjecture, not \(LI_p\); nothing here says \(LI_p\) passes to an extension.
- Solvable groups and the general conjecture. Both remain open, and this does not narrow them.
Verification
The arithmetic layer is checked by verify/R004.py: it rebuilds \(A_5\) from scratch as the even permutations, enumerates its 59 subgroups and 1019 cosets, and confirms the subgroup-order spectrum, the single conjugacy class per order, the coset distribution, the candidate counts \(785/957/993/1018\), the capacity sums \(0,1,2,4,4,9,13,16,43\), the Table of \(c_{A_5}(S,m)\) entries, the index arithmetic \(\mathcal J(A_5) = 103/60\) and \(\mathcal J(A_5\times C_2) = 55/24 > 2\), and the order thresholds around 1440. It does not check the four infeasibilities: that needs a MILP or SAT solver, and for anchor 12 it is exactly the gap described above.
References
- M. Garonzi, L. Margolis, The Herzog–Schönheim conjecture for simple and symmetric groups, arXiv:2509.25118. Lemma 2.1(1) (the \(\mathcal J(G) < 2\) criterion), Remark 5.1 (why direct products are out of reach for it).
- Z.-W. Sun, On the Herzog–Schönheim conjecture for uniform covers of groups, J. Algebra 273 (2004) 153–175, arXiv:math/0306099.
- The Herzog–Schönheim conjecture for small groups and harmonic subgroups, arXiv:1803.03569 — the case \(|G| < 1440\).
- M. C. Burkhart, arXiv:1901.10131 — withdrawn; the obstruction it names is what the linear-independence hypothesis avoids.
- Erdős Problems #274, erdosproblems.com/274 — the conjecture listed as open.