LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Polar decomposition of a real indefinite orthogonal matrix

Statement

Let $p, q \geq 0$ , $J = diag (I_{p}, - I_{q})$ , and $A \in O (p, q) = {A \in {GL}_{p + q} (R) : A^{T} J A = J}$ . There are unique matrices $K$ and $P$ such that

$A = K P, K \in O (p) \times O (q), P = (A^{T} A)^{1 / 2} > 0.$

Moreover $P J P = J$ , $X = \log P$ is symmetric and satisfies $J X J = - X$ , and $K \exp (s X) \in O (p, q)$ for every real $s$ . Thus $A$ is joined to its block-diagonal orthogonal factor $K$ by a path in $O (p, q)$ ; if $\det A = 1$ , the path lies in $S O (p, q)$ .

Facts & Assumptions

Given: The matrix $J$ and $A^{T} J A = J$ as in the Statement.

[F1]

Every self-adjoint endomorphism of a finite-dimensional real inner-product space has an orthonormal eigenbasis (Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis).

Proof

technique · direct

1.1givenalgebraconstruct

If $p + q = 0$ , there is one $0 \times 0$ matrix, and $A = K = P = I_{0}$ , $X = 0$ satisfy every assertion. If $p + q = 1$ , write $A = (a)$ ; $A^{T} J A = J$ gives $a^{2} = 1$ , so $P = (1)$ , $K = A$ , and $X = 0$ , and the factorization and path assertions follow. For $p + q \geq 2$ , set $M = A^{T} A$ . For $x \neq 0$ , $x^{T} M x = ∥ A x ∥^{2} > 0$ , so $M$ is positive definite and symmetric. The relation $A^{T} J A = J$ gives $A^{- 1} = J A^{T} J$ and, by transposition, $A^{- T} = J A J$ . Hence $J M J = J A^{T} A J = A^{- 1} A^{- T} = M^{- 1}$ .

2.1F1step 1.1construct

By [F1], diagonalize $M$ in an orthonormal basis; all its eigenvalues $λ_{i}$ are positive. Define $P$ to have eigenvalues $\sqrt{λ_{i}}$ in that basis. Then $P$ is symmetric positive definite and $P^{2} = M$ . If $R$ is another symmetric positive definite root, it commutes with $M = R^{2}$ and preserves each eigenspace of $M$ ; on the $λ$ -eigenspace, [F1] diagonalizes $R$ and positivity forces every eigenvalue to be $\sqrt{λ}$ . Thus $R = P$ .

3.1step 1.1step 2.1algebra

Both $J P J$ and $P^{- 1}$ are symmetric positive definite roots of $M^{- 1} = J M J$ . Uniqueness in step 2.1 yields $J P J = P^{- 1}$ , hence $P J = J P^{- 1}$ and $P^{- 1} J P^{- 1} = J$ .

4.1step 1.1step 3.1algebra

Put $K = A P^{- 1}$ . Then $K^{T} K = P^{- 1} A^{T} A P^{- 1} = I$ , and $K^{T} J K = P^{- 1} A^{T} J A P^{- 1} = P^{- 1} J P^{- 1} = J$ . Thus $K$ is Euclidean orthogonal and preserves $J$ ; multiplying $K^{T} J K = J$ by $K$ shows $J K = K J$ , so $K$ is block diagonal in the positive and negative coordinates. The factorization is unique because its positive factor must be the positive square root of $A^{T} A$ .

5.1F1step 3.1step 4.1algebra∎

Diagonalize $P$ by [F1] and define $X = \log P$ by replacing each positive eigenvalue $λ$ by $\log λ$ . Then $X$ is symmetric. Conjugation by $J$ preserves the matrix logarithm, so $J X J = \log (J P J) = \log (P^{- 1}) = - X$ . Consequently $J \exp (s X) J = \exp (- s X) = \exp (s X)^{- 1}$ ; because $K$ commutes with $J$ and is orthogonal, $K \exp (s X)$ preserves $J$ . At $s = 0$ this is $K$ and at $s = 1$ it is $A$ . Its determinant is constant and equals $\det A$ , proving the path assertion.

Remarks

When $p, q > 0$ , $K$ lies in $S (O (p) \times O (q))$ if $A \in S O (p, q)$ . The two possible common signs of $\det K ∣_{R^{p}}$ and $\det K ∣_{R^{q}}$ are analyzed in The even Clifford norm detects the identity component in mixed signature.

Depends on

Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis

Used by

The even Clifford norm detects the identity component in mixed signature Lemma

Dependency tree · two levels

4 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

Eckhard Meinrenken, Lie groups and Clifford algebras, Chapter 1 §6 and Chapter 2 §4.1 (standard reference, not scraped)