LemmaStatement: 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.

Monotonicity of inertial time and the Lipschitz graph property for causal curves in the flat model

Statement

Assume the Axioms of 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). Let $(M, η, N)$ be the flat model of The flat model: Minkowski space R^4, its standard Lorentz form, inertial charts and cone sets, with its global inertial chart $x = (x^{0}, x^{1}, x^{2}, x^{3})$ , written $x = (x^{0}, z)$ with $z \in R^{3}$ (clauses (a), (b) and (e) of that definition), and let $γ : I \to M$ be a future causal curve in the class of Causal curves, chronological and causal reachability, and inextendibility. Then:

(a) $x^{0} \circ γ : I \to R$ is strictly increasing.

(b) For all $a < b$ in $I$ , $∣ z (γ (b)) - z (γ (a)) ∣ \leq x^{0} (γ (b)) - x^{0} (γ (a)),$ and consequently $γ$ is injective and its image is a $1$ -Lipschitz graph over the interval $(x^{0} \circ γ) (I)$ .

(c) If $γ$ is future-inextendible then $\sup (x^{0} \circ γ) (I) = + \infty$ ; if $γ$ is past-inextendible then $\inf (x^{0} \circ γ) (I) = - \infty$ . Hence if $γ$ is inextendible then $x^{0} \circ γ$ is a strictly increasing surjection onto $R$ , and for every $c \in R$ the parameter set ${t \in I : x^{0} (γ (t)) = c}$ is a singleton.

(d) The coordinate function $u : = x^{0}$ is a temporal function of the flat model in the sense of Chronology, causality, strong causality, global hyperbolicity and time functions clause (e): its gradient is the vector field $\nabla u = - \partial_{0}$ on all of $M$ , with $η (\nabla u, \nabla u) = - 1 < 0$ and $d u (\partial_{0}) = 1 > 0$ everywhere.

Facts & Assumptions

Given: Countable Choice, Dependent Choice, the flat model of The flat model: Minkowski space R^4, its standard Lorentz form, inertial charts and cone sets, its global inertial chart $x = (x^{0}, z)$ , a future causal curve $γ : I \to M$ and real numbers $a < b$ in $I$ .

[L1]

At almost every $t \in I$ the velocity $γ^{'} (t)$ exists and is nonzero future causal; the coordinate path $t \mapsto x (γ (t))$ of the global inertial chart $x$ is locally absolutely continuous, with coordinate derivative equal to the coordinates of $γ^{'} (t)$ at almost every $t$ (Causal curves, chronological and causal reachability, and inextendibility clause (b), Chart independence, concatenation, reparametrization and transitivity for causal curves clauses (b) and (c)).

[L2]

Cone criterion for the flat model in the coordinates of the inertial chart $x$ : a nonzero vector $v \in T_{p} M$ is future causal exactly when $v^{0} \geq ∣ v_{s} ∣$ , future timelike exactly when $v^{0} > ∣ v_{s} ∣$ , and every nonzero future causal $v$ has $v^{0} > 0$ (The causal cones of the flat model in inertial coordinates, and closure of the future cone under sums clauses (a) and (b), The flat model: Minkowski space R^4, its standard Lorentz form, inertial charts and cone sets clause (f), Time orientation, future and past timelike/null/causal vectors, and the closed cones, Timelike, null, spacelike and causal vectors of a Lorentz vector space).

[L3]

Fundamental theorem of calculus for absolutely continuous functions, with its countable and dependent choice assumptions: for an absolutely continuous $F$ on $[a, b]$ , $F^{'}$ exists almost everywhere, $F^{'} \in L^{1}$ , and $F (b) - F (a) = \int_{a}^{b} F^{'}$ (Fundamental theorem of calculus for absolutely continuous functions, Absolute continuity on a compact interval).

[L4]

A nonnegative function with vanishing integral is zero almost everywhere (A nonnegative measurable function has integral $0$ exactly when it vanishes almost everywhere). For componentwise Lebesgue-integrable $w : [a, b] \to R^{3}$ and integrable $f$ with $f \geq ∣ w ∣_{e}$ almost everywhere, $∣ \int_{a}^{b} w ∣_{e} \leq \int_{a}^{b} f$ . To prove this, put $v : = \int_{a}^{b} w$ , componentwise. If $v \neq 0$ , put $e : = v / ∣ v ∣_{e}$ ; the inequality $e \cdot w \leq ∣ w ∣_{e}$ follows from $∣ w - (e \cdot w) e ∣_{e}^{2} = ∣ w ∣_{e}^{2} - (e \cdot w)^{2} \geq 0$ . The integrable function $f - e \cdot w$ is nonnegative after modification on a null set, so its integral is nonnegative; linearity gives $\int f \geq e \cdot v = ∣ v ∣_{e}$ . If $v = 0$ , use $f \geq 0$ . These are Lebesgue statements, using The Lebesgue integral is linear on $L^{1} (μ)$ , Integrable real and complex functions, and their integrals, Monotonicity and nonnegative homogeneity of the nonnegative integral and Two integrable functions are equal almost everywhere exactly when all of their indefinite integrals agree.

[L5]

Future-inextendibility means absence of a point limit at the upper parameter end, whether finite or infinite; the dual holds at the lower end (Causal curves, chronological and causal reachability, and inextendibility clause (d)). This no-limit definition is sufficient below; no parameter-preserving extension at an infinite end is asserted.

Proof

technique · direct

1.1givenL1L2algebra

(Almost-everywhere cone inequality.) Write $c (t) : = x (γ (t)) = (c^{0} (t), c_{s} (t))$ . By [L1], $c$ is locally absolutely continuous and at almost every $t$ its derivative $c^{'} (t)$ exists and equals the coordinates of the nonzero future causal velocity, so by [L2] $c^{0}^{'} (t) \geq ∣ c_{s}^{'} (t) ∣_{e}$ and $c^{0}^{'} (t) > 0$ . This proves nothing yet but fixes the a.e. information used below.

2.1step 1.1L3L4algebra

(Monotonicity and the Lipschitz bound.) Let $a < b$ in $I$ . By [L3] applied to the absolutely continuous functions $c^{0}$ and the components of $c_{s}$ on $[a, b]$ , and by [L4], $c^{0} (b) - c^{0} (a) = \int_{a}^{b} c^{0}^{'} (t) d t \geq {∣ \int_{a}^{b} c_{s}^{'} (t) d t ∣}_{e} = ∣ c_{s} (b) - c_{s} (a) ∣_{e} \geq 0.$ This is (b). If $c^{0} (b) = c^{0} (a)$ , then $\int_{a}^{b} c^{0}^{'} = 0$ with $c^{0}^{'} \geq 0$ almost everywhere, so [L4] gives $c^{0}^{'} = 0$ almost everywhere on $[a, b]$ , contradicting $c^{0}^{'} > 0$ on the full-measure set of step 1.1; hence $c^{0} (b) > c^{0} (a)$ , which is the strict monotonicity of (a). Moreover $c (a) = c (b)$ would give $c_{s} (a) = c_{s} (b)$ by the displayed inequality, hence $γ (a) = γ (b)$ , and strict increase of $c^{0}$ forbids $a < b$ ; so $γ$ is injective, and its spatial coordinates are $1$ -Lipschitz in $c^{0}$ again by the displayed inequality.

3.1step 2.1L5algebra

(Unboundedness at inextendible ends.) Suppose $γ$ is future-inextendible and let $T : = \sup (x^{0} \circ γ) (I)$ . If $T < + \infty$ , then for $t, t^{'} \to \sup I$ the spatial coordinates satisfy $∣ c_{s} (t) - c_{s} (t^{'}) ∣_{e} \leq ∣ c^{0} (t) - c^{0} (t^{'}) ∣ \to 0$ by step 2.1, so $(c^{0}, c_{s})$ has a limit $q = (T, z_{\infty}) \in R^{4}$ ; that is, $γ$ converges to the event with coordinates $q$ as $t \to \sup I$ . This point limit directly contradicts the no-limit definition of future-inextendibility [L5]. Hence $T = + \infty$ ; the past statement is the time reverse. With both statements, an inextendible $γ$ has range all of $R$ , and step 2.1 makes $x^{0} \circ γ$ a strictly increasing surjection onto $R$ , so each level set is attained at exactly one parameter. This proves (c).

4.1step 2.1step 3.1givenalgebra∎

(The time coordinate is temporal, and conclusion.) In the coordinates of the global inertial chart, $η = diag (- 1, 1, 1, 1)$ , and the vector field $w : = - \partial_{0}$ satisfies $η (w, \partial_{0}) = 1$ and $η (w, \partial_{i}) = 0$ for $i = 1, 2, 3$ ; hence $η (w, X) = X^{0} = d u (X)$ for every vector $X$ , so $w$ is the gradient $\nabla u$ of $u = x^{0}$ . It satisfies $η (w, w) = - 1 < 0$ and $d u (\partial_{0}) = 1 > 0$ , so $u$ is a temporal function as claimed in (d). With steps 2.1 and 3.1 this completes the proof.

Remarks

Coordinate and chart dependence. The coordinate $x^{0}$ depends on the choice of inertial chart, and the monotonicity statement is for the one global inertial chart $x$ ; the cone criterion used holds in every inertial chart (The causal cones of the flat model in inertial coordinates, and closure of the future cone under sums), and no claim is made here about how different inertial charts are related. The physical reading of $x^{0}$ as a time coordinate requires the framework postulates and is not part of this lemma.
Sharpness. The Lipschitz bound is the cone bound integrated; it is attained by null straight paths, for which the inequality is an equality on every subinterval.

Monotonicity of inertial time and the Lipschitz graph property for causal curves in the flat model

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources