Lemma 3.1 — the Riemann–Hurwitz count giving genus $4$

Proved

MathieuM23.lemma_3_1_riemann_hurwitz

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

algebraic-curvesgroup-theorymathieu-group

The degree-23 cover $X_{\mathbb{C}}\to\mathbb{P}^1_{\mathbb{C}}$ with monodromy $(g_1,g_2,g_3)$ has genus $4$ . Its ramification is read off from the cycle types. $g_1$ has cycle type $1^7 2^8$ , so the fiber over the first branch point consists of eight points of ramification index $2$ and seven unramified points. $g_2$ and $g_3$ are $23$ -cycles, so the other two fibers are totally ramified. The Riemann–Hurwitz formula then gives

2\cdot 4-2=23\,(2\cdot0-2)+\big[8(2-1)+(23-1)+(23-1)\big].

Formalization Note The curve $X_{\mathbb{C}}$ itself (obtained via the Riemann existence theorem) is not formalized. The milestone records the combinatorial content of Lemma 3.1: the cycle types of $g_1,g_2,g_3$ and the Riemann–Hurwitz identity. Here the contribution of $g$ is $\sum_{\text{cycles}}(\ell-1)$ , the sum of the cycle lengths $\ell\ge2$ minus the number of such cycles.

Preamble

import Definitions.Def_MathieuM23_Group

Formal statement

namespace MathieuM23

theorem lemma_3_1_riemann_hurwitz :
    g₁.cycleType = Multiset.replicate 8 2 ∧ g₂.cycleType = {23} ∧ g₃.cycleType = {23} ∧
      (2 * 4 - 2 : ℤ) = 23 * (2 * 0 - 2) +
        (((g₁.cycleType.sum : ℤ) - g₁.cycleType.card) +
          ((g₂.cycleType.sum : ℤ) - g₂.cycleType.card) +
          ((g₃.cycleType.sum : ℤ) - g₃.cycleType.card)) := 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. 5, Lemma 3.1 and its proof

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:

the multiset of lengths of the nontrivial cycles (length $\ge2$ ) of $g_1$ is $\{2,2,2,2,2,2,2,2\}$ (eight 2's);
the multiset of nontrivial cycle lengths of $g_2$ is $\{23\}$ , and the same holds for $g_3$ ;
the integer identity $2\cdot4-2=23\cdot(2\cdot0-2)+\sum_{i=1}^{3}\big(s_i-n_i\big)$ holds, where $s_i$ is the sum and $n_i$ the number of nontrivial cycle lengths of $g_i$ . With items 1–2 this reads $6=-46+(16-8)+(23-1)+(23-1)$ .

No hypotheses. Nothing about a curve, a cover or a genus appears in the formal statement; only permutation cycle types and an arithmetic identity.

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

Lemma 3.1 — the Riemann–Hurwitz count giving genus 444

Lemma 3.1 — the Riemann–Hurwitz count giving genus $4$