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.

Strip functions: every inner strip carries a smooth function with past timelike gradient, constant below and above the outer levels

Statement

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 actual volume-time and causal suppliers. Let $(M, g, N)$ be a globally hyperbolic time-oriented smooth Lorentzian four-manifold (Chronology, causality, strong causality, global hyperbolicity and time functions clause (c)), let $t$ be the volume time function of The Geroch volume function: a continuous strictly increasing time function whose levels are Cauchy sets, and let $a < a^{'} < c^{'} < c$ be real numbers. Then there is a smooth function $v : M \to [- 1, 1]$ such that

(a) $v = - 1$ on ${t \leq a}$ and $v = + 1$ on ${t \geq c}$ ;

(b) $\nabla v$ is past causal or zero at every point of $M$ ;

(c) $\nabla v$ is past timelike at every point of the inner strip ${a^{'} \leq t \leq c^{'}}$ .

Facts & Assumptions

Given: Countable Choice and Dependent Choice; A globally hyperbolic $(M, g, N)$ with volume time $t$ and real numbers $a < a^{'} < c^{'} < c$ .

[L1]

Weak steps: for all reals $a < b < c$ there is a smooth $τ : M \to [- 1, 1]$ with $τ = - 1$ on ${t \leq a}$ , $τ = + 1$ on ${t \geq c}$ , $\nabla τ$ past causal or zero everywhere, and $\nabla τ$ past timelike at every point of $S_{b}$ , hence on an open neighborhood $U$ of $S_{b}$ (Weak steps: locally finite sums of cone bumps give a smooth step around each Cauchy level with past timelike gradient near the level).

[L2]

Cone algebra: the past causal vectors together with $0$ form a closed convex cone; a sum of past-causal vectors is past causal, and the sum of one past-timelike vector with any past-causal vector is past timelike. The cone is the closure of the open past timelike cone, so a limit of past-causal vectors is only guaranteed to be past causal or zero (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, The inverse metric, musical isomorphisms and index raising).

[L3]

Exhaustions and boxes: there is a smooth proper $f : M \to [0, \infty)$ (Every smooth manifold admits a smooth proper exhaustion function); the sets $L_{j} : = f^{- 1} ([0, j])$ are compact with $L_{j} \subseteq Int L_{j + 1}$ and $⋃_{j} L_{j} = M$ . There is a countable family $(B_{i}, x_{i})_{i \geq 1}$ of relatively compact coordinate balls whose interiors cover $M$ (Assuming Countable Choice, every smooth manifold admits a countable smooth atlas with relatively compact domains). Compactness of a subset agrees for the manifold topology and any metric inducing it, and a continuous real function on a nonempty compact metric space attains its maximum (For a metric space with its metric topology, compactness in the topological sense is compactness in the metric sense, and the two notions of compact subset coincide, A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value, Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).

[L4]

Series calculus: if a series of functions converges uniformly on a set and its termwise derivatives converge uniformly, then on each coordinate line segment the partial sums satisfy the hypotheses of the uniform-derivative limit theorem, so the limit is differentiable with the derivative of the limit given by the differentiated series; iterating this coordinate-line argument through all orders gives a smooth limit whose coordinate derivatives are the termwise differentiated series (The Weierstrass M-test gives absolute pointwise convergence and uniform convergence of a function series, If continuously differentiable functions converge at one point and their derivatives converge uniformly on a closed interval, then the functions converge uniformly to a differentiable function whose derivative is the derivative limit, The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , $C^{r}$ and smooth maps between smooth manifolds).

[L5]

A smooth function is bounded with all its coordinate derivatives through any finite order on the compact closure of a coordinate ball, by continuity and [L3] ( $C^{r}$ and smooth maps between smooth manifolds, Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point).

Proof

technique · constructive

1.1L1L3givenchoose

(Finite lists of weak steps for each compact slice.) For $j \geq 1$ put $K_{j} : = L_{j} \cap {a^{'} \leq t \leq c^{'}}$ , compact by [L3]. Consider all tuples $(b, τ, U)$ with $b \in [a^{'}, c^{'}]$ , $τ$ a weak step supplied by [L1] with outer bounds $a, c$ , and $U$ its open past-timelike-gradient locus containing $S_{b}$ . Their open sets cover $K_{j}$ , since at $x \in K_{j}$ a tuple exists with $b = t (x)$ . Compactness supplies a finite tuple list covering $K_{j}$ . For empty $K_{j}$ , a single tuple at $b = (a^{'} + c^{'}) / 2$ is available, so every list may be taken nonempty. Countable Choice selects one nonempty finite list for each $j$ . Write its entries $(b_{j, i}, τ_{j, i}, U_{j, i})$ , $1 \leq i \leq m_{j}$ . No weak-step family indexed by all real levels is selected.

2.1step 1.1L1L2given

(The averaged slice functions.) Define $v_{j} : = \frac{1}{m_{j}} \sum_{i = 1}^{m_{j}} τ_{j, i}$ . Then $v_{j}$ is smooth, $v_{j} = - 1$ on ${t \leq a}$ and $v_{j} = + 1$ on ${t \geq c}$ because every summand has these properties, $∣ v_{j} ∣ \leq 1$ , and $\nabla v_{j}$ is past causal or zero everywhere as a finite average of past causal or zero vectors [L2]. On $K_{j}$ the gradient is past timelike: at $x \in K_{j}$ some $i$ satisfies $x \in U_{j, i}$ , so $\nabla τ_{j, i} (x)$ is past timelike and all other summands are past causal or zero, whence the finite sum $\nabla v_{j} (x)$ is past timelike by [L2].

3.1step 2.1L3L5choose

(Derivative bounds.) For each $j \geq 1$ the set $\overline{B_{1}} \cup \dots \cup \overline{B_{j}}$ is compact and the finitely many functions $\partial^{α} v_{j}$ , $∣ α ∣ \leq j$ , are continuous, so by [L5] each of them has a finite maximum there; let $A_{j} \geq 1$ be an integer bounding all these maxima. Since $∣ v_{j} ∣ \leq 1 \leq A_{j}$ as well, every coordinate derivative of $v_{j}$ of order at most $j$ is bounded by $A_{j}$ on the closures of the first $j$ boxes.

4.1step 3.1L3L4construct

(The series.) Put $c_{j} : = 2^{- j} A_{j}^{- 1}$ and $C : = \sum_{j \geq 1} c_{j}$ , a positive real number with $C \leq 1$ , and define $v : = \frac{1}{C} \sum_{j \geq 1} c_{j} v_{j}$ . On the box $B_{i}$ , for every multiindex $α$ and every $j \geq \max (i, ∣ α ∣)$ the bound of step 3.1 gives $\sup_{B_{i}} ∣ \partial^{α} (c_{j} v_{j}) ∣ \leq 2^{- j}$ , so by the Weierstrass M-test the series $\sum_{j} c_{j} v_{j}$ and each of its termwise coordinate derivative series $\sum_{j} c_{j} \partial^{α} v_{j}$ converge uniformly on $B_{i}$ ; since the boxes cover $M$ , this holds on every compact set after finitely many boxes. Applying the coordinate-line argument of [L4] inductively in the order of differentiation, $v$ is smooth on $M$ and every coordinate derivative of $v$ is the corresponding termwise derivative of the series.

5.1step 2.1step 4.1L2givendischarge-construct∎

(Properties of the series.) On ${t \leq a}$ all summands equal $- 1$ , so $v = - 1$ ; on ${t \geq c}$ they equal $+ 1$ , so $v = + 1$ ; and $∣ v ∣ \leq 1$ because $C = \sum_{j} c_{j}$ and $∣ v_{j} ∣ \leq 1$ . Termwise differentiation gives $\nabla v = \frac{1}{C} \sum_{j \geq 1} c_{j} \nabla v_{j}$ . Its partial sums lie in the closed past-causal cone by [L2], hence their limit is past causal or zero; this proves (b). Now fix $x$ in the inner strip and choose $j_{0}$ with $x \in L_{j_{0}}$ . Then $x \in K_{j_{0}}$ , so $c_{j_{0}} \nabla v_{j_{0}} (x)$ is past timelike by step 2.1. The series of all remaining terms converges by step 4.1; its partial sums are past causal or zero by [L2], so its limit is past causal or zero by closedness of that cone. The sum of the fixed past-timelike vector and this limiting past-causal vector is past timelike by [L2]. Thus $\nabla v (x)$ is past timelike, proving (c) without treating a limit of timelike vectors as timelike.

Remarks

Why the average is needed. A single weak step has a timelike gradient only near its own level, so a compact slice is covered by finitely many such neighborhoods and the average turns this cover into one function that is strictly timelike on the whole slice; the exhaustion then lets countably many slice functions be summed with rapidly decaying coefficients.
Why the gradient bounds are enough. The coefficients $2^{- j} A_{j}^{- 1}$ only have to absorb the bounds on the first $j$ boxes through order $j$ , so each derivative series is dominated there by $\sum_{j} 2^{- j}$ ; no uniformity in the point is needed beyond compactness of the boxes.
Use. The strip functions are the building blocks of Smooth Cauchy temporal splitting: a global temporal function with Cauchy levels and an orthogonal complete flow: applied to the strips $[j - 2, j + 2]$ with inner strip $[j - 1, j + 1]$ , their paired sum is a global temporal function.

Depends on

Dependency tree · 2 levels

Sources

A. N. Bernal and M. Sanchez, Smoothness of time functions and the metric splitting of globally hyperbolic spacetimes (arXiv:gr-qc/0401112), Corollary 3.9, Lemma 3.10 and Theorem 3.11, printed pp. 6-7: finite averaging and derivative-controlled series.