§3 — $(g_1,g_2,g_3)\in\Sigma_c$ for $c=(2,23A,23B)$

Proved

MathieuM23.triple_mem_sigmaC

by Lucas · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

group-theorymathieu-groupnielsen-class

The explicit triple $(g_1,g_2,g_3)$ represents a point of the Nielsen class for the classes $(2,23A,23B)$ :

$(g_1,g_2,g_3)\in\Sigma_c$ , i.e. $g_1g_2g_3=1$ , $\langle g_1,g_2,g_3\rangle=M_{23}$ (in particular $g_3\in M_{23}$ ), and each $g_i$ lies in its own class;
$g_2$ and $g_3$ are not conjugate in $M_{23}$ , so the two classes of elements of order $23$ ( $23A$ and $23B$ ) are distinct;
$g_1$ has order $2$ and $g_2,g_3$ have order $23$ .

Formalization Note The classes $C_1,C_2,C_3$ are defined as the $M_{23}$ -classes of $g_1,g_2,g_3$ , so the substantive content is the product relation, generation, the orders, and the non-conjugacy of $g_2$ and $g_3$ .

Preamble

import Definitions.Def_MathieuM23_Nielsen

Formal statement

namespace MathieuM23

theorem triple_mem_sigmaC :
    (g₁, g₂, g₃) ∈ sigmaC ∧ g₃ ∉ classIn g₂ ∧
      orderOf g₁ = 2 ∧ orderOf g₂ = 23 ∧ orderOf g₃ = 23 := by sorry

end MathieuM23

Source

X. Huang, B. Jackson, K.-H. Lee, B. Poonen, R. Pries, S. Zhang, *The Mathieu group M23 is a Galois group over Q*, arXiv:2608.08538v1 (2026), https://arxiv.org/abs/2608.08538, p. 4–5, §3 ("We have

(g_1,g_2,g_3)\in\Sigma_c

") together with the class labels

2, 23A, 23B

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; non-blind

Disclosure — NON-BLIND read-back. This read-back was written by the same agent that drafted the Lean statement (Aristotle, by Harmonic), with full knowledge of the source paper and of the intended meaning. It is not independent, blind testimony and must not be mistaken for an independent audit; a reviewer should compare it against the Lean code directly.

Statement. All of the following hold, with $M_{23}=\langle g_1,g_2\rangle$ and $\mathrm{cl}(g)=\{kgk^{-1}:k\in M_{23}\}$ :

the triple $(g_1,g_2,g_3)$ lies in $\Sigma_c$ . Explicitly, $g_1\in\mathrm{cl}(g_1)$ , $g_2\in\mathrm{cl}(g_2)$ and $g_3\in\mathrm{cl}(g_3)$ ; these hold provided the identity lies in $M_{23}$ , which it does. Also $g_1g_2g_3=1$ as a composition of functions with $g_3$ applied first, and $\langle g_1,g_2,g_3\rangle=M_{23}$ ;
$g_3\notin\mathrm{cl}(g_2)$ : there is no $k\in M_{23}$ with $g_3=kg_2k^{-1}$ ;
the order of $g_1$ in the permutation group is $2$ , and the orders of $g_2$ and of $g_3$ are $23$ .

No hypotheses. Conjugacy of $g_2$ and $g_3$ in the full permutation group (which does hold, as both are 23-cycles) is not excluded; only conjugacy within $M_{23}$ is.

Human review

Endorsed by Shuze Chen · Oct 5, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

§3 — (g1,g2,g3)∈Σc(g_1,g_2,g_3)\in\Sigma_c(g1​,g2​,g3​)∈Σc​ for c=(2,23A,23B)c=(2,23A,23B)c=(2,23A,23B)

§3 — $(g_1,g_2,g_3)\in\Sigma_c$ for $c=(2,23A,23B)$