Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedaudited 2026-09-22
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.

Hyperbolic space as so zero n one mod so n

Example

Assume the Axiom of Choice and let n2. Write v,w=i=1nviwivn+1wn+1 for the Lorentz form on Rn+1, let

Hn={vRn+1:v,v=1, vn+1>0}

be the upper sheet of the hyperboloid, and let G=SO0(n,1) be the identity component of the group of J-preserving matrices, J=diag(In,1). Then K=SO(n) is a maximal compact subgroup of G and the orbit map induces a diffeomorphism G/KHn; under it the Cartan metric of Riemannian symmetric pair of noncompact type is a G-invariant Riemannian metric on real hyperbolic n-space of constant sectional curvature 1/(2(n1)); equivalently the Cartan metric is 2(n1) times the standard normalization of curvature 1, namely the metric (2(n1))1Bθ (Cartan decomposition gives the invariant metric and curvature of G mod K, Cartan decomposition identifies p with the noncompact symmetric space).

Facts & Assumptions

Given: The Axiom of Choice; an integer n2; the Lorentz form , with matrix J; the groups O(n,1)={AGLn+1(R):ATJA=J}, SO(n,1)=O(n,1)SLn+1(R) and its identity component G=SO0(n,1); the hyperboloid Hn and its point e0=(0,,0,1).

[A1]

The Axiom of Choice is The Axiom of Choice; it enters through the closed-subgroup theorem, the quotient-manifold structure and the global Cartan decomposition used below.

[L1]

Every closed subgroup of a finite-dimensional real Lie group is an embedded Lie subgroup; GLn+1(R) is a Lie group with Lie algebra Mn+1(R); and SO(n)={R:RTR=I, detR=1} is a closed subgroup with Lie algebra so(n)={X:XT+X=0} (Cartan closed subgroup theorem, General and special linear Lie groups, Orthogonal and special orthogonal Lie groups). Closed and bounded subsets of a finite-dimensional real matrix space are compact by Heine-Borel in Rn: with the Euclidean metric a subset of Rn is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line.

[L2]

A regular level set of a smooth map is an embedded submanifold whose tangent space at a point is the kernel of the differential (A regular level set is an embedded submanifold, The tangent space of a regular level set is the kernel).

[L3]

The Killing form is B(X,Y)=tr(adXadY), and a finite-dimensional characteristic-zero Lie algebra is semisimple exactly when its Killing form is nondegenerate (Killing form, Cartan's semisimplicity criterion).

[L4]

For a Riemannian symmetric pair (G,K) of noncompact type with Cartan decomposition g0=k0p0, the form Bθ defines a G-invariant Riemannian metric on G/K with value Bθ at the origin, the curvature at the origin is R(X,Y)Z=[[X,Y],Z] for X,Y,Zp0, and the sectional curvature of a plane with basis X,Yp0 is Rm(X,Y,Y,X)/(Bθ(X,X)Bθ(Y,Y)Bθ(X,Y)2); moreover G/K is diffeomorphic to p0 by Xexp(X)K (Riemannian symmetric pair of noncompact type, Cartan decomposition gives the invariant metric and curvature of G mod K, Cartan decomposition identifies p with the noncompact symmetric space, Sectional curvature).

[L5]

G/K carries the unique smooth structure making the quotient map a submersion and the left G-action smooth, and the orbit map G/KHn, gKge0, is smooth and G-equivariant (Homogeneous spaces of Lie groups, Quotient manifold by a closed Lie subgroup).

[L6]

The matrix exponential is the Lie-group exponential of a matrix group, and the exponential map carries a neighborhood of 0 diffeomorphically onto a neighborhood of the identity (Matrix exponential as the Lie-group exponential, The exponential map is a local diffeomorphism at zero). Consequently the subgroup H generated by exp(g) is the identity component: H contains an open identity neighborhood and is therefore an open subgroup, while every path texp(tX) lies in the identity component, so HG0; the cosets of H make both H and its complement open in the connected group G0, forcing H=G0.

[L7]

For a connected real semisimple Lie group with finite center and a global Cartan involution, its fixed subgroup is maximal compact (Maximal compact subgroups exist and are conjugate in a connected finite center semisimple Lie group).

Verification

technique · direct matrix computation
1.1

The group O(n,1) is closed in GLn+1(R), so [L1] makes it an embedded Lie subgroup. Differentiating ATJA=J gives XTJ+JX=0; conversely this condition implies exp(tX)TJexp(tX)=J by differentiation in t, so it characterizes the Lie algebra. It consists of (AbbT0) with AT=A. Determinant has values ±1 on O(n,1), hence equals 1 on its identity component G. This component has the same Lie algebra. Write Xb=(0bbT0) and Kij=EijEji for i<jn.

L1L6algebra
1.2

The level function F(v)=v,v has differential dFv(w)=2v,w, nonzero at every F(v)=1. Thus [L2] gives tangent space v and dimension n. The upper sheet is the graph v=(u,1+u2), hence connected. Its Lorentz tangent metric is positive: if w=(a,b)v, then b=ua/1+u2 and w,wa2/(1+u2)>0 for w0. Every gG preserves this sheet, since the sign of the last coordinate of gv cannot change continuously on connected G.

L2algebra
1.3

The group SO(n) is compact, being closed and bounded in matrix space and hence compact by Heine--Borel in [L1], and is path connected: plane rotations can carry any unit first column to the first coordinate vector; after doing so the remaining block is in SO(n1), and induction ends with SO(1)={1}. Each plane rotation has a path to the identity through its angle. Therefore K={diag(R,1):RSO(n)} lies in G.

L1algebra
2.1

The basis Kij,Xi:=Xei satisfies [Kij,Xl]=δjlXiδilXj and [Xi,Xj]=Kij for i<j. For fixed Kij, its adjoint square is I on each two-dimensional span of the rotations joining i,j to a third spatial index, and on span(Xi,Xj); it vanishes on the remaining basis vectors. Its trace is 2(n2)2=2(n1). For fixed Xi, its adjoint square is +I on each span of Xj and the rotation joining i,j (ji), and zero on the rest, giving trace 2(n1). Mixed Killing pairings of different basis vectors vanish: conjugation by diag(ϵ1,,ϵn,1), ϵi=±1, is a Lie-algebra automorphism, preserves the adjoint trace, and acts with distinct sign characters ϵiϵj on Kij and ϵi on Xi. A sign choice therefore negates any mixed pairing while preserving it. This proves on the whole basis, hence bilinearly, B(X,Y)=(n1)tr(XY). It is nondegenerate for every n2, including n=3, so [L3] proves semisimplicity. The involution θX=XT has eigenspaces k=span(Kij) and p={Xb}, with Bθ(X,X)=(n1)tr(XXT)>0 for X0. Since [p,p]=k, no proper ideal contains p, so the noncompact-type criterion of [L4] is satisfied.

L3L4step 1.1algebra
2.2

The action is transitive: for v=(u,1+u2) with u0, put a=u/u and t0 with sinht=u. The matrix exponential gives exp(tXa)e0=(sinhta,cosht)=v and belongs to G; v=e0 uses the identity. The stabilizer of e0 consists exactly of diag(R,1) with RSO(n), since it preserves e0 and determinant one; these matrices are in G by step 1.3. Thus it is K.

L6step 1.1step 1.2step 1.3algebra
3.1

The smooth orbit map factors through the quotient submersion to a smooth bijection Φ:G/KHn by [L5] and step 2.2. Its derivative at eK, using g/kp, is Xb(b,0), an isomorphism. Equivariance makes the derivative an isomorphism everywhere, so the inverse function theorem gives a local diffeomorphism everywhere; a bijective local diffeomorphism has a smooth inverse.

L5step 2.1step 2.2algebra
3.2

The center of G is trivial. If z is central, ze0 is fixed by K; the only spatial vector fixed by all spatial rotations for n2 is zero. Since ze0Hn, it equals e0, so z=diag(R,1)K. Commuting with every exp(tXb) and differentiating forces Rb=b for every b, hence z=I. The group automorphism Θ(g)=(gT)1=JgJ preserves G, is involutive and differentiates to θ. Its fixed elements lie in both O(n+1) and O(n,1), hence commute with J and have block form diag(R,c); the upper-sheet condition gives c=1 and determinant one gives RSO(n). Thus GΘ=K. Together with step 2.1 this verifies all hypotheses of the symmetric-pair interface [L4].

L4step 2.1step 2.2algebra
4.1

Step 3.2 proves that G is connected semisimple with finite center, that Θ is a global Cartan involution, and that GΘ=K. Therefore [L7] applies directly and makes K maximal compact.

L7step 3.2
4.2

The metric of [L4] is now applicable by step 3.2. At the origin Bθ(Xa,Xb)=B(Xa,Xb)=2(n1)ab by step 2.1. Under dΦ, the Lorentz metric is ab. Both metrics are G-invariant, so the Cartan metric is 2(n1) times the Lorentz metric everywhere. For independent a,b let D=a2b2(ab)2>0. The bracket is [Xa,Xb]=diag(abTbaT,0), whose squared Bθ-norm is 2(n1)D, while the Gram determinant of Xa,Xb is 4(n1)2D. The sectional formula in [L4] therefore gives 1/(2(n1)) at the origin and, by transitivity, everywhere.

L4step 2.1step 3.1step 3.2algebra
5.1

Scaling a metric by a constant c>0 preserves its Levi-Civita connection and its curvature operator of type (1,3): the same connection remains torsion free and metric compatible. The sectional numerator scales by c and its Gram denominator by c2. Thus (2(n1))1Bθ, the Lorentz metric from step 4.2, has curvature 1. At n=2 the Cartan curvature is 1/2; at n=3 the direct trace proof remains valid. Rank n=1 is excluded because the algebra is abelian with zero Killing form and there are no tangent two-planes. AC covers the Lie-group, quotient, maximal-compact and symmetric-space interfaces; the finite matrix computations require no further choice.

A1L4step 4.2algebra

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

104 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