ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-30

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Area defect of a hyperbolic geodesic triangle

Example

Assume the Axiom of Choice (The Axiom of Choice). In the upper-half-plane metric $y^{- 2} (d x^{2} + d y^{2})$ on $H = {y > 0}$ , a compact geodesic triangle of area $A$ has angle sum $π - A$ ; every such angle sum is therefore below $π$ .

Here a compact geodesic triangle means a compact regular disk region in the sense of Regular oriented surface regions with corners, with exactly three distinct vertices and boundary the cyclic concatenation of three regular $C^{2}$ embedded geodesic segments. At each vertex the incoming and outgoing one-sided unit tangents are not antipodal. Its angles are the interior sector angles, and its orientation is induced by $d x \land d y$ . Thus degenerate collinear triples and ideal vertices are not included.

Facts & Assumptions

Given: The Axiom of Choice, the upper half-plane $H = {y > 0}$ with the metric $g = y^{- 2} (d x^{2} + d y^{2})$ , a compact geodesic triangle $T \subseteq H$ in the regular disk-region sense specified above, of Riemannian area $A$ , and the outward-normal-first orientation of $\partial T$ .

[F1]

For an oriented Riemannian surface with a smooth positive orthonormal frame $(E_{1}, E_{2})$ on an open set and connection form $ω (X) = g (\nabla_{X} E_{1}, E_{2})$ , one has $d ω = - K d A$ , where $K$ is the sectional curvature of the frame plane and $d A$ the Riemannian volume form of the orientation (Gaussian curvature structure equation).

[F2]

In coordinates the Levi-Civita symbols of a Riemannian metric are $Γ^{k}_{i j} = \frac{1}{2} \sum_{ℓ} g^{k ℓ} (\partial_{i} g_{j ℓ} + \partial_{j} g_{i ℓ} - \partial_{ℓ} g_{i j})$ (Christoffel formula for the levi civita connection).

[F3]

The Riemannian volume form of an oriented Riemannian manifold is the unique positive top form with $d A (E_{1}, \dots, E_{n}) = 1$ on every positive orthonormal frame; in particular for a positive orthonormal coframe $(e^{1}, e^{2})$ of a surface, $d A = e^{1} \land e^{2}$ (The riemannian volume form is the unique positive unit top form, Riemannian volume form on an oriented manifold).

[F4]

Under AC, for a positively oriented compact regular disk region with exactly three vertices whose boundary is the cyclic concatenation of three regular $C^{2}$ geodesic segments with non-antipodal one-sided tangents and which lies in a frameable neighbourhood, $\int_{T} K d A = α + β + γ - π$ , where $α, β, γ$ are the interior sector angles (Gauss-Bonnet for a geodesic triangle).

[F5]

The Axiom of Choice is the choice-function principle (The Axiom of Choice). It licenses the AC-qualified geodesic formula used at step 2.2.

Verification

technique · exhibit a global positive orthonormal frame, compute its connection form and curvature by the structure equation, then insert $K\equiv-1$ into the geodesic-triangle formula

1.1given

On $H$ oriented so that $(\partial_{x}, \partial_{y})$ is positive, the fields $e_{1} = y \partial_{x}$ and $e_{2} = y \partial_{y}$ are smooth and globally defined. Their Gram matrix is the identity because $g (e_{1}, e_{1}) = y^{2} \cdot y^{- 2} = 1$ , $g (e_{2}, e_{2}) = y^{2} \cdot y^{- 2} = 1$ and $g (e_{1}, e_{2}) = 0$ ; hence $(e_{1}, e_{2})$ is a global smooth positive orthonormal frame.

2.1F2step 1.1algebra

With $g_{x x} = g_{y y} = y^{- 2}$ and $g_{x y} = 0$ , all $x$ -derivatives of the coefficients vanish and $\partial_{y} g_{x x} = \partial_{y} g_{y y} = - 2 y^{- 3}$ . Formula [F2] gives $Γ^{x}_{x y} = Γ^{x}_{y x} = \frac{1}{2} y^{2} (- 2 y^{- 3}) = - 1 / y$ , $Γ^{y}_{x x} = \frac{1}{2} y^{2} (2 y^{- 3}) = 1 / y$ and $Γ^{y}_{y y} = \frac{1}{2} y^{2} (- 2 y^{- 3}) = - 1 / y$ , while all remaining symbols vanish.

2.2F4F5step 1.1given

Let $T$ be the supplied compact geodesic triangle of area $A$ , regarded with the orientation induced from $d x \land d y$ on $H$ ; its boundary receives the outward-normal-first orientation. Thus $T$ is positively oriented relative to the ambient area form. By the disk-region hypothesis it is a compact regular oriented disk region with exactly three vertices, its sides are regular $C^{2}$ geodesic segments with non-antipodal one-sided tangents, and the global frame of step 1.1 supplies a frameable neighbourhood. Under the assumed AC [F5], [F4] applies: $\int_{T} K d A = α + β + γ - π$ for the interior sector angles.

3.1step 2.1algebra

The coordinate formulas of step 2.1 give $\nabla_{\partial_{x}} \partial_{x} = (1 / y) \partial_{y}$ and $\nabla_{\partial_{y}} \partial_{x} = - (1 / y) \partial_{x}$ . Since $\nabla_{e_{1}} e_{1} = y \nabla_{\partial_{x}} (y \partial_{x}) = y ((\partial_{x} y) \partial_{x} + y \nabla_{\partial_{x}} \partial_{x}) = y \partial_{y} = e_{2}$ and $\nabla_{e_{2}} e_{1} = y \nabla_{\partial_{y}} (y \partial_{x}) = y ((\partial_{y} y) \partial_{x} + y \nabla_{\partial_{y}} \partial_{x}) = y (\partial_{x} - \partial_{x}) = 0$ , the connection form satisfies $ω (e_{1}) = g (e_{2}, e_{2}) = 1$ and $ω (e_{2}) = 0$ . Hence $ω$ is the coframe element dual to $e_{1}$ , namely $e^{1} = d x / y$ .

4.1F3step 3.1algebra

Therefore $d ω = d (d x / y) = y^{- 2} d x \land d y$ . The dual coframe is $e^{1} = d x / y$ and $e^{2} = d y / y$ , so $e^{1} \land e^{2} = y^{- 2} d x \land d y$ ; by [F3] this is the Riemannian volume form $d A$ of the chosen orientation, and $d ω = d A$ .

5.1F1step 1.1step 4.1algebra

The structure equation [F1] applied to the frame of step 1.1 gives $d ω = - K d A$ ; with step 4.1 this forces $K \equiv - 1$ on $H$ . Consequently, for any positively oriented compact surface region $T$ inside the frameable open set $H$ , $\int_{T} K d A = - \int_{T} d A = - A$ .

6.1step 5.1step 2.2algebra∎

Substituting the value $\int_{T} K d A = - A$ of step 5.1 into step 2.2 gives $α + β + γ = π - A$ . The interior of a nonempty disk region is nonempty and the area form $y^{- 2} d x \land d y$ is positive there, so $A > 0$ and consequently $α + β + γ < π$ : every such hyperbolic angle sum is a strict area defect of $π$ .

Source locator

Lee, Riemannian Manifolds: An Introduction to Curvature, Chapter 9, printed pp. 156-172, works the constant-curvature examples through the local Gauss-Bonnet formula, and Datar, Lectures on Riemannian Geometry, Lecture 2, Theorem 2.0.1 together with the Poincare upper half-plane model, records the same computation. The Christoffel symbols are evaluated here from Christoffel formula for the levi civita connection on the explicit frame $(y \partial_{x}, y \partial_{y})$ , and the curvature is read off from Gaussian curvature structure equation; the angle formula is Gauss-Bonnet for a geodesic triangle. No global result about hyperbolic geometry beyond this local computation is used.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

26 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

John M. Lee, Riemannian Manifolds: An Introduction to Curvature (1997) (standard reference, not scraped)
Ved Datar, Lectures on Riemannian Geometry (standard reference, not scraped)