LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-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.

Improper integrability and endpoint increments of weak piecewise future causal curves

Statement

Let $x : [a, b] \to A$ , $a < b$ , be a piecewise $C^{1}$ curve in the sense of Curves, regular causal curves and future timelike worldlines in affine Minkowski space, with a finite partition $a = s_{0} < \dots < s_{m} = b$ , $C^{1}$ on each open piece and finite one-sided difference-quotient derivatives at both ends of each piece. Assume its tangents are nonzero future causal at every open-piece point and at each one-sided endpoint.

In any inertial chart (Inertial frames and inertial charts of the affine Minkowski model) write $y = (y^{0}, z)$ , $z \in R^{3}$ , for the coordinate path. On a piece $(α, β)$ , choose $r \in (α, β)$ ; for a function $g$ continuous there, write

$\int_{(α, β)} g : = \lim_{u ↓ α} \int_{u}^{r} g + \lim_{v ↑ β} \int_{r}^{v} g$

when both limits are finite. Then:

(a) $y$ is continuous on $[α, β]$ , $y^{0^{'}} \geq ∣ z^{'} ∣ \geq 0$ on $(α, β)$ , and $y^{0^{'}} > 0$ there.

(b) Every coordinate derivative is absolutely improperly Riemann integrable (its absolute value has finite improper integral), and its signed improper integral equals the corresponding endpoint increment. The continuous functions $∣ z^{'} ∣$ and $f = \sqrt{(y^{0^{'}})^{2} - ∣ z^{'} ∣^{2}} = \sqrt{- η (x^{'}, x^{'})}$ have finite nonnegative improper integrals, with $\int_{(α, β)} f \leq \int_{(α, β)} y^{0^{'}} = y^{0} (β) - y^{0} (α)$ .

(c) The improper values are independent of $r$ , additive under subdivision, and the finite piece sums are independent of the admissible partition.

(d) $D = x (b) - x (a)$ is nonzero future causal: $D^{0} > 0$ and $∣ D_{s p a t i a l} ∣ \leq D^{0}$ in every inertial chart. If some interior or one-sided endpoint tangent is future timelike, then $D$ is future timelike. Coordinate time is strictly increasing on every nondegenerate subinterval. The integrals need not be ordinary closed-piece Riemann integrals. No derivative-limit hypothesis, Lebesgue-integration premise, clock identification, or choice principle is used.

Facts & Assumptions

Given: Reals $a < b$ ; a piecewise $C^{1}$ curve $x : [a, b] \to A$ with partition $a = s_{0} < \dots < s_{m} = b$ , $C^{1}$ on each open piece, finite one-sided difference-quotient derivatives at both ends of every piece, and nonzero future causal tangents at every open-piece point and at each one-sided endpoint; an inertial frame with chart $x_{A}$ and coordinate path $y = (y^{0}, z)$ ; a piece $(α, β)$ of the partition and a point $r \in (α, β)$ .

[L1]

Weak piecewise regularity and corner continuity (Curves, regular causal curves and future timelike worldlines in affine Minkowski space): $x$ is $C^{1}$ on each open piece, so $y$ is $C^{1}$ there and each coordinate $y^{j}$ is differentiable with $y^{j^{'}}$ the corresponding coordinate derivative; the finite one-sided difference-quotient derivatives at the piece endpoints exist, and their finiteness implies continuity of $x$ , hence of $y$ , at every corner and at $a$ and $b$ ; derivatives of a function differentiable on an interval are continuous there when the function is $C^{1}$ (A function differentiable at $c$ is continuous at $c$ ).

[L2]

Metric in an inertial chart (Inertial frames and inertial charts of the affine Minkowski model, The Euclidean spatial structure and cross product of an inertial frame, Lorentz forms of inertia (3,1,0) on a 4-dimensional real vector space): in the chart of an inertial frame the matrix of $η$ in the basis $(e_{0}, \dots, e_{3})$ is $diag (- 1, 1, 1, 1)$ , the spatial form $δ$ is the restriction of $η$ to $span (e_{1}, e_{2}, e_{3})$ with spatial coordinate identification $J : R^{3} \to S$ , $J (z) : = z^{1} e_{1} + z^{2} e_{2} + z^{3} e_{3}$ (the three entries of $z$ are labelled $z^{1}, z^{2}, z^{3}$ ), and coordinate norm $∣ z ∣ : = \sqrt{δ (J (z), J (z))} = ∥ z ∥_{2}$ , and for a tangent vector $v = x^{'} (u)$ with coordinates $y^{'} (u) = (y^{0^{'}} (u), z^{'} (u))$ , $- η (v, v) = (y^{0^{'}} (u))^{2} - ∣ z^{'} (u) ∣^{2}$ ; $η$ is bilinear (Lorentz forms of inertia (3,1,0) on a 4-dimensional real vector space).

[L3]

The future cone in orthonormal coordinates (The timelike set has exactly two convex components, described in orthonormal coordinates, Timelike, null, spacelike and causal vectors of a Lorentz vector space, Time orientation, future and past timelike/null/causal vectors, and the closed cones): with the first basis vector future, the future timelike set is $T_{+} = {v : v^{0} > ∣ v_{s p} ∣}$ , its closure is $cl (T_{+}) = {v : v^{0} \geq ∣ v_{s p} ∣}$ , and $T_{+}$ is open in $V$ ; a nonzero future causal vector $v$ satisfies $v^{0} \geq ∣ v_{s p} ∣$ and $v^{0} > 0$ ; a future timelike vector has $v^{0} > ∣ v_{s p} ∣$ .

[L4]

Truncated fundamental theorem of calculus (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ , The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral): if $α < u < v < β$ then on $[u, v]$ each coordinate function $y^{j}$ is differentiable with continuous derivative $y^{j^{'}}$ , so $y^{j^{'}}$ is Riemann integrable on $[u, v]$ and $\int_{u}^{v} y^{j^{'}} = y^{j} (v) - y^{j} (u)$ .

[L5]

Order, additivity and linearity of the Riemann integral (If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ , For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$ , Integrable functions on $[a, b]$ form a set closed under sums and scalar multiples, and $\int_{a}^{b} (λ f + μ g) = λ \int_{a}^{b} f + μ \int_{a}^{b} g$ ): if $a \leq c \leq d$ and the functions are integrable with $g_{1} \leq g_{2}$ pointwise then $\int_{c}^{d} g_{1} \leq \int_{c}^{d} g_{2}$ , and if $g \geq 0$ then $\int_{c}^{d} g \geq 0$ ; $\int_{c}^{e} g = \int_{c}^{d} g + \int_{d}^{e} g$ for $c \leq d \leq e$ ; and the integral is linear in the integrand.

[L6]

Completeness and least upper bounds (Complete ordered field (least-upper-bound property)): every nonempty subset of $R$ that is bounded above has a least upper bound, and if $S = \sup A$ then no $S - ε$ with $ε > 0$ is an upper bound of $A$ .

[L7]

Norm inequality for vector-valued integrals and the triangle inequality (For $a \leq b$ and $f : [a, b] \to R^{m}$ integrable when $a < b$ , $∥ \int_{a}^{b} f ∥_{2} \leq \int_{a}^{b} ∥ f ∥_{2}$ ; for $a < b$ , $∥ f ∥_{2}$ is integrable, The inner-product norm is definite, homogeneous, and satisfies the triangle inequality, The Euclidean spatial structure and cross product of an inertial frame): for $c \leq d$ and integrable vector-valued $f$ , $∥ \int_{c}^{d} f ∥_{2} \leq \int_{c}^{d} ∥ f ∥_{2}$ ; and $∣ u + w ∣ \leq ∣ u ∣ + ∣ w ∣$ for the Euclidean norm on the spatial space, finite sums included.

[L8]

Square root and continuity facts (Rational powers $a^{r}$ of a positive base, Continuity and derivatives of positive-base real powers, Monotonicity of $r \mapsto a^{r}$ and of $a \mapsto a^{r}$ , Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ , A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions, Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function): $t \mapsto t^{1 / 2}$ is continuous on $(0, \infty)$ and $a^{1 / 2}$ is the unique nonnegative square root of $a$ ; if $0 < s \leq t$ then $s^{1 / 2} \leq t^{1 / 2}$ and $0^{1 / 2} = 0$ ; products and finite sums of continuous real functions are continuous, and the components of a continuous $R^{4}$ -valued map are continuous.

[L9]

The future cone is closed under sums of its elements: if $v$ is future timelike and $w$ is future causal then $v + w$ is future timelike, and a sum of two future causal vectors is future causal. This is the coordinate computation $(v + w)^{0} = v^{0} + w^{0} > ∣ v_{s p} ∣ + ∣ w_{s p} ∣ \geq ∣ v_{s p} + w_{s p} ∣$ , respectively the same with nonstrict inequalities, using [L3] and [L7].

[L10]

Strict positivity of integrals of positive continuous functions (A continuous $f \geq 0$ on $[a, b]$ with $\int_{a}^{b} f = 0$ is identically $0$ , If $m \leq f \leq M$ on $[a, b]$ then $m (b - a) \leq L (f, P) \leq \underline{\int_{a}^{b}} f \leq \overline{\int_{a}^{b}} f \leq U (f, P) \leq M (b - a)$ for every partition $P$ ; in particular every constant function is integrable, with $\int_{a}^{b} c = c (b - a)$ ): if $g$ is continuous and nonnegative on a nondegenerate compact interval $[p, q]$ and $g (u_{0}) > 0$ for some $u_{0} \in [p, q]$ , then $\int_{p}^{q} g > 0$ , because $\int_{p}^{q} g = 0$ would force $g \equiv 0$ on $[p, q]$ ; in particular a continuous function that is strictly positive at every point of $[p, q]$ has strictly positive integral there. Moreover for a real constant $μ$ one has $\int_{p}^{q} μ = μ (q - p)$ , so $\int_{p}^{q} μ > 0$ whenever $μ > 0$ and $p < q$ .

Proof

1.1givenL1L2

The coordinate path $y$ is continuous at the corners and the endpoints of the piece by [L1] and $C^{1}$ on $(α, β)$ , so $y$ is continuous on $[α, β]$ ; on $(α, β)$ each coordinate derivative $y^{j^{'}}$ is continuous by [L1], and by the chart form [L2] one has $- η (x^{'} (u), x^{'} (u)) = (y^{0^{'}} (u))^{2} - ∣ z^{'} (u) ∣^{2}$ for every $u \in (α, β)$ .

2.1step 1.1L3

At every $u \in (α, β)$ the tangent $x^{'} (u)$ is nonzero future causal, so by [L3] $y^{0^{'}} (u) \geq ∣ z^{'} (u) ∣ \geq 0$ and $y^{0^{'}} (u) > 0$ : the spatial inequality uses the coordinate description of the future cone, and strict positivity uses that $x^{'} (u) \neq 0$ rules out the case $y^{'} (u) = 0$ .

2.2step 1.1L4

For $α < u < v < β$ and each $j \in {0, 1, 2, 3}$ the truncated fundamental theorem gives $\int_{u}^{v} y^{j^{'}} = y^{j} (v) - y^{j} (u)$ by [L4].

3.1step 2.1step 2.2L1L5

Letting $u ↓ α$ in the case $j = 0$ of step 2.2, continuity of $y^{0}$ at $α$ gives $\lim_{u ↓ α} \int_{u}^{r} y^{0^{'}} = y^{0} (r) - y^{0} (α)$ , a finite real number; it is nonnegative because $y^{0^{'}} (\cdot) \geq 0$ on $(u, r)$ and [L5] applies to the truncations, $y^{0} (r) - y^{0} (α) \geq 0$ .

3.2step 2.1step 2.2L1L5

Likewise $\lim_{v ↑ β} \int_{r}^{v} y^{0^{'}} = y^{0} (β) - y^{0} (r)$ , finite and nonnegative.

3.3step 2.1L3L8

The functions $∣ z^{'} ∣$ and $f = \sqrt{(y^{0^{'}})^{2} - ∣ z^{'} ∣^{2}}$ are continuous on $(α, β)$ and satisfy $0 \leq ∣ z^{'} ∣ \leq y^{0^{'}}$ and $0 \leq f \leq y^{0^{'}}$ there: $∣ z^{'} ∣^{2}$ is a finite sum of squares of the continuous functions $z^{' i}$ , hence continuous by [L8]; writing $t : = ∣ z^{'} ∣^{2}$ , the composite $t^{1 / 2}$ is continuous where $t > 0$ by [L8], and at a point where $t (u_{0}) = 0$ the estimate $0 \leq ∣ z^{'} (u) ∣ = (∣ z^{'} (u) ∣^{2})^{1 / 2} \leq (\sup_{∣ u - u_{0} ∣ < δ} ∣ z^{'} ∣^{2})^{1 / 2} < ε$ for small $δ$ , using monotonicity of the square root and continuity of $∣ z^{'} ∣^{2}$ at $u_{0}$ , gives continuity there; the same argument applies to $f$ , whose inner function $(y^{0^{'}})^{2} - ∣ z^{'} ∣^{2}$ is continuous and nonnegative by step 2.1; and the domination $f \leq y^{0^{'}}$ , $∣ z^{'} ∣ \leq y^{0^{'}}$ follows from $0 \leq (y^{0^{'}})^{2} - ∣ z^{'} ∣^{2} \leq (y^{0^{'}})^{2}$ , $y^{0^{'}} \geq 0$ and monotonicity of the square root, together with $(y^{0^{'}})^{2}$ 's unique nonnegative square root $y^{0^{'}}$ from [L8].

3.4step 2.2L1

For each $j$ , step 2.2 gives $\int_{u}^{r} y^{j^{'}} = y^{j} (r) - y^{j} (u)$ and $\int_{r}^{v} y^{j^{'}} = y^{j} (v) - y^{j} (r)$ ; letting $u ↓ α$ and $v ↑ β$ , continuity of $y^{j}$ at $α$ and $β$ gives the finite limits $y^{j} (r) - y^{j} (α)$ and $y^{j} (β) - y^{j} (r)$ , whose sum is $y^{j} (β) - y^{j} (α)$ : the signed improper integral of each coordinate derivative equals the corresponding endpoint increment.

4.1step 2.1step 3.1L5L6

Let $g$ be continuous on $(α, β)$ with $0 \leq g \leq y^{0^{'}}$ pointwise, and put $A (u) : = \int_{u}^{r} g$ for $u \in (α, r]$ . For $α < u_{1} < u_{2} \leq r$ , additivity and nonnegativity of the integral [L5] give $A (u_{1}) = A (u_{2}) + \int_{u_{1}}^{u_{2}} g \geq A (u_{2})$ , so $A$ is nondecreasing as $u$ decreases; and $A (u) \leq \int_{u}^{r} y^{0^{'}} = y^{0} (r) - y^{0} (u) \leq y^{0} (r) - y^{0} (α)$ by [L5] and step 3.1. The set ${A (u) : α < u \leq r}$ is nonempty and bounded above, so by [L6] it has a supremum $S$ ; for every $ε > 0$ the number $S - ε$ is not an upper bound, so there is $u_{*}$ with $A (u_{*}) > S - ε$ , and every $α < u < u_{*}$ then satisfies $S - ε < A (u) \leq S$ . Hence $\lim_{u ↓ α} A (u) = S$ exists and is finite.

4.2step 2.1step 3.2L5L6

Symmetrically, $B (v) : = \int_{r}^{v} g$ is nondecreasing in $v$ with $B (v) \leq y^{0} (β) - y^{0} (r)$ by [L5] and step 3.2, so by [L6] $\lim_{v ↑ β} B (v)$ exists and is finite.

5.1step 3.1step 3.2step 3.3step 4.1step 4.2L5

Applying steps 4.1 and 4.2 to $g : = ∣ z^{'} ∣$ and $g : = f$ , which are continuous and dominated by $y^{0^{'}}$ by step 3.3, and passing the truncation inequalities to the finite limits, gives finite improper integrals with $\int_{(α, β)} f \leq \int_{(α, β)} y^{0^{'}} = y^{0} (β) - y^{0} (α)$ .

5.2step 4.1step 4.2L5

The improper value is independent of $r$ : for $α < r_{1} < r_{2} < β$ and any admissible $g$ , the two-sided limit $\lim_{u ↓ α, v ↑ β} \int_{u}^{v} g$ exists and equals $\int_{(α, β)} g$ computed with $r = r_{1}$ , because $\int_{u}^{v} g = \int_{u}^{r_{1}} g + \int_{r_{1}}^{v} g$ by [L5] and the two one-sided limits add; the same identity with $r_{2}$ exhibits the same two-sided limit as the value computed with $r = r_{2}$ , so the two values agree.

6.1step 2.1step 4.1step 4.2step 5.1

For each $j$ the absolute value $∣ y^{j^{'}} ∣$ is continuous on $(α, β)$ with $0 \leq ∣ y^{j^{'}} ∣ \leq y^{0^{'}}$ by step 2.1, so steps 4.1 and 4.2 give $\int_{(α, β)} ∣ y^{j^{'}} ∣ \leq y^{0} (β) - y^{0} (α) < \infty$ : every coordinate derivative is absolutely improperly Riemann integrable.

6.2step 5.2L5

Additivity under subdivision: for $α < γ < β$ and admissible $g$ , splitting $\int_{u}^{v} g = \int_{u}^{γ} g + \int_{γ}^{v} g$ and passing to the one-sided limits gives $\int_{(α, β)} g = \int_{(α, γ)} g + \int_{(γ, β)} g$ .

7.1step 2.1step 5.1step 3.4step 6.1L5L7L10

For a piece $(s_{i - 1}, s_{i})$ write $Δ_{i} : = y (s_{i}) - y (s_{i - 1})$ and $Δ_{i, s p} : = z (s_{i}) - z (s_{i - 1})$ . By steps 4.1 and 4.2, $Δ_{i}^{0} = \int_{(s_{i - 1}, s_{i})} y^{0^{'}} > 0$ : the improper value dominates the ordinary integral of the continuous function $y^{0^{'}}$ over any nondegenerate compact interior subinterval, and that ordinary integral is strictly positive by [L10] because $y^{0^{'}} > 0$ at every point of the subinterval by step 2.1; and $∣ Δ_{i, s p} ∣ = ∥ \int_{(s_{i - 1}, s_{i})} z^{'} ∥_{2} \leq \int_{(s_{i - 1}, s_{i})} ∣ z^{'} ∣ \leq \int_{(s_{i - 1}, s_{i})} y^{0^{'}} = Δ_{i}^{0}$ , the first inequality by [L7] applied to the truncations and passed to the limit, the second by step 2.1 and [L5].

7.2step 6.2

Independence of the admissible partition: let two finite partitions of $[a, b]$ be admissible and let their union be the common refinement, whose points split each piece of either partition into finitely many subintervals; by step 6.2 the total sum over each piece equals the sum of the values over its subintervals, and inductively the total over the refined partition equals the total over each original partition, so the two finite sums agree.

8.1step 7.1L3L7

Summing over the finitely many pieces gives $D^{0} = \sum_{i} Δ_{i}^{0} > 0$ and, by the triangle inequality of [L7] for the finite sum $\sum_{i} Δ_{i, s p}$ and by step 7.1, $∣ D_{s p a t i a l} ∣ \leq \sum_{i} ∣ Δ_{i, s p} ∣ \leq \sum_{i} Δ_{i}^{0} = D^{0}$ ; hence $D$ is nonzero future causal by [L3].

8.2step 7.1L5L10

Coordinate time is strictly increasing on every nondegenerate subinterval: for $s < t$ in $[a, b]$ , the increment $y^{0} (t) - y^{0} (s)$ decomposes as a sum of increments over the pieces that meet $[s, t]$ , each nonnegative by step 7.1 and at least one strictly positive because $(s, t)$ is nonempty and open and meets some piece in a nondegenerate interval, over which $y^{0^{'}}$ is continuous and positive and hence has strictly positive integral by [L10].

9.1step 5.1step 7.1step 8.1L3L5L10

If an interior point $c \in (α, β)$ has $x^{'} (c)$ future timelike, then $y^{0^{'}} (c) - ∣ z^{'} (c) ∣ > 0$ by [L3]; the function $y^{0^{'}} - ∣ z^{'} ∣$ is continuous on $(α, β)$ by steps 1.1 and 3.3, so there are $δ > 0$ and $μ > 0$ with $y^{0^{'}} - ∣ z^{'} ∣ \geq μ$ on $[c - δ, c + δ] \subset (α, β)$ . Then $D^{0} - ∣ D_{s p a t i a l} ∣ \geq \sum_{i} (Δ_{i}^{0} - ∣ Δ_{i, s p} ∣) \geq \int_{(α, β)} (y^{0^{'}} - ∣ z^{'} ∣) \geq \int_{c - δ}^{c + δ} μ = μ \cdot 2 δ > 0$ by steps 3.4, 6.2, 7.1, [L5] and the constant-integral value of [L10], so $D$ is future timelike by [L3].

9.2step 7.1step 8.1L3L9

If a one-sided endpoint tangent is future timelike, say the right quotient of the piece at $s^{*} \in {a} \cup {s_{1}, \dots, s_{m - 1}}$ is the future timelike vector $v = y^{'} (s^{*} +)$ , then for small $h > 0$ the quotient $(y (s^{*} + h) - y (s^{*})) / h$ is eventually future timelike, since it tends to $v$ and the future timelike set is open by [L3]; so $y (s^{*} + h) - y (s^{*}) = h q_{h}$ is future timelike. Split $D = [y (s^{*}) - y (a)] + [y (s^{*} + h) - y (s^{*})] + [y (b) - y (s^{*} + h)]$ : the first bracket is absent when $s^{*} = a$ and is otherwise future causal by steps 6.2 and 7.1 applied to the restriction to $[a, s^{*}]$ , the middle bracket is future timelike, and the last bracket is future causal by steps 6.2 and 7.1 applied to the restriction to $[s^{*} + h, b]$ ; applying [L9] to the timelike middle bracket and the future causal last bracket, and then once more when the future causal first bracket is present, makes $D$ future timelike, and the cases of a left one-sided endpoint tangent are symmetric.

10.1step 9.1step 9.2∎

The argument uses only finite-dimensional coordinate computations, truncated Riemann integrals and one-sided limits: no derivative-limit hypothesis on the open pieces, no Lebesgue integration, no clock identification and no choice principle are used.

Remarks

The improper integrals need not be closed-piece Riemann integrals. The derivative is not assumed to extend continuously to the corners, and no bound on $∣ x^{'} ∣$ near a corner is assumed; the only estimate used is the coordinate domination $0 \leq ∣ z^{'} ∣ \leq y^{0^{'}}$ , which turns the (possibly unbounded) spatial derivatives into functions dominated by the milder quantity $y^{0^{'}}$ , itself controlled by the endpoint increment through the truncated fundamental theorem.
Where the causal hypothesis is spent. The sign of $η$ alone never enters the integrability conclusions: $\int y^{0^{'}}$ is a finite increment because $y^{0^{'}}$ is a derivative, and domination by $y^{0^{'}}$ needs only $∣ z^{'} ∣ \leq y^{0^{'}}$ , which is the future causal inequality. The strict positivity $y^{0^{'}} > 0$ uses in addition that the tangent is nonzero; the strict timelikeness conclusions of clause (d) are the only place where a future timelike (not merely causal) tangent is used.
The statement is chart-relative for the improper integrals and chart-independent for the displacement. The improper integrals are formed in a fixed inertial chart; the conclusions $D \in cl (C^{+}) ∖ {0}$ , strict coordinate-time monotonicity and the timelikeness criterion are statements about the intrinsic displacement $D$ and the intrinsic tangents, since the coordinate criterion of [L3] describes the same cone in every inertial chart.

Improper integrability and endpoint increments of weak piecewise future causal curves

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources