Lemma 3.2 — the hyperbolic triangle with angles $\pi/2,\theta,\theta$

Proved

MathieuM23.lemma_3_2_hyperbolic_triangle

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

hyperbolic-geometrytriangle-groups

Let $\theta\in(0,\pi/4)$ and let

a=e^{-i\theta}\sqrt{\tan\left(\tfrac{\pi}{4}-\theta\right)},\qquad b=0,\qquad c=\sqrt{\cos2\theta}.

Then $a,b,c$ are the vertices of a hyperbolic triangle in the Poincaré disk $D$ with interior angles $\pi/2$ at $a$ , $\theta$ at $b$ , and $\theta$ at $c$ .

With $\theta=\pi/23$ , the source uses this triangle to define the triangle group $\Delta$ generated by hyperbolic rotations by $2\pi/2, 2\pi/23, 2\pi/23$ around $a,b,c$ .

Formalization Note "Vertices of a hyperbolic triangle" is formalized as: the three points lie in the open unit disk and are pairwise distinct. The interior angles are computed by the hyperbolic law of cosines from the disk metric.

Preamble

import Definitions.Def_MathieuM23_HyperbolicDisk

Formal statement

namespace MathieuM23

theorem lemma_3_2_hyperbolic_triangle (θ : ℝ) (hθ₀ : 0 < θ) (hθ₁ : θ < Real.pi / 4) :
    ‖vertexA θ‖ < 1 ∧ ‖vertexB‖ < 1 ∧ ‖vertexC θ‖ < 1 ∧
      vertexA θ ≠ vertexB ∧ vertexB ≠ vertexC θ ∧ vertexA θ ≠ vertexC θ ∧
      diskAngle (vertexA θ) vertexB (vertexC θ) = Real.pi / 2 ∧
      diskAngle vertexB (vertexA θ) (vertexC θ) = θ ∧
      diskAngle (vertexC θ) (vertexA θ) vertexB = θ := 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.2

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. Let $\theta$ be a real number with $0<\theta<\pi/4$ (both strict). Put $a=e^{-i\theta}\sqrt{\tan(\pi/4-\theta)}$ , $b=0$ and $c=\sqrt{\cos2\theta}$ , with real square roots regarded as complex numbers. Then all of the following hold:

$|a|<1$ , $|b|<1$ , $|c|<1$ ;
$a\ne b$ , $b\ne c$ , $a\ne c$ ;
$\angle_a(b,c)=\pi/2$ , $\angle_b(a,c)=\theta$ and $\angle_c(a,b)=\theta$ .

Here, for points $p,q,r$ ,

\angle_p(q,r)=\arccos\frac{\Delta(p,q)\Delta(p,r)-\Delta(q,r)}{\sqrt{\Delta(p,q)^2-1}\sqrt{\Delta(p,r)^2-1}},\qquad \Delta(z,w)=1+\frac{2|z-w|^2}{(1-|z|^2)(1-|w|^2)},

with the definition file's conventions: division by $0$ gives $0$ , the real square root is $0$ on negatives, and $\arccos$ is clamped to $[0,\pi]$ . Because the points are required to be distinct and inside the disk, the degenerate "angle $=\pi/2$ by division by zero" case cannot occur at $a$ . The angle is defined by the law-of-cosines formula, not by tangent vectors of geodesics.

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.2 — the hyperbolic triangle with angles π/2,θ,θ\pi/2,\theta,\thetaπ/2,θ,θ

Lemma 3.2 — the hyperbolic triangle with angles $\pi/2,\theta,\theta$