LemmaStatement: AI-adaptedProof: AI-generatedprecheck pass

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.

The change between two future-directed tetrads is a Lorentz matrix

Statement

Let $(M, g, N)$ be a time-oriented smooth Lorentzian four-manifold, let $p \in M$ , and let $E = (E_{0}, E_{1}, E_{2}, E_{3})$ and $F = (F_{0}, F_{1}, F_{2}, F_{3})$ be two future-directed tetrads at $p$ (Local frame fields, coordinate frames and tetrad fields). Write $η = diag (- 1, 1, 1, 1)$ . Then there is a unique real $4 \times 4$ matrix $Λ = (Λ^{B}_{A})$ such that $F_{A} = \sum_{B} Λ^{B}_{A} E_{B}$ for all $A$ , and:

$\sum_{C, D} Λ^{C}_{A} η_{C D} Λ^{D}_{B} = η_{A B}$ for all $A, B$ ; equivalently $Λ^{T} η Λ = η$ .
$Λ$ is invertible and $\det Λ = \pm 1$ .
$Λ^{0}_{0} > 0$ .
For every covariant $2$ -tensor $T$ at $p$ , its components in the two tetrads satisfy $T (F_{A}, F_{B}) = \sum_{C, D} Λ^{C}_{A} Λ^{D}_{B} T (E_{C}, E_{D})$ . More generally, for a type $(r, s)$ tensor at $p$ each contravariant slot contributes a factor $(Λ^{- 1})^{A}_{B}$ and each covariant slot a factor $Λ^{A}_{B}$ .

Facts & Assumptions

Given: A time-oriented smooth Lorentzian four-manifold $(M, g, N)$ , a point $p \in M$ , and two future-directed tetrads $E = (E_{0}, \dots, E_{3})$ , $F = (F_{0}, \dots, F_{3})$ at $p$ .

[L1]

A tetrad at $p$ is an ordered basis $(E_{A})$ of $T_{p} M$ with $g_{p} (E_{A}, E_{B}) = η_{A B}$ ; a future-directed tetrad has $E_{0}$ future-directed (Local frame fields, coordinate frames and tetrad fields).

[L2]

A nonzero timelike vector has $g_{p} (v, N_{p}) \neq 0$ , and $C_{p}^{+} = {v : g_{p} (v, v) < 0, g_{p} (v, N_{p}) < 0}$ is the future timelike component (Classification of future and past causal vectors by a timelike field).

[L3]

In an orthonormal ordered basis of a Lorentz vector space, the timelike set splits as $T = T_{+} \cup T_{-}$ with $T_{+} = {v : v^{0} > ∣ v_{v e c} ∣}$ and $T_{-} = {v : v^{0} < - ∣ v_{v e c} ∣}$ the two components, in some order, in every orthonormal basis (The timelike set has exactly two convex components, described in orthonormal coordinates).

[L4]

Every vector of $T_{p} M$ has a unique coordinate list in the ordered basis $E$ (A finite list $v : n \to V$ is an ordered basis if and only if every $x \in V$ equals $\sum_{i < n} λ_{i} v_{i}$ for exactly one $λ : n \to F$ ; those scalars are the coordinates of $x$ in that ordered basis).

[L5]

Orthonormal bases of a Lorentz vector space exist, and the timelike vector $E_{0}$ of a tetrad is future-directed exactly when $g_{p} (E_{0}, N_{p}) < 0$ (Every Lorentz form admits an ordered basis with matrix diag(-1,1,1,1), Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model).

[L6]

A type $(r, s)$ tensor at $p$ is a multilinear map $(T_{p}^{*} M)^{r} \times (T_{p} M)^{s} \to R$ : its first $r$ slots are covectors and its last $s$ slots are vectors; components in a basis are its evaluations on the corresponding dual covectors and basis vectors (Tensor fields of type (r,s) on a Lorentzian four-manifold and their components).

Proof

technique · direct

1.1L1L4given

Since $E$ is a basis, [L4] gives unique coefficients $Λ^{B}_{A}$ with $F_{A} = \sum_{B} Λ^{B}_{A} E_{B}$ , which is the uniqueness assertion.

2.1step 1.1L1algebra

Evaluating $g_{p}$ and using bilinearity together with the tetrad property $g_{p} (E_{C}, E_{D}) = η_{C D}$ gives $η_{A B} = g_{p} (F_{A}, F_{B}) = \sum_{C, D} Λ^{C}_{A} Λ^{D}_{B} g_{p} (E_{C}, E_{D})$ , which is claim 1.

2.2step 1.1L1L2L3L5given

In the orthonormal ordered basis $E$ , [L3] describes the two timelike components as $T_{\pm}$ ; the vector $E_{0}$ has coordinates $(1, 0, 0, 0) \in T_{+}$ , and $E_{0}$ is future-directed by hypothesis, so $C_{p}^{+} = T_{+}$ and a vector is future timelike exactly when its $E$ -coordinates satisfy $v^{0} > ∣ v_{v e c} ∣$ . The vector $F_{0}$ has coordinates $(Λ^{0}_{0}, Λ^{1}_{0}, Λ^{2}_{0}, Λ^{3}_{0})$ by step 1.1 and is future-directed by hypothesis, so $Λ^{0}_{0} > ∣ (Λ^{1}_{0}, Λ^{2}_{0}, Λ^{3}_{0}) ∣ \geq 0$ ; this proves claim 3.

2.3step 1.1L1L6algebra

For a covariant $2$ -tensor $T$ , bilinearity of $T$ at $p$ and $F_{A} = \sum_{C} Λ^{C}_{A} E_{C}$ , $F_{B} = \sum_{D} Λ^{D}_{B} E_{D}$ give $T (F_{A}, F_{B}) = \sum_{C, D} Λ^{C}_{A} Λ^{D}_{B} T (E_{C}, E_{D})$ , the first part of claim 4.

3.1step 2.1L1algebra

Taking determinants in the matrix identity $Λ^{T} η Λ = η$ of claim 1 gives $(\det Λ)^{2} \det η = \det η$ ; since $\det η = - 1 \neq 0$ , we get $(\det Λ)^{2} = 1$ , so $\det Λ = \pm 1$ and $Λ$ is invertible. This proves claim 2.

4.1step 1.1step 3.1L1L6algebra

For the general type $(r, s)$ statement, let $(ε^{A})$ and $(θ^{A})$ be the dual bases of $(E_{A})$ and $(F_{A})$ . From $θ^{A} (F_{B}) = δ^{A}_{B}$ and the expansion of step 1.1 one gets $θ^{A} = \sum_{B} (Λ^{- 1})^{A}_{B} ε^{B}$ , where $Λ^{- 1}$ exists by claim 2; substituting this on each contravariant slot and the expansion of step 1.1 on each covariant slot into the multilinear evaluation gives the stated products of $(Λ^{- 1})^{A}_{B}$ and $Λ^{A}_{B}$ .

The change between two future-directed tetrads is a Lorentz matrix

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources