ExampleConstruction: AI-adaptedVerification: 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.

Reversing the time orientation reverses the future cone

Example

Let $(M, g, N)$ be a time-oriented smooth Lorentzian four-manifold (Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model) and put $N^{'} : = - N$ . Then $(M, g, N^{'})$ is again a time-oriented smooth Lorentzian four-manifold, and at every $p \in M$ the future-directed causal vectors of $N^{'}$ are exactly the past-directed causal vectors of $N$ ; equivalently $C_{p}^{+} (N^{'}) = C_{p}^{-} (N)$ . In the flat model of The constant Minkowski metric as a smooth time-oriented Lorentzian manifold with $N = \partial_{0}$ , the vector $\partial_{0}$ is future-directed for $N$ and past-directed for $- N$ .

Facts & Assumptions

Given: A time-oriented smooth Lorentzian four-manifold $(M, g, N)$ and its reversal $N^{'} = - N$ .

[L1]

A time orientation is a smooth vector field $N$ with $g_{p} (N_{p}, N_{p}) < 0$ at every $p$ ; a nonzero causal $v$ 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).

[L2]

For two smooth timelike fields $N, N^{'}$ the function $f (p) = g_{p} (N_{p}, N_{p}^{'})$ is smooth and nowhere zero, and on each connected set it has constant sign; where $f < 0$ the future cones of $N$ and $N^{'}$ agree, and where $f > 0$ they are opposite, in particular $C_{p}^{+} (N^{'}) = C_{p}^{-} (N)$ (Two time orientations agree or are opposite on each connected set).

[L3]

A nonzero causal vector is future-directed exactly when it lies in $cl (C_{p}^{+}) ∖ {0}$ and past-directed exactly when it lies in $cl (C_{p}^{-}) ∖ {0}$ (Classification of future and past causal vectors by a timelike field, Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model).

[L4]

In the flat model with $N = \partial_{0}$ , the vector $\partial_{0}$ is smooth and $g_{p} (\partial_{0}, \partial_{0}) = - 1 < 0$ (The constant Minkowski metric as a smooth time-oriented Lorentzian manifold, A smooth vector field is a smooth section of the tangent bundle).

Verification

technique · direct

1.1L1given

The field $N^{'} = - N$ has component functions the negatives of those of $N$ in every chart, hence is smooth, and $g_{p} (N_{p}^{'}, N_{p}^{'}) = g_{p} (N_{p}, N_{p}) < 0$ for every $p$ ; by [L1] the triple $(M, g, N^{'})$ is a time-oriented smooth Lorentzian four-manifold.

2.1step 1.1L2algebra

For the pair $(N, N^{'})$ the function of [L2] is $f (p) = g_{p} (N_{p}, - N_{p}) = - g_{p} (N_{p}, N_{p}) > 0$ for every $p$ ; so $f$ is positive on every connected set, and the positive-sign case of [L2] gives $C_{p}^{+} (N^{'}) = C_{p}^{-} (N)$ at every $p$ .

3.1step 2.1L3algebra

By [L3] applied in the two 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$ ; and symmetrically the future-directed causal vectors of $N$ are the past-directed ones of $N^{'}$ .

4.1step 3.1L1L4algebra∎

In the flat model, $N^{'} = - \partial_{0}$ and $g_{p} (\partial_{0}, N^{'}) = - g_{p} (\partial_{0}, \partial_{0}) = 1 > 0$ by [L4], so by [L1] the vector $\partial_{0}$ is past-directed for $N^{'}$ ; it is future-directed for $N$ since $g_{p} (\partial_{0}, N) = - 1 < 0$ . This is the concrete instance of step 3.1, and it shows that the future/past attribution of a fixed causal vector is relative to the adopted time orientation.

Remarks

Choice convention. The smooth vector fields of this example 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 example inherits that assumption and uses no further choice principle.

Reversing the time orientation reverses the future cone

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources