Four-dimensional determinant-one representations and cyclic singlets

S. Groot Nibbelink, O. Loukas, A. Mütter, E. Parr and P. K. S. Vaudrevange (arXiv:1710.09237, hep-th; Fortschr. Phys. 68 (2020) 2000044) reduce the question of heterotic orbifolds that are supersymmetric in every twisted sector but not globally to a statement about finite groups:

There does not exist any finite group $\mathbf{H}$ that has a
four-dimensional representation $D_\rep{4}$ with the following three
properties: (i) $D_\rep{4}$ has a trivial determinant … (ii) $D_\rep{4}$ does
not contain the trivial singlet representation of $\mathbf{H}$ … (iii) but
the branchings of $D_\rep{4}$ to all $\Z{N} \subset \mathbf{H}$ subgroups
always contain the trivial $\Z{N}$-singlet representation.

Issue #11489 fixes the reading: H is any finite group, D any complex representation on ℂ⁴, (ii) means that no nonzero vector is fixed by all of D(H), and (iii) means that every cyclic subgroup fixes a nonzero vector. The formal claim is the conjecture; the result proves it.

In the paper, groups violating the conjecture would give non-supersymmetric orbifolds with local Killing spinors in every sector. The authors verified the conjecture only by enumeration, over the 1,594 CARAT groups and all groups of order at most 500, and asked for a proof. The frozen declaration D5/S3/Quantum/Algebra/FourDimensionalSingletBranching.result proves it for every finite group.

Issue #11489 preregisters the reading, the route and the literature check. INSPIRE lists 38 citing records, and full-text searches within them find no proof or counterexample. The same authors' 2019 proceedings (arXiv:1903.03789, §5) report only the enumeration restricted to groups whose Λ²4 is an integral 6×6 CARAT representation (1,594 abstract groups) and do not restate the unrestricted conjecture. A. Mütter's 2020 TUM thesis (INSPIRE 1829126) restates it with "we do not have a rigorous proof for this statement". Groups in which every element has eigenvalue 1 are called unisingular. The unisingular literature (Zalesski, arXiv:2401.16075, and the related papers listed in #11489) treats irreducible groups; the conjecture's content lies in reducible representations. The proof is Molien's formula for the exterior algebra at t = −1, specialised to dimension 4 and determinant 1. The formula is classical; this corollary was not found in the searched sources.

These readings are not-found-in-searched-scope; they do not establish an exhaustive worldwide literature search, priority, or the absence of an independent answer.

1. Under (iii), the cyclic subgroup generated by h fixes a nonzero vector, so det(1 − D(h)) = 0 for every h.
2. For a 4 × 4 matrix with det A = 1, adj A = A⁻¹ and det(1 − A) = 2 − tr A − tr A⁻¹ + e₂(A), with e₂(A) = ((tr A)² − tr A²)/2.
3. S = Σ_h D(h) satisfies D(g)S = S, so S = 0 by (ii). Hence the traces of D(h) and of D(h)⁻¹ = D(h⁻¹) sum to 0.
4. With T = Σ_h D(h) ⊗ D(h) and W the swap, T² = |H|T, W² = 1 and TW = WT. So Q = T(1 − W)/(2|H|) is idempotent, and Σ_h e₂(D(h)) = |H| tr Q = |H| rank Q.
5. Σ_h det(1 − D(h)) = |H|(2 + rank Q) ≠ 0, contradicting step 1.

The statement would change in dimension 5, where the paper's Q₈ example violates it, or without the determinant condition, for example ℤ₂ × ℤ₂ acting as a + b + c + c. Both enter the proof: dimension 4 in the determinant expansion of step 2, and determinant 1 in adj A = A⁻¹.

The identities of steps 2 and 4 were checked symbolically, and the averaged identity was checked on 663 random four-dimensional monomial groups (issue #11489). The same checker flags the paper's five-dimensional Q₈ example.

The canonical source is D5/S3/Quantum/Algebra/FourDimensionalSingletBranching.lean. Its public declarations are claim and result. The frozen module state has statement identity sha256:ae04295c1edb9a4aa3e8b3136402e9f8ff55715be1f4038b38db381863abcc29. The result declaration has statement identity sha256:292c5373a7d4bc95f4657e5e0773787847626610e611cc6ece488b632dd1b4d3. The Freeze event is sha256:93abbe22680359ee8dca0398e7b8402e9208260bc84e2de412f35d08e447a218 and has no project-level frozen prerequisites. The proof uses only the standard axioms propext, Classical.choice and Quot.sound; no sorry, native_decide, or new axiom.

Tier 1 conjecture from a 2017 hep-th paper, preregistered in issue #11489 before any Lean. theorem; resolution proved. The public theorem has proof_shape: bind-only: the determinant identity, the averaging and the rank of the averaged idempotent are local steps of result, obtained from pinned Mathlib by instantiation and normalization. There is no escape witness; the admission basis is open-problem-resolution. Utility none.

What the settlement shows

Proved (Lean): no finite group has a representation on ℂ⁴ with trivial determinant, no trivial singlet and a trivial singlet in every cyclic subgroup; the paper's enumeration over the 1,594 CARAT groups and the groups of order at most 500 is therefore not a restriction.

Mechanism (proved, inside result): the average of det(1 − D(h)) over H equals 2 + m, where m is the rank of the idempotent Q = (Σ_h D(h) ⊗ D(h))(1 − Swap)/(2|H|); condition (iii) makes every det(1 − D(h)) vanish, while the average is at least 2. Interpretation, not separately formalized: Q projects onto the invariants of Λ²ℂ⁴, so m is the number of trivial singlets in Λ²ℂ⁴.

Not formalized (argument): for a representation of dimension n with trivial determinant and no trivial singlet, the same average is Σ_k (−1)^k m_k, with m_k the number of trivial singlets in Λ^k, and Λ^k ≅ (Λ^{n−k})^* gives m_k = m_{n−k}. For odd n the terms cancel and the average is 0, so the argument gives no obstruction; this matches the paper's five-dimensional Q₈ example. For n = 2 the average is 2. For n = 6 it is 2 + 2m₂ − m₃, which the identity alone does not keep away from 0.

Computed, not formalized: the six-dimensional analogue fails. For H = {±1} × {±1} and D(a, b) = diag(a, a, b, b, ab, ab), every D(a, b) has determinant 1; the elements (−1, 1) and (1, −1) together fix no nonzero vector; and every cyclic subgroup, of order at most 2, fixes a coordinate vector, since one of a, b, ab equals 1. Here the average of det(1 − D(h)) is 0.

Source consequences (paper's reduction, not formalized): in the paper, a group violating the conjecture is what a non-supersymmetric orbifold with a local Killing spinor in every twisted sector would require, so no point group of this kind gives such an orbifold.

The published Fortschr. Phys. text was not read, so it is unverified whether the conjecture was edited there. The bounded literature check does not establish exhaustive worldwide novelty, priority, or the absence of an independent answer. The Lean kernel does not authenticate the external source or its version history.