Betweenness in the Poincaré disc: the hyperbolic geodesic is unique

Poincare/Geodesic.lean shows that the Poincaré disc is a geodesic metric space: the Euclidean diameters, reparametrised by Real.tanh, are unit-speed geodesic lines, and moving one of them by a disc automorphism joins any prescribed pair of points. It leaves open the converse — that these are the only geodesics — and it is the converse that this file supplies.

Everything follows from one betweenness criterion, which says that the hyperbolic segment issued from the origin is the Euclidean radius:

hyperbolicDist 0 m + hyperbolicDist m w = hyperbolicDist 0 w ↔ m ∈ segment ℝ 0 w.

The implication ← is TauCeti.hyperbolicDist_zero_add_hyperbolicDist_ofReal_mul, already proved in Poincare/Geodesic.lean. The implication → is the new content, and it comes from the equality case of a triangle inequality. Writing A = ‖m‖, B = ‖w‖ and ρ for the pseudo-hyperbolic expression TauCeti.pseudoHyperbolicExpr m w, the addition formula for Real.artanh turns the hypothesis into (A + ρ) / (1 + A ρ) = B, hence into ρ = |A - B| / (1 - A B): the reverse pseudo-hyperbolic triangle inequality against the origin, TauCeti.abs_sub_div_one_sub_mul_le_pseudoHyperbolicExpr_of_norm_lt_one, is tight. Its equality case (proved in Hyperbolic/Triangle.lean from the Poincaré defect factorisation) says that this happens exactly when (m * conj w).re = ‖m‖ * ‖w‖, and that — with A ≤ B, which the nonnegativity of ρ forces — is exactly the statement that m lies on the Euclidean radius towards w. The mirror equality case, for the origin sitting in the middle rather than at an end, is proved the same way and identifies (z * conj w).re = -(‖z‖ * ‖w‖) with 0 ∈ segment ℝ z w.

Both of those last identifications are Euclidean, not hyperbolic, and hold in any real inner product space: (z * conj w).re is the real inner product of ℂ (Complex.inner), and the criteria are TauCeti.mem_segment_zero_left_iff_real_inner_eq_norm_mul_and_norm_le and TauCeti.zero_mem_segment_iff_real_inner_eq_neg_norm_mul of TauCeti/Analysis/Convex/Segment.lean, consumed here through that one translation.

Three geometric consequences follow, in increasing strength:

• a point at prescribed distance from z on a hyperbolic segment from z to w is unique, which is the Menger-convexity statement Poincare/Geodesic.lean proved only in its existence half;
• two unit-speed geodesics with the same pair of endpoints agree on the parameter interval between them — the Poincaré disc is uniquely geodesic;
• every unit-speed geodesic line through the origin is a radial one, TauCeti.PoincareDisc.radialGeodesic u for a unique direction u : Circle, which is the converse classification Poincare/Geodesic.lean explicitly left unproved.

The general case of a geodesic through an arbitrary point needs no separate argument: the disc automorphisms act transitively by isometries (TauCeti.PoincareDisc.unitDiscMoebiusIsometryEquiv), which is exactly how the betweenness criterion is transported off the origin in TauCeti.PoincareDisc.eq_of_dist_add_dist_eq. TauCeti.PoincareDisc.existsUnique_eq_geodesicLine records that transport for the classification itself, dropping the hypothesis that the line starts at the origin: it is the origin statement applied to fun t => unitDiscMoebiusIsometryEquiv (toUnitDisc (γ 0)) (γ t).

Main results

• TauCeti.hyperbolicDist_zero_add_eq_iff_of_norm_lt_one — the hyperbolic segment from the origin is the Euclidean radius.
• TauCeti.hyperbolicDist_add_zero_eq_iff_of_norm_lt_one — the origin is hyperbolically between two points exactly when it is Euclidean-between them.
• TauCeti.PoincareDisc.eq_of_dist_add_dist_eq — a point between z and w is determined by its distance to z.
• TauCeti.PoincareDisc.existsUnique_dist_eq_of_mem_Icc — the unique-Menger-convexity upgrade of TauCeti.PoincareDisc.exists_dist_eq_of_mem_Icc.
• TauCeti.PoincareDisc.eqOn_Icc_of_isometry — the Poincaré disc is uniquely geodesic.
• TauCeti.PoincareDisc.existsUnique_eq_radialGeodesic — every geodesic line through the origin is a Euclidean diameter, for a unique direction.
• TauCeti.PoincareDisc.existsUnique_eq_geodesicLine — the same statement with no restriction on the base point: every geodesic line is TauCeti.PoincareDisc.geodesicLine (γ 0) u for a unique direction.

This advances the conformal-mapping roadmap's L2 target "the hyperbolic / Poincaré metric on 𝔻" (see ConformalMapping/README.md), completing the geodesic description that Poincare/Geodesic.lean began. It reuses Tau Ceti's pseudo-hyperbolic, hyperbolic-distance and disc-automorphism API throughout, and TauCeti/Analysis/Convex/Segment.lean — itself built on Mathlib's segment and SameRay — for the Euclidean side. As with the rest of the L0--L3 conformal-mapping material it is coordinated with the upstream Mathlib Riemann-mapping effort leanprover-community/mathlib4#33505 and the preceding human-curated work in Analysis/Complex/RiemannMapping.lean and Analysis/Complex/BranchLogRoot.lean; none of that material contains a Poincaré metric on the disc, and Mathlib's hyperbolic geometry on the upper half-plane (Analysis/Complex/UpperHalfPlane) has no geodesics, so nothing here duplicates it. Should a human-curated Poincaré disc land upstream, this file should be refactored onto it.

Euclidean segments through the origin, in terms of (z * conj w).re

The two criteria of this section are the statements of TauCeti/Analysis/Convex/Segment.lean — which hold in any real inner product space — transcribed into the Hermitian language ℂ supplies for its own inner product. They stay private: the exported statements of this file are the hyperbolic ones below.

Hyperbolic betweenness

@[simp]

theorem TauCeti.hyperbolicDist_zero_add_eq_iff_of_norm_lt_one {m w : ℂ} (hm : ‖m‖ < 1) (hw : ‖w‖ < 1) : hyperbolicDist 0 m + hyperbolicDist m w = hyperbolicDist 0 w ↔ m ∈ segment ℝ 0 w

The hyperbolic segment issued from the origin is the Euclidean radius. A point m of the disc satisfies hyperbolicDist 0 m + hyperbolicDist m w = hyperbolicDist 0 w — it is hyperbolically between the origin and w — exactly when it lies on the Euclidean segment from 0 to w.

The implication ← is TauCeti.hyperbolicDist_zero_add_hyperbolicDist_ofReal_mul. For →, the addition formula Real.artanh_add and the injectivity of Real.artanh on Ioo (-1) 1 turn the hypothesis into (‖m‖ + ρ) / (1 + ‖m‖ ρ) = ‖w‖, hence into ρ (1 - ‖m‖ ‖w‖) = ‖w‖ - ‖m‖, where ρ = pseudoHyperbolicExpr m w; that is the equality case TauCeti.pseudoHyperbolicExpr_eq_abs_sub_div_one_sub_mul_iff_of_norm_lt_one of the reverse pseudo-hyperbolic triangle inequality, and ρ ≥ 0 supplies ‖m‖ ≤ ‖w‖.

@[simp]

theorem TauCeti.hyperbolicDist_add_zero_eq_iff_of_norm_lt_one {w z : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : hyperbolicDist z 0 + hyperbolicDist 0 w = hyperbolicDist z w ↔ 0 ∈ segment ℝ z w

The origin lies hyperbolically between two points exactly when it lies Euclidean-between them. The mirror of TauCeti.hyperbolicDist_zero_add_eq_iff_of_norm_lt_one, obtained from the equality case TauCeti.pseudoHyperbolicExpr_eq_add_div_one_add_mul_iff_of_norm_lt_one of the strong pseudo-hyperbolic triangle inequality in the same way.

Uniqueness of geodesics

theorem TauCeti.PoincareDisc.eq_of_dist_add_dist_eq {z w m₁ m₂ : PoincareDisc} (h₁ : dist z m₁ + dist m₁ w = dist z w) (h₂ : dist z m₂ + dist m₂ w = dist z w) (h : dist z m₁ = dist z m₂) : m₁ = m₂

A point between z and w is determined by its distance to z. The Poincaré disc has no two distinct hyperbolic segments joining a given pair of points.

The Moebius isometry TauCeti.PoincareDisc.unitDiscMoebiusIsometryEquiv carries z to the origin, where TauCeti.hyperbolicDist_zero_add_eq_iff_of_norm_lt_one places both candidates on the Euclidean radius towards the image of w; on that radius the distance to the origin is a strictly monotone function of the Euclidean norm, so it separates points.

theorem TauCeti.PoincareDisc.existsUnique_dist_eq_of_mem_Icc (z w : PoincareDisc) {r : ℝ} (hr : r ∈ Set.Icc 0 (dist z w)) : ∃! p : PoincareDisc, dist z p = r ∧ dist p w = dist z w - r

Menger convexity, with uniqueness. For 0 ≤ r ≤ dist z w there is exactly one point at distance r from z and dist z w - r from w. The existence half is TauCeti.PoincareDisc.exists_dist_eq_of_mem_Icc.

theorem TauCeti.PoincareDisc.eqOn_Icc_of_isometry {γ₁ γ₂ : ℝ → PoincareDisc} {z w : PoincareDisc} (h₁ : Isometry γ₁) (h₂ : Isometry γ₂) (hz₁ : γ₁ 0 = z) (hz₂ : γ₂ 0 = z) (hw₁ : γ₁ (dist z w) = w) (hw₂ : γ₂ (dist z w) = w) : Set.EqOn γ₁ γ₂ (Set.Icc 0 (dist z w))

The Poincaré disc is uniquely geodesic. Two unit-speed geodesics that start at z at time 0 and reach w at time dist z w agree at every intermediate time. Together with TauCeti.PoincareDisc.exists_isometry_apply_zero_apply_dist, which produces one such geodesic, this says that hyperbolic segments exist and are unique.

theorem TauCeti.PoincareDisc.existsUnique_eq_radialGeodesic {γ : ℝ → PoincareDisc} (hγ : Isometry γ) (h0 : γ 0 = Complex.UnitDisc.toPoincare 0) : ∃! u : Circle, γ = radialGeodesic u

Every geodesic line through the origin is a Euclidean diameter. This is the converse to TauCeti.PoincareDisc.isometry_radialGeodesic, and it completes the description of the geodesics of the Poincaré disc: an isometric embedding of the real line sending 0 to the origin is one of the radial geodesics TauCeti.PoincareDisc.radialGeodesic u.

On the nonnegative half-line the hypothesis places γ t and γ 1 on a common Euclidean radius — whichever of the two is nearer the origin lies on the segment towards the other — so γ t is a nonnegative multiple of γ 1, and its norm is pinned to Real.tanh t by its distance to the origin. On the negative half-line the origin is between γ t and γ (-t), which by TauCeti.hyperbolicDist_add_zero_eq_iff_of_norm_lt_one puts the two on opposite radii, at equal distance from the origin; so γ t = -γ (-t), and Real.tanh is odd.

The direction is unique: evaluating radialGeodesic u = radialGeodesic v at time 1 gives u * Real.tanh 1 = v * Real.tanh 1, and Real.tanh 1 ≠ 0 because Real.tanh is injective. In particular u ↦ radialGeodesic u is injective, so distinct directions give distinct lines.

theorem TauCeti.PoincareDisc.existsUnique_eq_geodesicLine {γ : ℝ → PoincareDisc} (hγ : Isometry γ) : ∃! u : Circle, γ = (γ 0).geodesicLine u

Every geodesic line of the Poincaré disc is a TauCeti.PoincareDisc.geodesicLine. This removes the restriction to the origin from TauCeti.PoincareDisc.existsUnique_eq_radialGeodesic: an isometric embedding γ of the real line is geodesicLine (γ 0) u for one and only one direction u : Circle, with no hypothesis on where it starts.

As the introduction says, the general case needs no separate argument. The composite fun t => unitDiscMoebiusIsometryEquiv (toUnitDisc (γ 0)) (γ t) is again an isometric embedding and now sends 0 to the origin, so the origin case applies to it; undoing that Moebius isometry turns its conclusion into the statement here.