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.

Two time orientations agree or are opposite on each connected set

Statement

Let $(M, g)$ be a smooth Lorentzian four-manifold and let $N, N^{'}$ be two smooth timelike vector fields on $M$ , so that both $(M, g, N)$ and $(M, g, N^{'})$ are time-oriented (Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model). Put $f (p) : = g_{p} (N_{p}, N_{p}^{'})$ for $p \in M$ , and for each $p$ let $C_{p}^{+} (N)$ and $C_{p}^{+} (N^{'})$ be the components of the timelike set of $T_{p} M$ containing $N_{p}$ and $N_{p}^{'}$ . Then:

$f : M \to R$ is $C^{\infty}$ and $f (p) \neq 0$ for every $p \in M$ .
On every nonempty connected subset $C \subseteq M$ the function $f$ has constant sign: either $f < 0$ throughout $C$ or $f > 0$ throughout $C$ .
If $f < 0$ on a nonempty connected subset $C$ , then $C_{p}^{+} (N^{'}) = C_{p}^{+} (N)$ and the future-directed causal vectors of $N^{'}$ agree with those of $N$ at every $p \in C$ ; if $f > 0$ on $C$ , then $C_{p}^{+} (N^{'}) = C_{p}^{-} (N)$ and the future-directed causal vectors of $N^{'}$ are exactly the past-directed causal vectors of $N$ at every $p \in C$ .
In particular $N$ and $- N$ define opposite future cones at every point.

Facts & Assumptions

Given: A smooth Lorentzian four-manifold $(M, g)$ and smooth timelike vector fields $N, N^{'}$ on $M$ .

[L1]

For $(M, g, N)$ and $p \in M$ : $N_{p}^{⊥}$ is positive definite, no nonzero causal $v$ has $g_{p} (v, N_{p}) = 0$ , and $C_{p}^{+} (N) = {v : g_{p} (v, v) < 0, g_{p} (v, N_{p}) < 0}$ , while a nonzero causal $v$ is future-directed exactly when $v \in cl (C_{p}^{+} (N))$ and past-directed exactly when $v \in cl (C_{p}^{-} (N))$ (Classification of future and past causal vectors by a timelike field).

[L2]

The timelike set of a Lorentz vector space has exactly two components, each convex and path-connected; the map $v \mapsto - v$ is a linear isomorphism carrying the timelike set onto itself, and a nonzero timelike $v$ and $- v$ lie in different components, since convexity would otherwise put $0 = \frac{1}{2} v + \frac{1}{2} (- v)$ in a component of the timelike set (The timelike set has exactly two convex components, described in orthonormal coordinates).

[L3]

A time orientation is a smooth vector field $N$ with $g_{p} (N_{p}, N_{p}) < 0$ for all $p$ ; a nonzero causal vector is future-directed when $g_{p} (v, N_{p}) < 0$ and past-directed when $g_{p} (v, N_{p}) > 0$ (Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model).

[L4]

A smooth vector field is a smooth section of $T M$ , and it is smooth exactly when its component functions in a smooth chart are smooth; in particular the component functions in an induced tangent-bundle chart are smooth (A smooth vector field is a smooth section of the tangent bundle, The induced tangent bundle chart, Smoothness of a vector field is equivalent to smooth coordinate components).

[L5]

In every smooth chart the metric components $g_{a b} = g (\partial_{a}, \partial_{b})$ are $C^{\infty}$ functions (Smooth covariant 2-tensor fields on a smooth manifold).

[L6]

A space is connected when it admits no separation, a separation being an ordered pair of open, nonempty, disjoint subsets whose union is the space (Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets).

[L7]

A map is continuous when preimages of open sets are open (Continuity of a map of topological spaces at a point and globally).

Proof

technique · direct

1.1L4L5algebra

In a smooth chart $(U, x)$ , $f (q) = \sum_{a, b} g_{a b} (q) N^{a} (q) N^{' b} (q)$ , where $N^{a}, N^{' b}$ are the component functions of the two fields in the induced tangent-bundle chart. By [L4] each $N^{a}, N^{' b}$ is $C^{\infty}$ on $U$ and by [L5] each $g_{a b}$ is $C^{\infty}$ on $U$ ; finite sums and products of smooth functions are smooth, so $f$ is $C^{\infty}$ on $U$ , and since the smooth charts cover $M$ , $f$ is $C^{\infty}$ on $M$ .

1.2L1L3given

For every $p \in M$ the vector $N_{p}^{'}$ is timelike, hence nonzero and causal, and [L1] applied with the roles of $N$ and $N^{'}$ interchanged gives $f (p) = g_{p} (N_{p}^{'}, N_{p}) \neq 0$ .

2.1step 1.1step 1.2L6L7

Let $C \subseteq M$ be nonempty and connected. By step 1.1 $f$ is $C^{\infty}$ , hence continuous, so $A : = C \cap f^{- 1} ((0, \infty))$ and $B : = C \cap f^{- 1} ((- \infty, 0))$ are open in $C$ by [L7]. They are disjoint, and by step 1.2 their union is $C$ . If both were nonempty, $(A, B)$ would be a separation of $C$ , contradicting connectedness by [L6]; hence one is empty and $f$ has constant sign on $C$ .

2.2step 1.2L1algebra

Suppose $f < 0$ on $C$ and let $p \in C$ . Then $g_{p} (N_{p}^{'}, N_{p}) < 0$ and $N_{p}^{'}$ is timelike, so claim 3 of [L1] gives $N_{p}^{'} \in C_{p}^{+} (N)$ ; symmetrically $g_{p} (N_{p}, N_{p}^{'}) < 0$ and $N_{p}$ timelike give $N_{p} \in C_{p}^{+} (N^{'})$ . Both $C_{p}^{+} (N)$ and $C_{p}^{+} (N^{'})$ are components of the timelike set containing $N_{p}^{'}$ (the first by the previous sentence, the second by definition of $C_{p}^{+} (N^{'})$ ), and components containing a common point coincide; hence $C_{p}^{+} (N^{'}) = C_{p}^{+} (N)$ . By claim 4 of [L1] the future-directed causal vectors of each time orientation are the nonzero points of the closure of its future component, so they agree at $p$ .

3.1step 1.2step 2.1L1L2algebra

Suppose $f > 0$ on $C$ and let $p \in C$ . Then $- N_{p}^{'}$ is timelike with $g_{p} (- N_{p}^{'}, N_{p}) = - f (p) < 0$ , so $- N_{p}^{'} \in C_{p}^{+} (N)$ by claim 3 of [L1]; by [L2] the vectors $N_{p}^{'}$ and $- N_{p}^{'}$ lie in different components of the timelike set, and by [L2] the timelike set has exactly two components, so the component containing $N_{p}^{'}$ is the complement of the component containing $- N_{p}^{'}$ , that is, $C_{p}^{+} (N^{'}) = C_{p}^{-} (N)$ . Applying claim 4 of [L1] in both time orientations, the future-directed causal vectors of $N^{'}$ are $cl (C_{p}^{+} (N^{'})) ∖ {0} = cl (C_{p}^{-} (N)) ∖ {0}$ , which are exactly the past-directed causal vectors of $N$ at $p$ .

4.1step 1.1step 1.2step 2.1step 2.2step 3.1L3∎

Steps 1.1-1.2 prove claim 1, step 2.1 proves claim 2, and steps 2.2 and 3.1 prove claim 3; moreover $g_{p} (N_{p}, - N_{p}) = - g_{p} (N_{p}, N_{p}) > 0$ for every $p$ , so the case $N^{'} = - N$ of step 3.1 gives $C_{p}^{+} (- N) = C_{p}^{-} (N)$ , which is claim 4.

Remarks

Choice convention. The smooth vector fields of this item are the tangent-bundle sections of A smooth vector field is a smooth section of the tangent bundle, whose canonical smooth structure on $T M$ assumes the axiom ${A C}_{ω}$ of The Axiom of Countable Choice ( ${A C}_{ω}$ ); this item inherits that assumption and uses no further choice principle.

Two time orientations agree or are opposite on each connected set

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources