Every p-Extension of A5 Satisfies the Herzog–Schönheim Conjecture
A lifting principle for normal p-subgroups, with its one finite input closed inside the Lean kernel
R004 · Novelty unconfirmed
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 family begins just above the \(|G| < 1440\) bound, and the index criterion reaches only part of it: \(\mathcal J(A_5 \times C_5^2) = 2743/1500 < 2\) at order 1500, while \(\mathcal J(A_5 \times C_3^3) = 3847/1620\) at order 1620 and \(\mathcal J(A_5 \times C_2^5) = 1087/384\) at order 1920 both exceed \(2\), and neither of those two orders is below \(1440\) or of the form \(p^aq^b\).
The theorem and its one finite input are inside the Lean kernel. The input is a statement about four anchored coset systems attached to \(A_5\): for each of the subgroup orders \(4, 6, 10, 12\), a family of pairwise distinct cosets — one member of that order, no repeated size, no point covered exactly once — is impossible. All four systems are refuted in the formalization, and the reduction that carries those four refutations to \(LI_p(A_5)\) for every prime \(p\) is formalized with them, so the theorem below is unconditional. The external certificates remain as corroboration, described under Verification.
What is new. The lifting principle (Theorem 1) 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 does not reach these kernels: 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 remark attached to those results [1, Remark 5.1] records that extensions of a simple group by a group of prime order are likely within reach of their methods while direct products are not; the closest case to a simple quotient, a kernel of prime order, is the one they expect to reach, and here the kernel is an arbitrary \(p\)-group. 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, and the re-check made at this revision, on arXiv and the open web, found nothing later either (2026-09-13).
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 \(S = 60\) row is the published criterion, not a new one: there \(c_Q(60,m) = m\), so the condition reads \(\sum_{m < 60} m = 43 < 60\), which is \(\mathcal J(Q) < 2\) — Korec and Znám’s criterion [6], the same one the index computation above uses. What the sieve adds is the rows below the top, and for \(A_5\) those are exactly the four anchored systems.
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 left-hand inequality says a used point is covered at least twice; the right-hand one says a covered point counts as used. Together they forbid a point from being covered exactly 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 (The four anchored systems) 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.
Each anchor is decided, in the kernel:
| anchor \(S\) | cosets | refutation |
|---|---|---|
| 4 | 785 | for any finite group and any subgroup of order \(4\) |
| 6 | 957 | for any finite group and any subgroup of order \(6\) |
| 10 | 993 | for every order-\(10\) subgroup of \(A_5\), from five trace tables built out of \(A_5\) data |
| 12 | 1018 | for every order-\(12\) subgroup of \(A_5\), by the argument below |
Two things should be said plainly about that 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, the solver route to anchor 12 is closed in practice rather than in principle: HiGHS and Kissat decide it (Kissat in 250 s), Glucose runs 45 minutes without a verdict, and the refutation logs written along the way pass 7 GB after two minutes, larger than anything that can be checked here. The refutations above are therefore direct, and the archived drat-trim transcripts for orders \(4\), \(6\) and \(10\) are corroboration rather than part of the argument.
The argument for \(S = 12\)
Fix one subgroup \(H \le A_5\) of order 12, so \(H \cong A_4\), and let \(\mathcal{F}\) be a family of distinct-size cosets containing \(H\) with no private point. Since \(H\) is selected and sizes do not repeat, \(H\) is the only selected coset of size 12. The five order-12 subgroups of \(A_5\) are conjugate, and conjugation carries cosets to cosets of the same size while preserving every incidence and coverage multiplicity, so this one \(H\) settles all five.
For each lower size \(m \in M \subseteq \{1,2,3,4,5,6,10\}\) that occurs, write \(D_m\) for the selected coset and put \(a_m = |D_m \cap H|\), \(b_m = m - a_m\). Every point of \(H\) already lies in the selected member \(H\) and so may not be covered exactly once; hence the traces \(D_m \cap H\) cover \(H\):
\[12 \;\le\; \sum_{m \in M} a_m . \tag{1}\]
With \(c_m = c_{A_5}(12,m)\) the largest intersection of an order-12 subgroup with one of order \(m\), the attainable trace sizes and the deficiency \(d_m = c_m - a_m\) are:
| size \(m\) | 1 | 2 | 3 | 4 | 5 | 6 | 10 |
|---|---|---|---|---|---|---|---|
| attainable \(a_m\) | 0, 1 | 0, 1, 2 | 0, 1, 3 | 0, 1, 4 | 1 | 0, 2, 3 | 2 |
| \(d_m\) | 1, 0 | 2, 1, 0 | 3, 2, 0 | 4, 3, 0 | 0 | 3, 1, 0 | 0 |
| \(b_m\) | \(d_1\) | \(d_2\) | \(d_3\) | \(d_4\) | 4 | \(3 + d_6\) | 8 |
The values \(c_m = 1,2,3,4,1,3,2\) are those largest intersections, and the first row is what a trace can actually attain. The reasons are small. An order-4 subgroup of \(A_5\) is a Klein four group and distinct ones meet trivially, so a size-4 trace has size 0, 1 or 4 — never 2 or 3. An order-6 subgroup \(K\) meets \(H\) in at least \(|K||H|/|G| > 1\) points and is not contained in \(H\), so a size-6 trace has size 0, 2 or 3, never 1. For orders 5 and 10 the product formula forces every coset to meet \(H\), in exactly 1 point for order 5 and 2 for order 10. Writing
\[\begin{aligned} \delta &= \sum_{m \in M} d_m, \\ s(M) &= \sum_{m \in M} c_m - 12, \\ e &= s(M) - \delta = \sum_{m \in M} a_m - 12 \;\ge\; 0, \end{aligned} \tag{2}\]
the last identity rewrites Equation 1: \(e\) is the excess of lower incidences on \(H\). So \(e = 0\) means the traces partition \(H\), and the deficiency budget \(\delta \le s(M)\) is the only slack available.
The outside sieve. Every point of \(B_m = D_m \setminus H\) must lie in some other selected member, so with \(c_{mn} = \max\{|K \cap L| : |K| = m, |L| = n\}\),
\[b_m \;\le\; \sum_{n \ne m} \min\{b_m,\, b_n,\, c_{mn}\} . \tag{3}\]
The cover constraint Equation 1 — equivalently \(\delta \le s(M)\) in Equation 2 — leaves exactly twenty size sets \(M\), and the outside sieve Equation 3 then refutes eighteen of them at once, because one member has more outside points than all the others together can cover. The survivors are
\[M_A = \{2,3,4,5,6,10\} \quad (s = 3), \qquad M_B = \{1,2,3,4,5,6,10\} \quad (s = 4).\]
Three small structure facts finish both.
Lemma 1 (A 3-trace and a 4-trace meet once) In \(H \cong A_4\), the three order-3 subgroups are complements to the unique \(V_4 \le H\): \(H = V_4C\) and \(V_4 \cap C = 1\). So every coset of an order-3 subgroup meets every coset of \(V_4\) in exactly one point, and a size-3 trace and a size-4 trace therefore meet in exactly one point of \(H\).
Lemma 2 (Disjoint traces cap the 5-versus-10 outside intersection) \(|D_5 \cap H| = 1\) and \(|D_{10} \cap H| = 2\) always. If those two traces are disjoint then \(|(D_5 \setminus H) \cap (D_{10} \setminus H)| \le 1\): meeting in more than one point forces \(D_5 \subseteq D_{10}\), and then the point of \(D_5 \cap H\) also lies in \(D_{10} \cap H\).
Lemma 3 (A 3-trace 6-coset meets a 10-coset at most once outside) An order-6 subgroup of \(A_5\) is \(S_3\), and \(K \cap H\) is its normal order-3 subgroup \(C\), with \(K \setminus C\) the three involutions. Two distinct elements of \(K \setminus C\) differ by an element of \(C\), of order 3, which no subgroup of order 10 contains. So \(|(D_6 \setminus H) \cap (D_{10} \setminus H)| \le 1\) whenever \(|D_6 \cap H| = 3\), and at most \(2\) otherwise.
The size-10 member. In both survivors \(a_{10} = 2\), so \(b_{10} = 8\): all eight points of \(D_{10} \setminus H\) must be covered by the others, and
\[8 \;\le\; \sum_{m \in M \setminus \{10\}} |B_{10} \cap B_m| . \tag{4}\]
The contributions are capped by the lemmas and the capacity matrix: size 1 at most \(d_1\); size 2 at most \(d_2\); size 3 at most \(\min(d_3, 1)\); size 4 at most \(\min(d_4, 2)\); size 5 at most 4, or at most 1 when its trace is disjoint from the size-10 trace (Lemma 2); size 6 at most \(1 + d_6\) — at most 1 when \(d_6 = 0\) (Lemma 3), at most 2 otherwise. With that in hand every case falls short of Equation 4:
| case | size set | bound from Equation 4 | required |
|---|---|---|---|
| \(e = 0\) | \(M_A\) | \(\le 2 + \delta = 5\) | 8 |
| \(e = 0\) | \(M_B\) | \(\le 2 + \delta = 6\) | 8 |
| \(e > 0\) | \(M_A\) | \(\le 5 + \delta \le 7\), since then \(\delta \le s - 1 = 2\) | 8 |
| \(e > 0\) | \(M_B\) | \(\le 5 + \delta \le 7\); tightness in the \(\delta = 3\) case would admit 8 | 8 |
The last row is the only place a bound reaches 8, and it is closed by exhaustion rather than by slack. There, \(\delta = 3\) with \(s = 4\) forces \(e = 1\) and every estimate tight; since the size-3 estimate is strict whenever \(d_3 > 0\) (the attainable values are \(0, 2, 3\) while the contribution is at most 1) and the size-4 estimate is strict whenever \(d_4 > 0\) (\(0, 3, 4\), contribution at most 2), tightness forces \(d_3 = d_4 = 0\), hence \(a_3 = 3\) and \(a_4 = 4\). By Lemma 1 those two traces meet in exactly one point of \(H\), and since \(e = 1\) that single repeated incidence is the only overlap among the lower traces — so the size-5 and size-10 traces are disjoint, Lemma 2 drops the size-5 contribution from 4 to 1, and the bound falls to 5. No case reaches 8, so no such family exists, and the \(S = 12\) system is infeasible.
With Theorem 2 proved, PP\((A_5)\) follows by the capacity sieve of the previous section, hence \(LI_p(A_5)\) for every prime \(p\), hence the lifting principle applies to every normal \(p\)-subgroup extension of \(A_5\).
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_5^2\) of order 1500, 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)\) — non-direct semidirect products, split by construction;
- \(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\) — a genuinely nonsplit extension — 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 order in this family above the \(|G| < 1440\) bound 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 page’s claims are formalized in the private technical record’s Lean development, which its workflow builds and audits on every change. All four anchors of Theorem 2 are refuted there. Orders \(4\) and \(6\) are refuted in the strong form — any finite group, any subgroup of that order. Orders \(10\) and \(12\) are refuted for every subgroup of that order: the five trace tables of the order-\(10\) argument and the twenty size sets, capacity matrix and three structure lemmas of the order-\(12\) argument are constructed from explicit \(A_5\) data rather than assumed, and the conjugacy of the subgroups of each order is proved. The capacity sieve that reduces \(\mathrm{PP}(A_5)\) to the four refutations is formalized, as is \(\mathrm{PP}(A_5) \Rightarrow LI_p(A_5)\) for every prime \(p\), and the lifting principle of Theorem 1. Every headline theorem of the development depends only on propext, Classical.choice and Quot.sound, and it contains no sorry, admit, axiom or native_decide.
Two small bridges are stated here rather than formalized there, and it is worth saying where. The anchors are refuted as statements about families of cosets — the form the page’s equivalence with the \(0/1\) system translates to — and the sieve uses the crude bound \(|xK \cap yL| \le \gcd(|K|,|L|)\) rather than the table of exact \(c_{A_5}\) values. Both give the same exceptional set \(\{4,6,10,12\}\), so the formalization depends on neither the \(c\)-table nor the solver certificates.
The arithmetic layer remains as an independent cross-check, by verify/R004.py in the record: 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 \(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.
The finite inputs of the \(S = 12\) argument are checked independently by a second verifier in the record, by brute force over \(A_5\): the attainable trace sizes with the reasons behind them (including that no coset of size 5 or 10 misses \(H\)), the capacity matrix, the three lemmas over all 2160 disjoint-trace \((D_5,D_{10})\) pairs and all 576 \((D_6,D_{10})\) pairs, the twenty size sets with eighteen refuted and \(M_A\), \(M_B\) surviving, and the case analysis for every admissible deficiency tuple. Read its scope narrowly: it machine-checks every finite input and every inequality of the argument, and confirms the sieve is exhaustive over the twenty size sets, but it is not a from-scratch search of the anchor.
The archived drat-trim transcripts for orders \(4\), \(6\) and \(10\) are corroboration rather than the argument: the linear relaxation of each system is feasible, so no Farkas or cutting-planes certificate exists, and the order-\(12\) refutation logs run to gigabytes, which is why the anchored systems are refuted directly — and in the kernel — instead. Smaller encodings of anchor \(12\) were tried outside the record: a \(0/1\) formulation of \(2{,}028\) variables and \(6{,}503\) clauses, a MILP that HiGHS decided in 14.34 s, and an 82 MB partial DRUP log. Those are reported with the proof and nothing on this page depends on them.
References
- M. Garonzi, L. Margolis, The Herzog–Schönheim conjecture for simple and symmetric groups, arXiv:2509.25118v2 (2026). Lemma 2.1(1) (the \(\mathcal J(G) < 2\) criterion), Lemma 2.1(2) (the index-product inequality), Remark 5.1 (prime-order extensions likely within reach; almost simple and direct-product classes not).
- 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.
- I. Korec, Š. Znám, On disjoint covering of groups by their cosets, Math. Slovaca 27 (1977) 3–7 — the reciprocal-sum criterion \(\mathcal J(G) < 2\) that the top row of the capacity sieve restates.
How to cite
Steps Unbounded, Every p-Extension of A5 Satisfies the Herzog–Schönheim Conjecture, R004, 2026. https://stepsunbounded.com/results/R004/
@misc{stepsunboundedR004,
author = {{Steps Unbounded}},
title = {Every p-Extension of A5 Satisfies the Herzog–Schönheim Conjecture},
year = {2026},
note = {Result R004, Steps Unbounded},
url = {https://stepsunbounded.com/results/R004/}
}