§3 — $|\mathrm{Ni}_c|=7$ for $c=(2,23A,23B)$

Proved

MathieuM23.nielsenClass_ncard

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

group-theoryinverse-galois-problemmathieu-groupnielsen-class

For the classes $C_1=2$ , $C_2=23A$ , $C_3=23B$ of $M_{23}$ (the classes of $g_1,g_2,g_3$ ), the Nielsen class

\mathrm{Ni}_c=M_{23}\backslash\{(h_1,h_2,h_3)\in C_1\times C_2\times C_3: h_1h_2h_3=1,\ \langle h_1,h_2,h_3\rangle=M_{23}\}

has exactly $7$ elements:

|\mathrm{Ni}_c|=7.

Hence, by the Riemann existence theorem, there are exactly seven $M_{23}$ -covers of $\mathbb{P}^1_{\mathbb{C}}$ with this ramification data. The triple is therefore not rigid, and this is the starting point of the paper's construction.

Preamble

import Definitions.Def_MathieuM23_Nielsen

Formal statement

namespace MathieuM23

theorem nielsenClass_ncard : nielsenClass.ncard = 7 := 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, §3 ("This is

\{2, 23A, 23B\}

, with

|\mathrm{Ni}_c| = 7

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. The Nielsen class, defined as the set of $M_{23}$ -simultaneous-conjugation orbits of $\Sigma_c$ , has exactly $7$ elements. Here $\Sigma_c$ is the set of triples $(h_1,h_2,h_3)$ of permutations of $\{0,\dots,22\}$ with $h_i$ conjugate within $M_{23}$ to $g_i$ , $h_1h_2h_3=1$ , and $\langle h_1,h_2,h_3\rangle=M_{23}$ . Each orbit is the set of all $(kh_1k^{-1},kh_2k^{-1},kh_3k^{-1})$ , $k\in M_{23}$ . The count is the natural-number cardinality of a set of sets; it would be reported as $0$ if the set were infinite, which is impossible since there are finitely many triples. No hypotheses.

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 — ∣Nic∣=7|\mathrm{Ni}_c|=7∣Nic​∣=7 for c=(2,23A,23B)c=(2,23A,23B)c=(2,23A,23B)

§3 — $|\mathrm{Ni}_c|=7$ for $c=(2,23A,23B)$