# Verification report — KOU-16.46 (Conder: does the index-8 subgroup K of G_3 *_{G_1} G_4 have a non-trivial finite quotient?) Verification date: 2026-10-24. **Verdict.** The note gives a **partial answer**; the question itself is **not decided**. - **Proved without computation.** K is perfect; in every non-trivial image of K the generators keep their orders (A, B order 3; C, D, E, F order 2) and S4 embeds; L = = S4 *_{D8} S4, with H = = C3 * C3 of index 8; K is the amalgamated free product of four copies of L over H, glued along the four sign automorphisms (A,B) -> (A^±1, B^±1); a non-trivial finite quotient of K gives one of J = L_C *_H L_D (Theorem 1.2). - **Computer-assisted, exhaustive.** Every homomorphism from J to S_n, n <= 36, is trivial, so J and K have no subgroup of index 2 to 36 (Theorem 3.1). There is no non-trivial homomorphism from J (hence from K) to any non-abelian finite simple group of order < 10^8 (Theorem 4.2, GAP 4.16.1), nor to the twelve simple groups of order between 10^8 and 10^9 that are not PSL2(q) (Theorem 4.3). Hence every non-trivial finite quotient of J or K has order >= 10^8, and, with Jambor's machine computation (J. Algebra 423 (2015), Prop. 12.2 of arXiv:1402.6788v1: no quotient PSL2(q) or PGL(2,q)), every non-trivial finite quotient of K has order >= 10^9 (Corollary 1.4). - **Known.** The question and the construction are Conder's (J. Algebraic Combin. 1 (1992), Section 5); the exclusion of all PSL2(q), PGL(2,q) is Jambor's; Theorem 1.2 is elementary and may be known to experts. - **Contrast.** L_C *_H L_F (twist (A,B) -> (A^-1,B^-1)) maps onto A6 and PSL(2,7) (Proposition 5.1). - **Open.** Whether K (or J) has a non-trivial finite quotient; whether K is simple. The note is unrefereed. ## Statement checked - **Primary source.** Kourovka Notebook, Problem 16.46 (M. Conder, 16th issue, 2006), arXiv:1401.0300 v48 (6 October 2026) and v49 (20 October 2026). The text gives G3 = , G4 = , G1 = = PSL2(Z), the normal subgroup K of index 8 of G3 *_{G1} G4 generated by A = h, B = aha, C = p, D = PpP, E = QpQ, F = PQpPQ with dihedral complement , its presentation with 22 relators, and asks "Does this group have a non-trivial finite quotient?". In v48 and v49 the problem has no comment and no mark (neither * nor the ♯ that v49 introduced for unconfirmed AI solutions; page 105 of v49 rendered and read by verification run 3); the v49 text is identical to v48. - **Origin.** M. Conder, Group actions on the cubic tree, J. Algebraic Combin. 1 (1992) 209–218, doi:10.1023/A:1022490600465, read in full in an open scanned copy. Section 5: the same groups and relations (Conder's G4^1 and G3, the subgroup called S), the Schreier transversal {1, a, P, Q, PQ, aP, aQ, aPQ}, the questions whether S can be simple and whether it has a non-trivial finite quotient, and the remark that the author had found no proper subgroup of finite index (no bound given); the same section recalls that for two copies of G4^1 (Problem 6 of Djoković–Miller) the group generated by the vertex stabilisers is residually finite and maps onto PSL2(7). The displayed presentation of S (p. 217) is not in the text layer of the scan; read from the rendered page (verification run 3), it has the same 22 relators as the Kourovka text and Jambor's Proposition 12.2, and the relators are re-derived from the definition of K in Remark 2.6 of the note (Bass–Serre theory for the action of K on the tree of the amalgam). - **Corpus record.** ulamai/UnsolvedMath, KOU-16.46 (dataset version 1.8.0), status `open`; its statement reproduces the Kourovka text. ## Readings | Reading | Answer | Where | |---|---|---| | "this group" = K, the group with the 22-relator presentation | not decided; every non-trivial finite quotient has order >= 10^8 (>= 10^9 with Jambor) and K has no subgroup of index 2..36 | Theorems 3.1, 4.2, 4.3, Corollary 1.4 | | "this group" = G3 *_{G1} G4 | trivially yes (G maps onto D8); not the intended reading. Equivalent in substance: K has a non-trivial finite quotient iff G has a finite quotient of order > 8 | (verification run A) | | Conder's second question: is K simple? | not decided | Section 1.3 | | "non-trivial finite quotient" = finite quotient of order > 1 | used throughout; K is infinite (contains C3 * C3) | Section 1.1 | ## Results in the paper - **Lemma 2.1.** K, J, L are perfect. - **Lemma 2.2.** If a homomorphism of K (of J, of L) kills one generator, it is trivial; so in a non-trivial image A, B have order 3 and the other generators order 2. - **Lemma 2.3.** (a) b^3 = c^2 = (bc)^3 = 1 implies [c, b^-1 c b] = 1; the (2,3,3) triangle group is A4. (b) The presentation is S4. (c) L = S4 *_{D8} S4 with the two copies and ; the identification of the D8's swaps the roles of the two non-central involution classes. (d) = C3 * C3 and [L : ] = 8 (H acts simply transitively on the edges of the tree of the amalgam). - **Lemma 2.4.** The relators of K involving X = C, D, E, F are those of L at (A^e, B^d, X) with (e,d) = (1,1), (1,-1), (-1,1), (-1,-1); K = L_C *_H L_D *_H L_E *_H L_F, J = L_C *_H L_D; homomorphisms K -> S correspond to solutions of four "roles". - **Corollary 2.5.** A non-trivial homomorphism of K restricts to a non-trivial one of J; S4 = embeds in every non-trivial image. - **Remark 2.6.** Re-derivation of Lemma 2.4(b) from the action of K on the tree of G (confirms the presentation). - **Theorem 3.1** (computer-assisted). No non-trivial homomorphism J -> S_n for n <= 36; no subgroup of index 2..36 in J or K. - **Lemma 4.1.** The search over class representatives a and C_T(a)-orbit representatives b (double cosets) is exhaustive. - **Theorem 4.2** (computer-assisted, GAP). No non-trivial homomorphism from J to a non-abelian simple group of order < 10^8 (stated for all homomorphisms, which is what the search gives and what Corollary 1.4 needs). - **Theorem 4.3** (computer-assisted, GAP). The same for the twelve simple groups of order in [10^8, 10^9) other than PSL2(q): S4(7), O8+(2), O8-(2), 3D4(2), L3(11), A12, M24, G2(4), L3(13), U3(13), McL, L4(4). - **Corollary 1.4.** Every non-trivial finite quotient of J or K has order >= 10^8; of K, >= 10^9 with Jambor. - **Proposition 5.1.** L_C *_H L_F maps onto A6 and PSL(2,7) (explicit permutations). - **Remark 5.2** (without proof). G, K, J are expected to be cocompact lattices in products of two trees. ## Computations (sanity checks; programs and outputs in reproducibility/) Theorems 3.1, 4.2 and 4.3 are computer-assisted; the proofs of Section 2 use no computation. - **The program of the note** (`check_note.py`, standard library, 27 s; 144 checks, 0 failures): word-level checks of Lemmas 2.3(c), 2.4(a); the abelianisations; coset enumerations for Lemma 2.3 (orders 12 and 24, [L : H] = 8, image of L on L/H of order 168); the D8 in both copies of S4; Proposition 5.1 with all involutions of S6, S7, S8; plain low-index searches (L up to index 10; J none up to 12; K none up to 7); the search of Lemma 4.1 in A5–A8, PSL(2,p) for p <= 31, M11, M12; the list of simple groups of order < 10^9 from the order formulas against the recorded GAP outputs (orders, skipped groups, conclusions, summary lines, the 124 values of q, the 74 groups of GQuotients); the recorded run of Theorem 3.1 and the H-orbit elimination on the list of run B. - **Programs with which the results were obtained** (`original/`): Python, the L-set enumeration with Sims' canonicity test and the D-role solver (N = 12, 20, 26, 32 single runs; N = 36 in three parts of 712, 764, 947 s and a search step of 11 s; 1156 transitive L-sets, 55862 configurations, D-role unsolvable in all), a self-test, the plain low-index search (J: index 1 only up to 12), the contrast example, the role table (degree <= 26: D, E never; F on 18 of 161), and a numpy search for A6, PSL(2,7), PSU3(5), PSp4(4); GAP 4.16.1, the search of Lemma 4.1 over all simple groups of order < 10^9 from `SimpleGroupsIterator` (PSL2(q) for q <= 577 searched separately, PSL2(q) in [10^8, 10^9) excluded by Jambor, Sz(q) by 3 not dividing the order), C+D = 0 in every group; and `GQuotients(J, T)` for 74 groups, 0 epimorphisms, with positive controls. - **Programs of verification run 3** (`independent_run_2/`, written for the final text; standard library except `r2_matrix.py`, numpy): `r2_structure.py` (33 checks), `r2_lsets.py 36` (25 checks: own a_n(L), the list of 1156 L-sets certified complete, H-orbit elimination, own role solver: D-role unsolvable in all 55862 configurations, roles on the L-sets of degree <= 26), `r2_simple.py` (28 checks: the lists of simple groups, every entry and mark of Table 2, Section 4.1), `r2_prop51.py` (14 checks), `r2_matrix.py L37`, `L43` (PSL3(7), PSL4(3) from matrices, no GAP: all pairs, C+D = 0, orbit counts of Table 2 reproduced). All checks passed. - **Re-runs at the writing stage.** `check_note.py` (full and quick); `k1646_lsets_selftest.py`, `k1646_lsets.py 20`, `k1646_CF_example.py`, `k1646_roles_table.py 26` (identical outputs); parts of the programs of both verification runs (identical); by verification run 3, from an extracted copy of the source archive, `check_note.py` and programs of `original/`, `verification_run_A/`, `verification_run_B/` and `independent_run_2/` (identical apart from running times). Details in `reproducibility/README.md`. ## Independent verification runs Two independent verification runs, both AI-assisted, examined the first write-up of the result (2026-10-24). Each re-derived the proofs of Section 2 and wrote its own programs. | Item | Run A | Run B | |---|---|---| | Statement, record, sources (Kourovka v48, v49; Conder 1992; Jambor arXiv v1) | CONFIRMED (sources read; v49 identical to v48, no comment) | CONFIRMED (same; Crossref data checked) | | Lemmas 2.1–2.4, Corollary 2.5, S4 in every image | PROVED (re-derived), including the Bass–Serre derivation of the presentation | PROVED (re-derived); Lemma 2.4(a) also checked at the level of words by machine | | Theorem 3.1 | CONFIRMED by own code (own enumeration and solver, N = 36 in two parts; same counts in every degree; no solution); direct search on J to index 16 | CONFIRMED by a different method: GAP's list of 1156 L-sets, completeness certified by an exact count of subgroups of L (amalgam structure, Hall's recursion), H-orbit elimination; GAP low-index on J to index 16 | | Theorem 4.2, PSL2(q), q <= 577 | CONFIRMED by own arithmetic in SL2(q), all q | CONFIRMED by own code for the primes 5 <= p <= 199 | | Theorem 4.2, other groups | list of groups checked complete from the order formulas; PSp4(4), PSU3(4), PSU3(5) by own code (exact agreement with the GAP counts) | own Python search for 22 groups (A6, PSL(2,7), A7, M11, L3(4), U3(3), L3(3), U4(2), A8, M12, A9, U3(4), L3(5), M22, J1, U3(5), S4(4), J2, L3(7), U4(3), G2(3), HS) on generators from GAP's primitive groups library; weighted GAP counts equal to the Python counts for 13 groups; GQuotients re-run for 5 groups | | Theorem 4.3 and the bound 10^9 | logic CONFIRMED; GAP part not re-run | M24 and O8-(2) by own Python search and weighted GAP enumeration; the other 10 groups rest on the original GAP run | | Proposition 5.1 | CONFIRMED (own relator check, order 360) | CONFIRMED (own construction of a degree-6 solution) | | Classification PARTIAL, novelty | CONFIRMED | CONFIRMED; no publication settles 16.46 | No run found an error in a statement or a proof. **Corrections required by the runs, all applied in the note:** 1. (Run A) Theorem 4.2 states the strong form: no non-trivial homomorphism, not only no epimorphism. 2. (Run A) The comparison of the 22 relators with Conder's printed presentation (a figure in the scan) is described: through the Kourovka text, Jambor's Proposition 12.2 and the Bass–Serre re-derivation (Remark 2.6). (Verification run 3 then read the display itself from the rendered scan; see below, item 1.) 3. (Run A) The dependencies are stated (Section 4.1): the bound 10^8 rests on GAP 4.16.1 alone for J1, J2, J3, HS, L3(7), L3(8), L3(9), U3(7), U3(8), U3(9), U3(11), U4(3), L4(3), U5(2), S4(5), G2(3), 2F4(2)' (for six of them run B's Python search used generators exported from GAP); the extension to 10^9 rests on GAP for twelve groups and on Jambor's Magma computation; PSL2(q), q <= 577, has three independent computations. (After verification run 3, which searched L3(7) and L4(3) from its own matrices, the list has 15 groups; see below.) 4. (Run A) [L : H] = 8 is stated and proved (Lemma 2.3(d)). 5. (Run B) The GAP counts are counts of C_T(a)-orbits of pairs, weighted by their sizes they give the Python counts; not counts divided by abs(C_T(a)) (Section 4, "Controls"). 6. (Run B) Jambor is cited as J. Algebra 423 (2015) 1109–1142, with Proposition 12.2 in the numbering of arXiv:1402.6788v1. 7. (Run B) The 124 values of q give 123 groups PSL2(q). 8. (Run B) The statement about cocompact lattices is a remark without proof (Remark 5.2). 9. (Run B) Djoković and Miller, J. Combin. Theory Ser. B 29 (1980) 195–230, is cited (Crossref checked). 10. (Run A) For the groups PSL2(q) with 10^8 <= abs(PSL2(q)) < 10^9 the note relies on Jambor's theorem alone. **Verification run 3 (final text of the note, 2026-10-24, AI-assisted).** It examined the text of the note itself: every proof re-derived in the note's wording (including Remark 2.6 and the reduction finite quotient -> simple quotient -> homomorphism of J in the proof of Corollary 1.4); the sources read again (Kourovka v48 and v49, page rendered; Conder 1992 in full, the display of p. 217 read from the rendered scan; Jambor arXiv v1, Section 12, the only arXiv version); the bibliography checked with Crossref (all nine DOIs); the literature search repeated (arXiv API, Crossref, OpenAlex, zbMATH Open, one web search; nothing on the question). Its own programs (`independent_run_2/`) confirmed Theorem 3.1 in full on a certified list, Table 1, every entry and mark of Table 2, the lists of simple groups of order < 10^8 and between 10^8 and 10^9, Proposition 5.1 and the controls, and searched PSL3(7) and PSL4(3) from matrices without GAP (no homomorphism of J; the orbit counts of Table 2 reproduced). It re-ran the package from the source archive (identical outputs apart from running times). It found no mathematical error. Its eleven corrections, all applied: 1. Remark 2.6 and "Scope and priority": the presentation in Conder 1992 is legible in the rendered scan (same 22 relators), not a figure that could not be read. 2. Section 3: one round of the H-orbit elimination empties both sides for J (not two; the programs count a confirming pass). 3. Section 4: the GQuotients check excludes epimorphisms; since J is perfect, epimorphisms suffice for the bound (the earlier sentence "the same strength for the groups it covers" was imprecise). 4. Sections 1.3, 4.1 and "Scope and priority": the re-check of Jambor's theorem is for the PSL2(q) of order < 10^8 (q <= 577, q != 512). 5. Remark 5.2: the unproved faithfulness of G on the tree Y was removed; the vertex stabilisers in T3 x Y are finite. 6. Section 4.1 and Table 2: PSL3(7) and PSL4(3) searched from own matrices; the bound 10^8 rests on GAP alone for 15 groups (J1, J2, J3, HS, L3(8), L3(9), U3(7), U3(8), U3(9), U3(11), U4(3), U5(2), S4(5), G2(3), 2F4(2)'), five of them searched again by run B on generators from GAP; L4(3) marked with a dagger. 7. Verification paragraph, Section 6, this report and the README: the third run recorded. 8. Section 1.1: no comment and no mark in v48, v49; the companion question for two copies of G4^1 mentioned. 9. "Scope and priority": the third run's searches (four web searches in all); Jambor's arXiv v1 is the only arXiv version. 10. README: `python3 -I` breaks the programs that import a module of their own folder; `vb_an_L.py 40 7`; the annotation in `out_vb_lemma4.txt`; the section on `independent_run_2/`. 11. Lemma 2.4(a): the comparison of relators is as cyclic words in the free product of , , . ## Relation to the literature, novelty and scope - **Searches** (22 and 24 October 2026): arXiv (API and listing pages: Conder's papers, the cubic tree, Kourovka 16.46, amalgams of arc-transitive groups, lattices in products of trees and finite quotients), zbMATH Open API, Crossref, OpenAlex (topic searches; works citing Conder 1992: 3; citing Jambor 2015: 6), Semantic Scholar (citations: 6 and 14 records), four web searches; repeated by verification run 3 on 24 October (arXiv API, Crossref, OpenAlex citing works and topic search 2024-2026, zbMATH Open, one web search). Read: Kourovka v48, v49; Conder 1992 (in full); Jambor, Section 12 of arXiv v1, the only arXiv version (the journal version was not compared); Jambor's thesis (RWTH Aachen 2012; does not mention K); Caprace, Finite and infinite quotients of discrete and indiscrete groups (arXiv:1709.05949v3; does not mention K); texts of works citing Jambor 2015 (Bridson–Evans–Liebeck–Segal; Nebe–Parker–Rees) do not mention K. A thesis of 2010 citing Conder 1992 could not be retrieved (HTTP status 504). - **Result.** No printed answer to the question was found in these sources; Jambor's Proposition 12.2 is the only published partial result found. A search that finds nothing is not a proof of novelty; no priority is claimed. - **Scope.** The question is open. The bounds are computer-assisted; the bound 10^8 rests on GAP 4.16.1 alone for 15 of the 159 searched groups (Section 4.1 of the note), and the bound 10^9 for K also depends on Jambor's Magma computation. Conder 1992 reports the failure to find a subgroup of finite index but no bound, so the extent of earlier unpublished searches is unknown. ## 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/