TheoremStatement: AI-adaptedProof: AI-adaptedprecheck 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.

Existence of a smooth future-directed tetrad field near every event

Statement

Let $(M, g, N)$ be a time-oriented smooth Lorentzian four-manifold and let $p \in M$ (Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model). Then there is an open neighborhood $U \subseteq M$ of $p$ and a smooth future-directed tetrad field $(E_{0}, E_{1}, E_{2}, E_{3})$ on $U$ (Local frame fields, coordinate frames and tetrad fields), i.e. $g_{q} (E_{A} (q), E_{B} (q)) = diag (- 1, 1, 1, 1)_{A B}$ for all $q \in U$ with $E_{0} (q)$ future-directed for every $q \in U$ .

Facts & Assumptions

Given: A time-oriented smooth Lorentzian four-manifold $(M, g, N)$ and a point $p \in M$ .

[L1]

A tetrad field on an open set is a tuple of four smooth vector fields that is pointwise a $g$ -orthonormal ordered basis, and it is future-directed when its first member is future-directed at every point (Local frame fields, coordinate frames and tetrad fields).

[L2]

There is an ordered $g_{p}$ -orthonormal basis of $T_{p} M$ (Every Lorentz form admits an ordered basis with matrix diag(-1,1,1,1)).

[L3]

For a nonzero timelike $v \in T_{p} M$ one 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, Timelike, null, spacelike and causal vectors of a Lorentz vector space).

[L4]

The component functions $g_{a b} (q) = g_{q} (\partial_{a} ∣_{q}, \partial_{b} ∣_{q})$ of $g$ in a smooth chart are $C^{\infty}$ (Smooth covariant 2-tensor fields on a smooth manifold).

[L5]

The coordinate derivations $\partial_{a} ∣_{q}$ of a chart form a basis of $T_{q} M$ , and every vector of $T_{q} M$ has a unique coordinate list (Coordinate derivations form a basis of the tangent space, 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).

[L6]

A vector field on a chart domain is smooth exactly when its coordinate component functions are smooth (Smoothness of a vector field is equivalent to smooth coordinate components).

[L7]

A smooth map between smooth manifolds is continuous ( $C^{r}$ and smooth maps between smooth manifolds).

[L8]

If $f : X \to R$ is continuous at $x$ and $f (x) > 0$ , then there is an open neighborhood $W$ of $x$ with $f > 0$ on $W$ ; the same holds with $>$ replaced by $<$ . (Continuity of a map of topological spaces at a point and globally)

[L9]

Finite sums, products and composites of $C^{\infty}$ maps on Euclidean domains are $C^{\infty}$ ( $C^{k}$ Euclidean maps are closed under componentwise algebra and composition).

[L10]

On $(0, \infty)$ the squaring map $u \mapsto u^{2}$ has derivative $2 u$ , and for powers and quotients the product and quotient rules hold (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$ ).

[L11]

If $U \subseteq R^{n}$ is open and $f : U \to R^{n}$ is injective, $C^{k}$ with $k \geq 1$ , and $D f$ is invertible everywhere, then $f [U]$ is open and $f : U \to f [U]$ is a $C^{k}$ diffeomorphism (An injective regular $C^{k}$ map is a $C^{k}$ diffeomorphism onto its image).

[L12]

The smooth structure of the tangent bundle used for smooth vector fields assumes the axiom ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

technique · direct, by an explicit construction with successive shrinking of neighborhoods

1.1L2L3L5L6L12given

Choose a smooth chart $(U_{0}, x)$ around $p$ . By [L2] there is an ordered $g_{p}$ -orthonormal basis $(b_{0}, b_{1}, b_{2}, b_{3})$ of $T_{p} M$ ; by [L3], $g_{p} (b_{0}, N_{p}) \neq 0$ , so after replacing $b_{0}$ by $- b_{0}$ if necessary we may assume $b_{0}$ is future-directed, still an orthonormal basis. Expand each $b_{A}$ uniquely in the coordinate basis, $b_{A} = \sum_{a} b_{A}^{a} \partial_{a} ∣_{p}$ [L5], and define $B_{A} : = \sum_{a} b_{A}^{a} \partial_{a}$ on $U_{0}$ , with the constants $b_{A}^{a}$ as coefficients. Each $B_{A}$ is a smooth vector field by [L6] (so that the tangent-bundle smooth structure of [L12] is in force), and $B_{A} (p) = b_{A}$ .

2.1step 1.1L4L9given

Consider the smooth functions $G_{A B} (q) : = g_{q} (B_{A} (q), B_{B} (q))$ and $h (q) : = g_{q} (B_{0} (q), N_{q})$ on $U_{0}$ . They are smooth because in the chart $x$ they equal the finite sums $G_{A B} = \sum_{a, b} b_{A}^{a} b_{B}^{b} g_{a b}$ and $h = \sum_{a, b} b_{0}^{a} N^{b} g_{a b}$ of products of smooth functions, using [L4] and [L9]; and $G_{A B} (p) = η_{A B}$ , while $h (p) < 0$ by step 1.1 and the definition of future-directedness.

3.1step 2.1L7L8

By [L7] and [L8] applied to the continuous functions $- G_{00}$ (positive at $p$ ) and $- h$ (positive at $p$ ), there is an open neighborhood $U_{1} \subseteq U_{0}$ of $p$ on which $G_{00} < 0$ and $h < 0$ .

4.1step 3.1L1L3L9L10L11

Define $F_{0} : = B_{0} / \sqrt{- G_{00}}$ on $U_{1}$ . The function $u \mapsto u^{- 1 / 2}$ is $C^{\infty}$ on $(0, \infty)$ : the map $u \mapsto u^{1 / 2}$ is the inverse of the injective $C^{\infty}$ squaring map $u \mapsto u^{2}$ on $(0, \infty)$ whose derivative $2 u$ is invertible everywhere there, so it is $C^{\infty}$ by [L11], and $u \mapsto u^{- 1}$ has derivatives $(- 1)^{n} n! u^{- n - 1}$ for every $n$ by iterating the product and quotient rules of [L10]; composites and products of $C^{\infty}$ maps are $C^{\infty}$ by [L9]. Hence $F_{0}$ is smooth on $U_{1}$ , and $g_{q} (F_{0} (q), F_{0} (q)) = G_{00} (q) / (- G_{00} (q)) = - 1$ ; since $- G_{00} > 0$ , the field $F_{0}$ is a positive multiple of $B_{0}$ at every point, so $g_{q} (F_{0} (q), N_{q}) = h (q) / \sqrt{- G_{00} (q)} < 0$ and $F_{0} (q)$ is future-directed.

5.1step 4.1L4L7L8L9algebra

For $i = 1, 2, 3$ define $P_{i} : = B_{i} + g_{q} (B_{i}, F_{0}) F_{0}$ on $U_{1}$ ; these are smooth fields by [L9], and $g_{q} (P_{i}, F_{0}) = g_{q} (B_{i}, F_{0}) + g_{q} (B_{i}, F_{0}) (- 1) = 0$ , so $P_{i} (q)$ lies in the $g_{q}$ -orthogonal complement of $F_{0} (q)$ . The function $φ_{1} : = g_{q} (P_{1}, P_{1})$ is smooth by [L4] and [L9], and $φ_{1} (p) = g_{p} (b_{1}, b_{1}) = 1 > 0$ because $F_{0} (p) = b_{0}$ and $g_{p} (b_{1}, b_{0}) = 0$ . By [L7] and [L8] there is an open $U_{2} \subseteq U_{1}$ containing $p$ with $φ_{1} > 0$ on $U_{2}$ . Define $F_{1} : = P_{1} / \sqrt{φ_{1}}$ on $U_{2}$ ; it is smooth by the argument of step 4.1, $g (F_{1}, F_{1}) = 1$ , and $g (F_{1}, F_{0}) = 0$ .

6.1step 5.1L4L7L8L9algebra

Define $P_{2}^{'} : = P_{2} - g (P_{2}, F_{1}) F_{1}$ on $U_{2}$ , a smooth field with $g (P_{2}^{'}, F_{1}) = g (P_{2}, F_{1}) - g (P_{2}, F_{1}) = 0$ and $g (P_{2}^{'}, F_{0}) = 0$ , and let $φ_{2} : = g (P_{2}^{'}, P_{2}^{'})$ , smooth with $φ_{2} (p) = g_{p} (b_{2}, b_{2}) = 1 > 0$ because $F_{1} (p) = b_{1}$ and $g_{p} (b_{2}, b_{1}) = 0$ . Shrink to an open $U_{3} \subseteq U_{2}$ containing $p$ with $φ_{2} > 0$ and define $F_{2} : = P_{2}^{'} / \sqrt{φ_{2}}$ ; then $F_{2}$ is smooth, $g (F_{2}, F_{2}) = 1$ and $g (F_{2}, F_{0}) = g (F_{2}, F_{1}) = 0$ .

7.1step 6.1L4L7L8L9algebra

Define $P_{3}^{'} : = P_{3} - g (P_{3}, F_{1}) F_{1} - g (P_{3}, F_{2}) F_{2}$ on $U_{3}$ , smooth with $g (P_{3}^{'}, F_{1}) = g (P_{3}^{'}, F_{2}) = g (P_{3}^{'}, F_{0}) = 0$ , and let $φ_{3} : = g (P_{3}^{'}, P_{3}^{'})$ , smooth with $φ_{3} (p) = g_{p} (b_{3}, b_{3}) = 1 > 0$ . Shrink to an open $U_{4} \subseteq U_{3}$ containing $p$ with $φ_{3} > 0$ and define $F_{3} : = P_{3}^{'} / \sqrt{φ_{3}}$ ; then $F_{3}$ is smooth, $g (F_{3}, F_{3}) = 1$ and $g (F_{3}, F_{A}) = 0$ for $A = 0, 1, 2$ .

8.1step 4.1step 5.1step 6.1step 7.1L1algebra

On $U_{4}$ the four smooth fields $F_{0}, F_{1}, F_{2}, F_{3}$ satisfy $g (F_{A}, F_{B}) = η_{A B}$ by steps 4.1-5.1, and $F_{0}$ is future-directed by step 4.1. The Gram matrix $η$ is invertible, so a linear relation $\sum_{A} λ^{A} F_{A} (q) = 0$ implies $\sum_{A} λ^{A} η_{A B} = 0$ for all $B$ after pairing with $F_{B} (q)$ , hence $λ = 0$ ; thus the tuple is pointwise an ordered basis, a future-directed tetrad field on $U_{4}$ by [L1].

9.1step 8.1∎

The open neighborhood $U_{4}$ of $p$ and the field $(F_{0}, F_{1}, F_{2}, F_{3})$ have the asserted properties; this proves the theorem.

Remarks

Choice convention. The construction uses smooth vector fields, hence tangent-bundle sections, whose canonical smooth structure assumes the axiom ${A C}_{ω}$ of The Axiom of Countable Choice ( ${A C}_{ω}$ ) as recorded in [L12]; no further choice principle is used, and the construction selects a definite basis at $p$ by an explicit finite procedure.

Existence of a smooth future-directed tetrad field near every event

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources