Hyperbolic distance and angles in the Poincaré disk; the vertices $a,b,c$

Definition

MathieuM23_HyperbolicDisk

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

hyperbolic-geometrytriangle-groups

Model the hyperbolic plane by the open unit disk $D=\{q\in\mathbb{C}:|q|<1\}$ with its metric $d$ of curvature $-1$ , for which

\cosh d(z,w)=1+\frac{2|z-w|^2}{(1-|z|^2)(1-|w|^2)}.

For a hyperbolic triangle with vertices $p,q,r$ , the interior angle at $p$ is the unique $\alpha\in[0,\pi]$ with

\cos\alpha=\frac{\cosh d(p,q)\cosh d(p,r)-\cosh d(q,r)}{\sinh d(p,q)\,\sinh d(p,r)}

(hyperbolic law of cosines). For $\theta\in(0,\pi/4)$ the source defines

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

Formalization Note The interior angle is defined through the hyperbolic law of cosines, with $\sinh d=\sqrt{\cosh^2 d-1}$ . In the disk model this agrees with the Euclidean angle between the geodesic arcs.

Definition code

import Mathlib

/-!
# Hyperbolic triangles in the Poincaré disk (Lemma 3.2)

The hyperbolic plane is modelled by the open unit disk `D = {q ∈ ℂ : |q| < 1}` with the
metric of constant curvature `-1`, for which
`cosh d(z, w) = 1 + 2|z - w|² / ((1 - |z|²)(1 - |w|²))`.
The interior angle of a hyperbolic triangle at a vertex is expressed through the hyperbolic law
of cosines.
-/

namespace MathieuM23

/-- `cosh d(z, w)` for the hyperbolic metric on the unit disk. -/
noncomputable def diskCoshDist (z w : ℂ) : ℝ :=
  1 + 2 * ‖z - w‖ ^ 2 / ((1 - ‖z‖ ^ 2) * (1 - ‖w‖ ^ 2))

/-- The interior angle at the vertex `p` of the hyperbolic triangle with vertices `p, q, r` in
the unit disk, defined by the hyperbolic law of cosines
`cos ∠p = (cosh d(p,q) cosh d(p,r) - cosh d(q,r)) / (sinh d(p,q) sinh d(p,r))`,
with `sinh d = √(cosh² d - 1)`. -/
noncomputable def diskAngle (p q r : ℂ) : ℝ :=
  Real.arccos
    ((diskCoshDist p q * diskCoshDist p r - diskCoshDist q r) /
      (Real.sqrt (diskCoshDist p q ^ 2 - 1) * Real.sqrt (diskCoshDist p r ^ 2 - 1)))

/-- The vertex `a = e^{-iθ} √(tan(π/4 - θ))`. -/
noncomputable def vertexA (θ : ℝ) : ℂ :=
  Complex.exp (-(θ : ℂ) * Complex.I) * (Real.sqrt (Real.tan (Real.pi / 4 - θ)) : ℂ)

/-- The vertex `b = 0`. -/
noncomputable def vertexB : ℂ := 0

/-- The vertex `c = √(cos 2θ)`. -/
noncomputable def vertexC (θ : ℝ) : ℂ := (Real.sqrt (Real.cos (2 * θ)) : ℂ)

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, definitions of

a,b,c

before 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.

All quantities are real or complex numbers; no restriction to the unit disk is built into the definitions.

Cosh-distance. For $z,w\in\mathbb{C}$ , $\Delta(z,w)=1+\dfrac{2|z-w|^2}{(1-|z|^2)(1-|w|^2)}$ , where $|\cdot|$ is the complex modulus. If $|z|=1$ or $|w|=1$ the denominator is $0$ and, by the convention that division by zero gives $0$ , $\Delta(z,w)=1$ . Outside the disk the formula is evaluated as written.
Angle. For $p,q,r\in\mathbb{C}$ , $\angle_p(q,r)=\arccos\left(\dfrac{\Delta(p,q)\Delta(p,r)-\Delta(q,r)}{\sqrt{\Delta(p,q)^2-1}\,\sqrt{\Delta(p,r)^2-1}}\right)$ . Here $\sqrt{\cdot}$ is the real square root, taken as $0$ on negative inputs. $\arccos$ is the real arccosine with values in $[0,\pi]$ , extended by $\arccos(y)=0$ for $y\ge1$ and $\pi$ for $y\le-1$ . Edge case: if $p=q$ or $p=r$ (so a square root vanishes), the quotient is $0$ by convention and the "angle" equals $\arccos 0=\pi/2$ .
Vertices. For real $\theta$ : $a(\theta)=e^{-i\theta}\cdot\sqrt{\tan(\pi/4-\theta)}$ (real square root, $0$ if the tangent is negative), $b=0$ , and $c(\theta)=\sqrt{\cos 2\theta}$ (real square root, regarded as a complex number).

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

Hyperbolic distance and angles in the Poincaré disk; the vertices a,b,ca,b,ca,b,c

Hyperbolic distance and angles in the Poincaré disk; the vertices $a,b,c$