# Verification report — KP-4.124 (Problem 4.124 of the K3 list; torsion-free subgroups of [5,3,3,3])

Verification dates: 2026-10-07 (two independent verification runs; checks of the release package); 2026-10-07/08
(third verification run, on the written note and the package); 2026-10-08 (literature addendum: Long's thesis,
Davis 1985, Chen 2025).

**Verdict.** The note proves, with computer assistance, that the Coxeter group W = [5,3,3,3] has no torsion-free
subgroup of index 14400. Equivalently, no facet pairing of one compact regular hyperbolic 120-cell with dihedral
angle 2π/3 gives a closed hyperbolic 4-manifold; every torsion-free subgroup of finite index of W has index 14400·m
with m ≥ 2; and no finite-sheeted manifold cover of the orbifold H⁴/W has Euler characteristic 1. The theorem decides
none of the three questions of Problem 4.124, which concern Euler characteristic 2 (index 28800). Problem 4.124
stays open. The note is unrefereed.

**Dataset label.** The record KP-4.124 is labelled `partially_solved` in the dataset (commit 372682f of
2026-09-28, the current one on 2026-10-07). Our status note of 2026-10-04 recommended `open`, because no part of
the question is settled. The present result does not change that recommendation. The paper states no dataset
status.

## Statement checked
- **Source problem.** R. İ. Baykur, R. Kirby, D. Ruberman (eds.), *K3: A New Problem List in Low-Dimensional
  Topology*, AMS Math. Surveys Monogr. 295 (2026), Problem 4.124 (A. Reid): does a hyperbolic integer homology
  4-sphere exist; an arithmetic one; more generally any closed hyperbolic 4-manifold with Euler characteristic 2?
  - Remark (3) of the problem: by Belolipetsky's theorem an arithmetic example is an index-28800 cover of the
    reflection orbifold of [5,3,3,3].
  - The problem statement and the remarks (1)–(3) were read in the corpus record (ulamai/UnsolvedMath, KP-4.124,
    commit 372682f) and in the authors' preliminary version of the book (pp. 292–293 of that version); the two
    agree. The line "Proposed for K3 by: A. Reid" is only in the preliminary version. The published volume was not
    consulted (the publisher's record of Chapter 4 gives pp. 179–289).
- **Belolipetsky's theorem** (Ann. Sc. Norm. Super. Pisa 2004, Theorem 5.5; Addendum 2007, Theorem 5.5′): hypotheses
  compact, orientable, arithmetic, χ ≤ 16; conclusion: Γ_M is a torsion-free subgroup of index 7200·χ(M) of the
  rotation subgroup W⁺. The statements were read in the arXiv versions. The theorem is used for context only and
  was **not re-verified**.
- **Statement proved in the note.** Theorem 1.2 (computer-assisted): W has no torsion-free subgroup of index 14400.

## Readings
| Reading | Decided by the note? | Evidence |
|---|---|---|
| Is there a torsion-free subgroup of index 14400 in [5,3,3,3] (one 120-cell, χ = 1)? | yes: there is none | two complete enumerations, 0 solutions each |
| Is there a hyperbolic integer homology 4-sphere? | no | not addressed |
| Is there an arithmetic one, or an arithmetic closed hyperbolic 4-manifold with χ = 2 (index 28800 inside W⁺)? | no | only excluded: subgroups of index 28800 contained in a torsion-free subgroup of index 14400 (double covers of one-cell manifolds) |
| Is there any closed hyperbolic 4-manifold with χ = 2? | no | not addressed (nothing is said about manifolds that do not cover H⁴/W) |
| Smallest index of a torsion-free subgroup of [5,3,3,3] | partly | it is 14400·m₀ with 2 ≤ m₀ ≤ 8 (upper bound: Conder–Maclachlan 2005) |

## Results in the paper
- **Theorem 1.2 (computer-assisted).** W = [5,3,3,3] has no torsion-free subgroup of index 14400.
- **Corollary 1.3.** The geometric form, the index form and the Euler characteristic form (with "finite-sheeted").
- **Section 2 (complete proofs).** The polytope P₀ = union of the 14400 chambers at a vertex is a compact regular
  120-cell with dihedral angle 2π/3 (Lemma 2.1); the honeycomb and its symmetry group W (Lemma 2.3); a facet pairing
  that gives a closed hyperbolic manifold develops to this honeycomb, and conversely (Theorem 2.5);
  χ(H⁴/G) = [W : G]/14400 by a direct count of cells (Proposition 2.6).
- **Section 3 (complete proofs).** Finite subgroups (cited: Davis, Theorem 12.3.4(i); Bourbaki, Ch. V, §4,
  Exercise 2 d); also a direct argument); torsion-free ⇔ the five maximal finite parabolic subgroups act freely on
  the cosets; bijection between the subgroups in question and involutions ρ of the 14400 flags with (R0), (R1), (R2)
  (Proposition 3.4); loops; the exact finite-order test over Z[φ] (only "flagged ⇒ finite order" is used); the
  188 = 17 + 17 + 154 classes (computed three times); the slice decompositions (Propositions 3.11, 3.12); the search
  scheme with inherited candidate lists (Lemma 3.16).
- **Section 4.** Program A: 13 rules, each proved to be a necessary condition; completeness (Theorem 4.3); the 14
  empty slices.
- **Section 5.** Program B: 14 rules, each proved; completeness of `fps_final` (Theorem 5.3) and of `fps_v7` with the
  lex-leader reduction under the stabilizer of the root gluing (Lemma 5.5, Proposition 5.6, Theorem 5.7).
- **Sections 6–8.** The computation, the controls and rejection tests, the weaknesses found, and the open case of
  index 28800.

## Computations (scripts, logs and outputs in reproducibility/)
- **Program A** (`programA/`): 154 slices, 383 jobs, 1 596 433 384 search nodes, 36.48 cpu-hours, 0 solutions,
  0 complete gluings reached. Engine `fsearch_production.c`, options `-k 1 -root t -ell 1 -keys 8 -sub S I`.
  Checksum of the logs (sorted DONE lines without the cpu field):
  `22bb406ca14479324db761d10c4e6cb78bf4a799f3f3d47fbb5d3aca97c1912c`.
- **Program B** (`programB/`): 140 slices, 935 jobs, 326 322 489 739 trial gluings, 65.15 cpu-hours, 0 solutions,
  0 complete gluings reached. 87 light slices and 6 heavy slices with `fps_final.c`; 47 heavy slices (752 logs,
  97 % of the trials) with `fps_v7.c -bw 200 -sym`. Checksum of the logs (names and digests):
  `e93013be9073d3e89fcb906648716dc9b646e0eaabc902f82cfda679822b2c9f`.
- **Machine and tools.** Apple M3 Max, macOS 26.6.2; Apple clang 21.0.0; Python 3.13.5, numpy 2.5.2. Runs of
  2026-10-03 and 2026-10-04. (The third verification run regenerated the table of program A with numpy 2.3.1 and
  obtained the same hash.)
- **No complete gluing was reached** in any production job of either program. The leaf tests were never executed;
  the theorem rests on the necessity of the pruning rules, on the agreement of the sources with the rules as
  described, and on the tables.
- **Acceptance tests.** `checks/check_p1.py`, `checks/check_p2.py`: RESULT: PASS (0 failures) on the packaged logs
  (`checks/out_check_p1.txt`, `checks/out_check_p2.txt`).

## Independent verification runs
Two independent, AI-assisted verification runs examined the result after the enumerations were complete
(2026-10-07). Both returned CONFIRMED, with required corrections that were applied.

| Item | Checked by | Verdict |
|---|---|---|
| The three forms of the statement | mathematical run | CONFIRMED after corrections (form 3 needs "finite-sheeted"; form 1 needs the definition of a facet pairing and the developing argument) |
| The reduction (finite subgroups, W-sets, loops, elliptic filter, types, slices) | mathematical run | CONFIRMED, every proof re-derived; citations checked in Davis's book |
| Every pruning rule of both programs (13 + 14), inherited lists, quick test, forced deductions, lex-leader reduction | mathematical run | CONFIRMED, one proof per rule, compared with the code lines |
| Tables of both programs | both runs | CONFIRMED: regenerate bit-identically; every entry equal to an independent construction; the two programs exclude the same 1680 elements |
| Coverage of the job lists, integrity of the 383 + 935 logs, totals, checksums | computational run | CONFIRMED (strict checkers written for this purpose) |
| Binaries correspond to the sources | computational run | CONFIRMED (all rebuilds bit-identical) |
| Reruns | computational run | 102 jobs of program A and 52 of program B: every counter identical (2.2 % of the nodes, 1.5 % of the trials) |
| Positive controls with the production options | both runs | CONFIRMED: [3,5,3] 432 labelled solutions / 7 classes; [5,3,5] 698 / 12; [3,4,3,3] 14999 / 149; Conder–Maclachlan gluing rebuilt from 40 to 60 of its facet gluings; Davis manifold |
| Rejection tests | computational run | mutated programs give wrong counts on the controls; manipulated logs are rejected by the strict checkers |
| Cross-check of 57 partial gluings between the engines | computational run | 0 completions in every finished run |
| Third engine | mathematical run | 52 of the 154 slices of program A searched completely, 0 solutions, node counts equal to the plain search; first node of all 154 + 140 slices reproduced; candidate lists reproduced at about 1400 sampled deeper nodes |
| Literature and novelty | mathematical run | nothing found that decides index 14400 or 28800; "to our knowledge" only |

Weaknesses found by the runs, all addressed in Section 7.7 of the paper: the original validation of program B did
not use the production options (closed by new controls); the summary scripts were too weak (replaced by strict
checkers); part of the validation of program A was not tied to commands (controls rerun); the production source of
program A is a later copy of the file from which the binary was built (same hash, bit-identical rebuild); the leaf
tests were never used; 47 heavy slices of program B depend on the symmetry reduction of `fps_v7` (now proved and
tested); minor points of the code.

**Checks at the writing stage.** All proofs were written out again and compared with the two sources. From a copy
of the release package: all binaries and tables rebuilt with the recorded hashes; both strict checkers PASS; the log
checksums reproduced; the positive controls, the Conder–Maclachlan control, all mutation tests, the manipulated-log
tests, the comparison of the stored reruns, the first-branching probes and seven scripts of the third engine
(classes, table comparison, sub-slice consistency, first node of all slices of both programs, the two recomputations
of the symmetry reduction) were run again and reproduced the recorded outputs.

### Third verification run (AI-assisted, 2026-10-07/08)
A further independent, AI-assisted verification run examined the written note and the release package before the
final revision. Verdict: CONFIRMED; 17 required corrections of the text and the package, all applied; no error in
the proofs, no difference between the rules of the paper and the code. Its code and outputs are in
`reproducibility/independent_run_2/`.

| Item | What was done | Outcome |
|---|---|---|
| Proofs written at the writing stage (Lemma 2.1, Theorem 2.5, Proposition 2.6, Lemma 3.16, Corollaries 4.4 and 5.4, Lemma 5.5, Proposition 5.6, Theorem 5.7) | read line by line; tested against [5,3,3,5] (Davis manifold) and the Euclidean group [3,4,3,3] | correct; two clarifying sentences added (Lemma 2.1(iii), proof of Theorem 5.7) |
| Rules (A1)–(A13), (B1)–(B14) against `fsearch_production.c`, `fps_final.c`, `fps_v7.c` | all three sources read completely; rule → lines → verdict; converse (every other place that discards something); integer types; option values of all 1318 logs | agree; the lists of inactive code in the paper were completed |
| Proposition 3.9 and Table 2 | new code: H as matrices over Z[φ], literal finite-order test, certificate of infinite order for the other 12720 elements | 188 = 17 + 17 + 154, 480 / 1200 / 12720, 126 + 14 pairs, 140 type classes, 1680 flagged; 1/14400 |
| Tables read by the engines | every entry used in production (program A: 14400·120 + 120·14400 entries and the small tables; program B: flagged file, table of V) against the new construction | no mismatch |
| First node of every slice | new implementation of the root step, the trial, the branching rule, the sub-slice selection and rule (B13) | program A: 154 of 154 slices, nodes of depth 2 in 356 of 356 jobs; program B: 140 of 140 slices, nodes of depth 2 in 890 of 890 logs, SYM line in 752 of 752 logs |
| Controls | literal enumeration for [3,5,3]; the control scripts of both programs; program A on [3,4,3,3] | 432 / 7; outputs identical to the stored ones; 239 solutions, 149 classes |
| Reruns | new random sample (seed 4124100801): 12 jobs of program A, 8 of program B | every counter reproduced; 174 jobs run twice in all (5.0 % of the nodes of A, 1.9 % of the trials of B) |
| Package | `setup.sh`, strict checkers, log checksums, manifest, README commands; totals of Section 6.2; hygiene; SANITIZATION.txt | reproduced; two logs of the Davis control added to the package |
| Statement, quotations, literature | corpus record, authors' preliminary version of the book, local extracts of Belolipetsky and Conder–Maclachlan; arXiv, OpenAlex, Crossref, zbMATH, one web search | dataset label and source of the attribution corrected; Ratcliffe–Tschantz (1998) and Long's thesis (2007) added; first name of C. Long corrected |

What this run did **not** check: the long production jobs (not repeated); anything below depth 2 of the search
trees; the fields `tries` (program A) and COUNTS (program B); the mutation runs and the long scripts of the third
engine (not run again); Long's thesis (abstract only); Ratcliffe–Tschantz 2001 and the journal version of
Ratcliffe–Tschantz 1998 (not read); Belolipetsky's theorem (not re-verified); the published volume of the K3 list.

## What was not checked, and remaining risks
- **No complete rerun of the heavy jobs.** The jobs that were run twice contain 5.0 % of the nodes of program A and
  1.9 % of the trials of program B. The long jobs were run once.
- **No third complete enumeration.** The third engine searched 52 of 154 slices completely and sampled the rest.
- **Belolipetsky's theorem** was not re-verified. It is used only to explain the relation to Problem 4.124.
- **Index 28800** (the case of Problem 4.124): both enumerations are incomplete; the estimated cost is 10³ to 10⁴
  core-hours. Nothing is claimed.
- **Remaining risk.** An error common to both programs in a place that the controls, the mutation tests and the
  partial third enumeration do not reach. Both programs were written from the same short specification; the
  specification itself (Proposition 3.4) is proved in the note. The small controls [3,5,3] and [5,3,5] do not
  exercise every code path of the main problem; this is mitigated by the rank-5 control [3,4,3,3], by reruns with
  generic propagation, and by the comparisons with the third engine on the real problem. For the 47 slices run with
  the symmetry reduction, the independence of the two programs is the main safeguard.
- Sources not read in full: Long 2008, Conder–Liversidge 2023, Ma–Zheng 2021 and Conder–Kellerhals 2022 (abstracts
  only); Long's doctoral thesis (read: abstract, Section 1.3, Chapters 7 and 8; its proofs were not checked); Davis
  1985 (Section 3 and the closing remarks read); Chen 2025 (introduction and Section 5.3 read); Ratcliffe–Tschantz
  2001 (quoted from Martelli's survey); Ratcliffe–Tschantz, "Gravitational instantons of constant curvature" (read
  in the arXiv version of the workshop proceedings astro-ph/0010170, not in the journal version of 1998);
  Bourbaki's exercise (identified through Davis's citation). The third run knew Long's thesis from its abstract
  only; the thesis was read afterwards, see the literature addendum below.

## Literature addendum (2026-10-08, after the third run)
The third run knew Long's doctoral thesis from its abstract only and named this as a risk for the novelty
statement. The thesis was then obtained from the repository of the University of Southampton (record 466178, scan
of 227 pages, SHA-256 of the file 56f3e784da95099bbfa49c92ae1bf1165a2213e92bc593c79ecc2f876f217198). The abstract,
Section 1.3, Chapter 7 (pp. 173–185, on [5,3,3,3]) and Chapter 8 were read in the text layer of the scan; the
passages used in the note (pp. 173–175, 179, 184–185) were compared with the page images.

- **What the thesis contains on index 14400.** It calls it "an outstanding question" whether [5,3,3,3] has a
  torsion-free subgroup of index 14400 (p. 173) and traces the question to the closing remarks of Davis's paper of
  1985 (p. 174). Proposition 7.3.1: there is no epimorphism of [5,3,3,3] onto [5,3,3] with torsion-free kernel; this
  is the case of normal subgroups of the theorem of the note. Theorem 7.1: if H is torsion-free of index 14400 with
  core K, then the quotient by K has no epimorphism onto a sporadic simple group. Further: the numbers of conjugacy
  classes of subgroups of each index up to 720 (Table 7.9), and three torsion-free subgroups of index 115200, not
  contained in the rotation subgroup. The thesis does not decide the question; its conclusion speaks of "a possible
  approach towards determining the minimal index torsion-free subgroup". Its proofs were not checked here.
- **Davis 1985.** The closing remarks (Proc. Amer. Math. Soc. 93, p. 328) were read in a scan of the journal pages:
  the groups [5,3,3,3] and [5,3,3,4] have Euler characteristics 1/14400 and 17/28800; "the second one does not
  admit a torsion-free subgroup of index 14400; however, the first one quite possibly does". The theorem of the
  note shows that the first one does not.
- **Parity.** A closed hyperbolic 4-manifold with Euler characteristic 1 would be non-orientable. Parity does not
  exclude it: Ratcliffe and Tschantz (astro-ph/0010170, Section 1.3) report two closed non-orientable hyperbolic
  4-manifolds with Euler characteristic 17, glued from two right-angled 120-cells, and Chen (arXiv:2501.11610,
  Section 5.3) writes that these are the only closed hyperbolic 4-manifolds of odd Euler characteristic that he
  could find in the literature. Two further web searches on this point found no parity obstruction for
  non-orientable closed hyperbolic 4-manifolds and no result on index 14400.
- **Consequences for the note.** The novelty statement stands: no source decides the question. The credit was
  completed: the question goes back to Davis (1985); the case of normal subgroups is in Long's thesis. Changed in
  the note: one sentence of the abstract, the account of earlier work in Section 1.1 (Long's thesis, Davis's remark,
  the paragraph on parity), the paragraphs "Verification" (one new item) and "Scope and priority" of Section 8, and
  the bibliography (Chen 2025 added). The statements, the proofs, the programs and the computations were not changed.

## Relation to the literature, novelty and scope
- Davis (1985, closing remarks) notes that [5,3,3,3] has Euler characteristic 1/14400 and writes that it "quite
  possibly" has a torsion-free subgroup of index 14400. The note answers this in the negative.
- Ratcliffe and Tschantz (workshop contribution of 1998, arXiv:astro-ph/0010170, Section 1.3) consider manifolds
  glued from one or two 120-cells with dihedral angle 2π/3, call a purely combinatorial search "essentially
  intractable" and report that restricted searches found none. The note settles the case of one cell.
- Conder and Maclachlan (2005) found a torsion-free subgroup of index 115200 = 8·14400 and left smaller indices
  open. Long (thesis 2007, paper 2008) gave further examples of index 115200; his thesis calls the question of
  index 14400 outstanding and contains the case of normal subgroups (Proposition 7.3.1). Belolipetsky (2004,
  Section 5.6) proposed a computer search for torsion-free subgroups of the Coxeter group.
  Emery (2014) settled the analogous question in dimensions above 4. Martelli's survey lists the smallest volume of
  a closed hyperbolic 4-manifold as an open question. Conder and Liversidge (2023) treat the rank-4 analogue.
- **Searches (October 2026).** arXiv listings, OpenAlex (including the works citing Conder–Maclachlan 2005, Long 2008,
  Emery 2014 and Belolipetsky 2004), Crossref, zbMATH, five web searches. Nothing was found that decides index
  14400 or 28800 in [5,3,3,3], or the existence of a closed hyperbolic 4-manifold with Euler characteristic 1 or 2.
  Apart from Long's thesis, theses and unpublished computations are not covered. This negative
  search is not a proof of priority. Two papers with related titles treat other questions (Ma–Zheng 2021: small
  covers of the right-angled 120-cell; Conder–Kellerhals 2022: cusped manifolds from [3,…,3,6]).
- **Scope.** The result is new to our knowledge. It raises the lower bound for the smallest index of a torsion-free
  subgroup of [5,3,3,3] from 14400 to 28800. No novelty is claimed for the control cases (Everitt's lists, the Davis
  manifold, the Conder–Maclachlan subgroup). No claim is made on Problem 4.124.

## Public release and license
This paper, its source files, and this verification report are licensed under the Creative Commons Attribution
4.0 International License (CC BY 4.0): https://creativecommons.org/licenses/by/4.0/