ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13

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.

Geodesics in the Poincare upper half-plane

Example

For the Poincaré metric $g = (d x^{2} + d y^{2}) / y^{2}$ on $H = {(x, y) \in R^{2} : y > 0}$ , every nonconstant affinely parametrized geodesic is a restriction of exactly one of the following forms, with $k \neq 0$ : $γ (t) = (a, b e^{k t}) (a \in R, b > 0),$ $γ (t) = (a + R \tanh (k t + c), R sech (k t + c)) (a, c \in R, R > 0) .$ Conversely, each displayed curve on all of $R$ is a geodesic and traces a whole vertical line or upper Euclidean semicircle $(x - a)^{2} + y^{2} = R^{2}$ orthogonal to the boundary $y = 0$ ; a restriction traces the corresponding subarc. Constant curves are the zero-speed geodesics. An affine change of parameter merely changes the constants in these displayed parametrizations.

Facts & Assumptions

Given: The upper half-plane $H$ , its displayed metric, and a geodesic on an interval $I$ .

[F1]

Christoffel formula for the levi civita connection computes Levi–Civita symbols from the metric matrix; Coordinate geodesic equation makes the coordinate ODE equivalent to the intrinsic geodesic condition.

[F2]

A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant makes a continuous function with zero interior derivative constant on an interval, including included endpoints.

[F3]

The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t gives $(\log y)^{'} = 1 / y$ for $y > 0$ , and The natural logarithm as the inverse of the exponential function makes $\log$ the inverse of $\exp$ on positive reals.

[F4]

The functions $\tanh$ and $sech$ are defined on all of $R$ by The six hyperbolic functions and their natural domains; Addition formulas, identities, parity, and derivatives of the hyperbolic functions gives $\tanh^{'} = {sech}^{2}$ , ${sech}^{'} = - sech \tanh$ , $\tanh^{2} + {sech}^{2} = 1$ , and the range $\tanh (R) = (- 1, 1)$ .

[F5]

The exponential function is smooth and $(\exp)^{'} = \exp$ gives $(\exp)^{'} = \exp$ .

[F6]

The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ gives $\exp (u + v) = \exp (u) \exp (v)$ .

[F7]

Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ gives the sum, product and quotient rules, and The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ differentiates the composites used below.

Verification

1.1

Here $(g_{i j}) = y^{- 2} I_{2}$ and $(g^{i j}) = y^{2} I_{2}$ . Applying the formula in [F1], the only nonzero symbols are $Γ^{x}_{x y} = Γ^{x}_{y x} = - 1 / y$ , $Γ^{y}_{x x} = 1 / y$ , and $Γ^{y}_{y y} = - 1 / y$ . Hence the two geodesic equations are $x^{''} - 2 x^{'} y^{'} / y = 0, y^{''} + (x^{' 2} - y^{' 2}) / y = 0.$

F1given

2.1

The first equation gives $(x^{'} / y^{2})^{'} = 0$ , so $C : = x^{'} / y^{2}$ is constant by [F2]. Differentiating $E : = (x^{' 2} + y^{' 2}) / y^{2}$ gives $E^{'} = \frac{2 x^{'}}{y^{2}} (x^{''} - 2 x^{'} y^{'} / y) + \frac{2 y^{'}}{y^{2}} (y^{''} + (x^{' 2} - y^{' 2}) / y) = 0.$ Thus $E$ is constant too. If $E = 0$ , positive definiteness forces $x^{'} = y^{'} = 0$ , and the curve is constant.

F2F7step 1.1given

3.1

If $C = 0$ , then $x^{'} = 0$ , so $x = a$ . The second equation becomes $(\log y)^{''} = (y^{''} y - y^{' 2}) / y^{2} = 0$ . By [F2], [F3] and [F7], $\log y = k t + d$ ; therefore [F6] gives $y = b e^{k t}$ with $b = e^{d} > 0$ . A nonconstant curve has $k \neq 0$ . Conversely, [F5] and [F7] give $x^{'} = 0$ and $y^{''} = y^{' 2} / y$ for $x = a$ , $y = b e^{k t}$ , so both equations in step 1.1 hold.

F2F3F5F6F7step 1.1step 2.1

3.2

Suppose $C \neq 0$ . Put $a : = x + y^{'} / (C y)$ . From the second equation and $x^{'} = C y^{2}$ , $a^{'} = x^{'} + (y^{''} y - y^{' 2}) / (C y^{2}) = C y^{2} - x^{' 2} / (C y^{2}) = 0.$ Thus $a$ is constant. Since $E > 0$ , set $R = \sqrt{E} / ∣ C ∣ > 0$ . Direct substitution into the identity defining $E$ gives $(x - a)^{2} + y^{2} = E / C^{2} = R^{2}$ . In particular $z : = (x - a) / R$ lies in $(- 1, 1)$ , and $y = R \sqrt{1 - z^{2}}$ .

F2F7step 1.1step 2.1

4.1

Define $u = \frac{1}{2} \log ((1 + z) / (1 - z))$ , which is defined because $∣ z ∣ < 1$ . The logarithm, chain and quotient rules give $u^{'} = z^{'} / (1 - z^{2})$ , while $z^{'} = x^{'} / R = C y^{2} / R = C R (1 - z^{2})$ ; hence $u^{'} = C R = : k \neq 0$ . By [F2], $u = k t + c$ . The inverse-log law in [F3] and exponential addition [F6] give $e^{2 u} = (1 + z) / (1 - z)$ , so the definitions in [F4] give $z = \tanh u$ ; since $y > 0$ and $1 - \tanh^{2} u = {sech}^{2} u$ , $y = R sech u$ . This yields the stated semicircle parametrization on the entire interval.

F2F3F4F6F7step 2.1step 3.2

5.1

Conversely, set $U = k t + c$ , $T = \tanh U$ , and $S = sech U$ . For $x = a + R T$ and $y = R S > 0$ , [F4] and [F7] give $x^{'} = R k S^{2}$ , $y^{'} = - R k S T$ , $x^{''} = - 2 R k^{2} S^{2} T$ , and $y^{''} = R k^{2} S (2 T^{2} - 1)$ . The first equation of step 1.1 has left side $- 2 R k^{2} S^{2} T + 2 R k^{2} S^{2} T = 0$ ; the second has left side $R k^{2} S (T^{2} + S^{2} - 1) = 0$ . These curves therefore are geodesics. The identity $(x - a)^{2} + y^{2} = R^{2}$ shows the circle meets $y = 0$ at right angles; $S > 0$ and the range of $\tanh$ show the whole upper semicircle is traced as $t$ ranges over $R$ .

F1F4F7step 1.1step 4.1

6.1

The alternatives $E = 0$ , $C = 0 < E$ , and $C \neq 0$ exhaust every geodesic. In the vertical case the curve determines $a = x$ , $k = (\log y)^{'}$ , $d = \log y - k t$ and $b = e^{d}$ . In the semicircle case its invariants determine $a = x + y^{'} / (C y)$ , $R = \sqrt{E} / ∣ C ∣$ , $k = C R$ , $u = \frac{1}{2} \log ((1 + z) / (1 - z))$ and $c = u - k t$ . Hence, for the fixed affine parameter, the displayed constants are unique. Steps 3.1 and 5.1 verify both nonconstant families, including their restrictions to intervals with endpoints. For an affine parameter change $t \mapsto α t + β$ with $α \neq 0$ , the first family changes $b, k$ and the second changes $k, c$ ; $α = 0$ yields a constant curve. No countable choice or geodesic existence theorem is used: the conclusion follows by integrating the given curve's own ODE.

F3step 2.1step 3.1step 3.2step 4.1step 5.1∎

Source locator

Datar, Example 15.1.6, p. 115, supplies the metric and coordinate geodesic equations. Its final printed circle equation has the coordinate roles of the center interchanged; the boundary-centered equation used here follows from the calculation in step 3.2.

Depends on

Used by

Hyperbolic space is complete Example

Dependency tree · two levels

52 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

Ved Datar, Lectures on Riemannian Geometry, Example 15.1.6, p. 115 (standard reference, not scraped)