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.

Worked Minkowski slice: Cauchy level sets, causal double cones and the compact diamond

Example

Assume Countable Choice and Dependent Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ ), The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain) for the general absolutely continuous causal-curve conclusions used here.

Let $(A, η, N)$ be the flat model of The flat model: Minkowski space R^4, its standard Lorentz form, inertial charts and cone sets, written $A = R^{4}$ , with its global inertial chart $x = (x^{0}, z) = (t, z)$ , and write $e_{0} : = (1, 0, 0, 0) \in A$ . This example works through the explicit computations behind The flat model is globally hyperbolic and its inertial level sets are Cauchy hypersurfaces.

(i) For every $c \in R$ the level set $Σ_{c} : = x^{- 1} ({c} \times R^{3})$ is a spacelike embedded hypersurface with induced metric $δ = diag (1, 1, 1)$ in the coordinates $(z^{1}, z^{2}, z^{3})$ and future unit normal $\partial_{0}$ (Spacelike hypersurfaces, acausal sets, Cauchy sets, domains of dependence and Cauchy horizons clause (a)).

(ii) The coordinate $t = x^{0}$ is a temporal function: its gradient in the chart is $\nabla t = - \partial_{0}$ , with $η (\nabla t, \nabla t) = - 1 < 0$ and $d t (\partial_{0}) = 1 > 0$ (Chronology, causality, strong causality, global hyperbolicity and time functions clause (e), Monotonicity of inertial time and the Lipschitz graph property for causal curves in the flat model clause (d)).

(iii) For $ε > 0$ and $p \in A$ the double cone $V_{ε} (p) : = I^{+} (p - ε e_{0}) \cap I^{-} (p + ε e_{0})$ is open, contains $p$ , and is causally convex for causal curves that meet it twice: if a future causal curve $γ : [a, b] \to A$ has $γ (a), γ (b) \in V_{ε} (p)$ , then $γ (s) \in V_{ε} (p)$ for every $s \in (a, b)$ . In coordinates, $V_{ε} (p) = {q : ∣ z (q) - z (p) ∣_{e} < ε - ∣ x^{0} (q) - x^{0} (p) ∣} .$

(iv) For $o : = 0 \in A$ and $q : = T e_{0}$ , $T > 0$ , the causal diamond is $J^{+} (o) \cap J^{-} (T e_{0}) = {r : ∣ z (r) ∣_{e} \leq x^{0} (r) \leq T - ∣ z (r) ∣_{e}},$ a closed bounded subset of $R^{4}$ , hence compact; its $t$ -sections are closed balls of radius $\min (t, T - t)$ for $0 \leq t \leq T$ , and are empty otherwise.

(v) The domain of dependence of each $Σ_{c}$ is all of $A$ : $D^{+} (Σ_{c}) \supseteq {t \geq c}$ , $D^{-} (Σ_{c}) \supseteq {t \leq c}$ and $D (Σ_{c}) = A$ (Spacelike hypersurfaces, acausal sets, Cauchy sets, domains of dependence and Cauchy horizons clause (d)).

Facts & Assumptions

Given: The flat model $(A, η, N)$ of The flat model: Minkowski space R^4, its standard Lorentz form, inertial charts and cone sets, its global inertial chart, and the sets and curves of the claims.

[L1]

In the global inertial chart $x$ , $η = diag (- 1, 1, 1, 1)$ , the cone sets of clause (f) are $C^{+} = {v : v^{0} > ∣ v_{s} ∣_{e}}$ and $\overline{C^{+}} = {v : v^{0} \geq ∣ v_{s} ∣_{e}}$ , and $q - p \in \overline{C^{+}}$ exactly when $q \in J^{+} (p)$ , $q - p \in C^{+}$ exactly when $q \in I^{+} (p)$ (The flat model: Minkowski space R^4, its standard Lorentz form, inertial charts and cone sets clauses (a), (b), (f), The flat model is globally hyperbolic and its inertial level sets are Cauchy hypersurfaces clause (a), Time orientation, future and past timelike/null/causal vectors, and the closed cones).

[L2]

Along every future causal curve the coordinate $t$ is strictly increasing and $∣ z (b) - z (a) ∣_{e} \leq t (b) - t (a)$ for $a < b$ ; every inextendible causal curve has $t$ -range all of $R$ and meets each level $t = c$ exactly once (Monotonicity of inertial time and the Lipschitz graph property for causal curves in the flat model clauses (a), (b), (c), The flat model is globally hyperbolic and its inertial level sets are Cauchy hypersurfaces clause (b)).

[L3]

Cone additivity: $C^{+} + \overline{C^{+}} \subseteq C^{+}$ and $\overline{C^{+}} + \overline{C^{+}} \subseteq \overline{C^{+}}$ (The causal cones of the flat model in inertial coordinates, and closure of the future cone under sums clause (c)).

[L4]

The hyperplanes ${t = c}$ are embedded submanifolds with slice chart $x$ , and the restriction of $η$ to $span (\partial_{1}, \partial_{2}, \partial_{3})$ is $diag (1, 1, 1)$ (Embedded submanifolds and slice charts, The flat model: Minkowski space R^4, its standard Lorentz form, inertial charts and cone sets clauses (a), (b)).

[L5]

A subset of $R^{4}$ that is closed and bounded is compact (A subset of $R^{n}$ with the product topology is compact exactly when it is closed and bounded, the product topology being the Euclidean metric topology, Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).

[L7]

The domain of dependence of $S \subseteq A$ consists of the points through which every past-inextendible (respectively future-inextendible) causal curve meets $S$ (Spacelike hypersurfaces, acausal sets, Cauchy sets, domains of dependence and Cauchy horizons clause (d)).

[L8]

Euclidean space $R^{3}$ is complete: every Cauchy sequence in its Euclidean norm converges to a point of $R^{3}$ ( $R$ and $R^{n}$ for $n \geq 1$ with the Euclidean metric are complete, componentwise from the Cauchy criterion in $R$ ).

Verification

technique · direct

1.1givenL4

(The level sets.) By [L4] each $Σ_{c}$ is an embedded three-dimensional submanifold with tangent space $span (\partial_{1}, \partial_{2}, \partial_{3})$ on which $η$ restricts to $diag (1, 1, 1) > 0$ ; hence $Σ_{c}$ is a spacelike embedded hypersurface. Its normal line is spanned by $\partial_{0}$ with $η (\partial_{0}, \partial_{0}) = - 1$ , and $g (\partial_{0}, N) = g (\partial_{0}, \partial_{0}) = - 1 < 0$ with $N = \partial_{0}$ , so $\partial_{0}$ is the future unit normal. This proves (i).

1.2givenL1L4

(The coordinate is temporal.) The function $t = x^{0}$ has differential $d t$ with $d t (\partial_{0}) = 1$ and $d t (\partial_{a}) = 0$ for $a = 1, 2, 3$ ; the vector field $w : = - \partial_{0}$ satisfies $η (w, X) = d t (X)$ for every $X$ because $η (- \partial_{0}, \partial_{0}) = η (\partial_{0}, \partial_{0}) (- 1) = 1$ and $η (- \partial_{0}, \partial_{a}) = 0$ ; hence $\nabla t = w$ with $η (\nabla t, \nabla t) = - 1 < 0$ and $d t (\partial_{0}) = 1 > 0$ . This is (ii).

2.1step 1.2givenL1L2L3

(The double cone is causally convex.) Let $p \in A$ , $ε > 0$ , let $γ : [a, b] \to A$ be future causal with $γ (a), γ (b) \in V_{ε} (p)$ and let $a < s < b$ . Since $γ (a) \in I^{+} (p - ε e_{0})$ , [L1] gives $γ (a) - (p - ε e_{0}) \in C^{+}$ ; since $γ ∣_{[a, s]}$ is future causal, [L1] gives $γ (s) - γ (a) \in \overline{C^{+}}$ ; by [L3], $γ (s) - (p - ε e_{0}) \in C^{+}$ , so $p - ε e_{0} ≪ γ (s)$ . Similarly $γ (b) \in I^{-} (p + ε e_{0})$ gives $(p + ε e_{0}) - γ (b) \in C^{+}$ ; since $γ ∣_{[s, b]}$ is future causal, $γ (b) - γ (s) \in \overline{C^{+}}$ and [L3] gives $(p + ε e_{0}) - γ (s) \in C^{+}$ , so $γ (s) ≪ p + ε e_{0}$ . Hence $γ (s) \in V_{ε} (p)$ , which is causally convex. The displayed coordinate description follows from [L1]: $q \in V_{ε} (p)$ iff $(x^{0} (q) - x^{0} (p) + ε, z (q) - z (p)) \in C^{+}$ and $(x^{0} (p) + ε - x^{0} (q), z (p) - z (q)) \in C^{+}$ , i.e. $∣ z (q) - z (p) ∣_{e} < ε + x^{0} (q) - x^{0} (p)$ and $∣ z (q) - z (p) ∣_{e} < ε - x^{0} (q) + x^{0} (p)$ , which is the stated inequality. This proves (iii).

2.2step 1.2givenL1L5

(The diamond is compact.) Let $r \in A$ with coordinates $(t_{r}, z_{r})$ . By [L1], $r \in J^{+} (o)$ means $t_{r} \geq ∣ z_{r} ∣_{e}$ and $r \in J^{-} (T e_{0})$ means $T - t_{r} \geq ∣ z_{r} ∣_{e}$ ; this is the displayed description. The set described is closed (non-strict inequalities of continuous functions) and bounded: $t_{r} \in [0, T]$ and $∣ z_{r} ∣_{e} \leq \min (t_{r}, T - t_{r}) \leq T / 2$ . By [L5] it is compact, and its $t$ -section is the closed ball of radius $\min (t, T - t)$ in $R^{3}$ . This proves (iv).

2.3step 1.1givenL2L7L8

(The domain of dependence is everything.) Let $p \in A$ with $t (p) \geq c$ , and let $γ : I \to A$ be any past-inextendible causal curve through $p$ . I claim $\inf (t \circ γ) (I) = - \infty$ . Otherwise put $m : = \inf (t \circ γ) (I) > - \infty$ . Since $t \circ γ$ is increasing, it tends to $m$ as the parameter tends to $\inf I$ . For every $ε > 0$ choose a parameter $a \in I$ with $m \leq t (γ (a)) < m + ε$ . For any $u, v \in I$ with $u, v \leq a$ , the Lipschitz bound [L2] gives $∣ z (γ (u)) - z (γ (v)) ∣_{e} \leq ∣ t (γ (u)) - t (γ (v)) ∣ < ε$ . Thus the full spatial tail is Cauchy as the parameter tends to $\inf I$ ; by completeness [L8] it converges to some $z_{\infty} \in R^{3}$ . Since $t (γ (\cdot)) \to m$ , the full curve tail converges to $x^{- 1} (m, z_{\infty}) \in A$ , contradicting past-inextendibility by clause (d) of Causal curves, chronological and causal reachability, and inextendibility. Hence its time range is unbounded below. Since $t \circ γ$ is continuous and strictly increasing on the interval $I$ and attains $t (p) \geq c$ at the parameter of $p$ , its image contains $(- \infty, t (p)]$ , in particular $c$ ; so some parameter lies on $Σ_{c}$ and $p \in D^{+} (Σ_{c})$ . The case $t (p) \leq c$ is the time reverse: every future-inextendible causal curve through $p$ has time range unbounded above and hence meets $Σ_{c}$ , so $p \in D^{-} (Σ_{c})$ . Therefore $D^{+} (Σ_{c}) \cup D^{-} (Σ_{c}) = A$ , which is (v).

3.1step 1.1step 1.2step 2.1step 2.2step 2.3∎

(Conclusion.) Parts (i)-(v) are steps 1.1, 1.2, 2.1, 2.2 and 2.3; this completes the example.

Remarks

Reparametrization of the proof. The computations above are exactly the content of the general theorem for this model; they are recorded separately because the concrete inequalities are used by the flat cylinder and slab examples.
The double cone. The set $V_{ε} (p)$ has two vertex tips at $p \pm ε e_{0}$ and is the standard causally convex neighborhood of strong causality; it is not an open coordinate ball.

Worked Minkowski slice: Cauchy level sets, causal double cones and the compact diamond

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources