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.

The causal past of a point truncated by the causal future of the initial Cauchy surface is compact

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, g, N, j, ψ)$ be a development of the given data in the sense of Smooth developments of constrained initial data, data-fixing isometries, development embeddings and maximality clause (a), write $Σ : = j (Σ)$ , and let $h$ be the auxiliary complete metric of The auxiliary Riemannian metric h=g+2n-flat tensor n-flat is complete after a proper-exhaustion conformal factor, and its closed bounded sets are compact. Then for every $q \in M$ the set $K_{q} : = J^{-} (q) \cap J^{+} (Σ)$ is compact. Moreover $K_{q} = {q}$ when $q \in Σ$ , and $K_{q}$ is empty when $q \in I^{-} (Σ)$ .

Facts & Assumptions

Given: a development $(M, g, N, j, ψ)$ with Cauchy set $Σ = j (Σ)$ , a point $q \in M$ , and a sequence $x_{n} \in K_{q}$ to be shown to have a convergent subsequence.

[L1]

Global hyperbolicity and sides: $Σ$ Cauchy implies that $M$ is globally hyperbolic, hence strongly causal and causal, with closed causal relation and closed $J^{-} (q)$ (The existence of a Cauchy set implies strong causality and compact causal diamonds clauses (a)-(c), In a globally hyperbolic manifold the causal relation is closed and truncated causal cones over compact sets are compact clause (a)). The Cauchy trichotomy is $M = I^{-} (Σ) ⊔ Σ ⊔ I^{+} (Σ)$ , with $Σ$ acausal (Cauchy sets are closed, split the manifold into past, set and future, and are locally Lipschitz graphs clause (a)). In fact $J^{+} (Σ) = Σ \cup I^{+} (Σ)$ : the right side is contained in the left by reflexivity and timelike reachability. Conversely, if $σ \leq x$ for $σ \in Σ$ and $x \in I^{-} (Σ)$ , choose $ζ \in Σ$ with $x ≪ ζ$ . Concatenation gives a causal segment from $σ$ to $ζ$ ; distinct endpoints contradict acausality, and equal endpoints give a nonconstant closed causal segment, contradicting causality. Trichotomy excludes all other possibilities outside the right side. Thus $J^{+} (Σ) = M ∖ I^{-} (Σ)$ is closed, because $I^{-} (Σ) = ⋃_{ζ \in Σ} I^{-} (ζ)$ is open (Openness of the chronological future and past, openness of the chronological relation, and closure of future and past sets clause (a), Chart independence, concatenation, reparametrization and transitivity for causal curves clauses (d),(f)). The reversed argument gives $J^{-} (Σ) = Σ \cup I^{-} (Σ)$ and $J^{+} (Σ) \cap J^{-} (Σ) = Σ$ .

[L2]

Auxiliary metric: throughout this item $h$ denotes the complete conformally rescaled metric called $h^{'}$ in The auxiliary Riemannian metric h=g+2n-flat tensor n-flat is complete after a proper-exhaustion conformal factor, and its closed bounded sets are compact clauses (b)-(d). It is a smooth positive definite metric, its distance induces the manifold topology, closed $h$ -bounded subsets are compact, and the $h$ -arclength of a causal curve dominates the $h$ -distance of its endpoints (The auxiliary Riemannian metric h=g+2n-flat tensor n-flat is complete after a proper-exhaustion conformal factor, and its closed bounded sets are compact, Basic limit curve lemma: arclength-parametrized causal curves have causal limit curves on compact parameter intervals and future-inextendible limits on half-lines).

[L3]

Length bound on compact sets: for every compact $K \subseteq M$ there is $L (K)$ such that every causal curve with image in $K$ has $h$ -arclength at most $L (K)$ (Strong causality bounds the auxiliary length of causal curves contained in a compact set).

[L4]

Half-line limits: future causal curves parametrized by $h$ -arclength whose intervals contain $[- n, 0]$ and whose value at $0$ converges admit a subsequence converging uniformly in $d_{h}$ on every compact subinterval of $(- \infty, 0]$ to a past-inextendible future causal curve, which is nonconstant on every nondegenerate interval (Basic limit curve lemma: arclength-parametrized causal curves have causal limit curves on compact parameter intervals and future-inextendible limits on half-lines clause (b) and its dual, clause (a4)).

[L5]

Inextendible extension and compaction: a one-sided-inextendible causal curve is contained in an inextendible causal curve (Equivalence of the absolutely-continuous and continuous causal conventions, and one-sided inextendible extensions clause (d)); a closed causal segment lies on an inextendible causal curve (Convergent causal ends are extendible, maximal geodesics have no limit, and Cauchy sets are acausal clause (c)); a compact causal diamond is compact and a causal segment with endpoints in different components cannot be confined to one diamond (The existence of a Cauchy set implies strong causality and compact causal diamonds clause (c)).

[L6]

Metrizable topology on the relevant component: a causal curve stays in one connected component of $M$ . Each component is closed and open, and by [L2] its auxiliary Riemannian distance induces its manifold topology. When $K_{q}$ is nonempty it lies in the component containing $q$ , because every $x \leq q$ is joined to $q$ by a continuous curve (or equals $q$ ). A subset of this metric space is compact exactly when it is sequentially compact, under the stated Countable and Dependent Choice assumptions (For a metric space, compact, countably compact, limit point compact, sequentially compact, and complete together with totally bounded are all equivalent, given countable choice and dependent choice, Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric, Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right). The empty case is compact directly. No general manifold metrization theorem or arbitrary-index choice is used.

Proof

technique · direct

1.1L1algebra

(The two easy cases.) If $q \in Σ$ and $x \in K_{q}$ , then $x \in J^{+} (Σ) \cap J^{-} (Σ) = Σ$ by [L1]. The relation $x \leq q$ and acausality force $x = q$ , while $q \in K_{q}$ by reflexivity. Hence $K_{q} = {q}$ . If $q \in I^{-} (Σ)$ and $x \in K_{q}$ , then some $σ \in Σ$ satisfies $σ \leq x \leq q$ , so $q \in J^{+} (Σ)$ by transitivity, contradicting [L1]. Thus $K_{q} = \emptyset$ .

1.2L1L6algebra

(Closure of $K_{q}$ and reduction to sequential compactness.) For every $q$ , $K_{q}$ is the intersection of the two closed sets $J^{-} (q)$ and $J^{+} (Σ)$ ([L1]), hence closed. By [L6] it remains to show that every sequence in $K_{q}$ has a convergent subsequence.

1.3givenL1L3chooseconstruct

(Curves through the sequence.) Assume $q \notin Σ$ and $q \notin I^{-} (Σ)$ , so $q \in I^{+} (Σ)$ by [L1]; let $x_{n} \in K_{q}$ . For each $n$ choose $σ_{n} \in Σ$ with $σ_{n} \leq x_{n}$ and concatenate a causal curve from $σ_{n}$ to $x_{n}$ with one from $x_{n}$ to $q$ (omitting any equality segment), obtaining a future causal curve $β_{n}$ from $σ_{n}$ to $q$ whose image contains $x_{n}$ , is contained in $J^{+} (σ_{n}) \cap J^{-} (q)$ , and has finite $h$ -arclength (a compact causal diamond) ([L1], [L3], Causal curves, chronological and causal reachability, and inextendibility). Reparametrize $β_{n}$ by $h$ -arclength from $q$ backwards: this gives a future causal curve $α_{n} : [- L_{n}, 0] \to M$ with $α_{n} (0) = q$ , $α_{n} (- L_{n}) = σ_{n}$ and with $x_{n} = α_{n} (- s_{n})$ for the $h$ -arclength $s_{n} \in [0, L_{n}]$ of the segment from $x_{n}$ to $q$ .

2.1step 1.3L1L2algebra

(Bounded length case.) Suppose some subsequence of $(L_{n})$ is bounded by $C$ . Then for the corresponding $n$ one has $s_{n} \leq L_{n} \leq C$ , so $x_{n} = α_{n} (- s_{n})$ lies in the closed $h$ -ball of radius $C$ around $q$ , which is compact by [L2]; the sequence $(x_{n})$ therefore has a convergent subsequence, whose limit lies in $K_{q}$ by step 1.2.

2.2step 1.3L1L4algebra

(Unbounded length case is impossible.) Suppose instead that $L_{n} \to \infty$ along a subsequence. The curves $α_{n}$ are parametrized by $h$ -arclength with $α_{n} (0) = q$ and intervals containing $[- m, 0]$ for all sufficiently large $n$ , for each fixed positive integer $m$ ; by [L4] there is a subsequence converging uniformly in $d_{h}$ on every compact subinterval of $(- \infty, 0]$ to a past-inextendible future causal curve $α : (- \infty, 0] \to M$ with $α (0) = q$ , nonconstant on every nondegenerate interval. For each fixed $t \leq 0$ , $α (t) = \lim α_{n_{k}} (t)$ , and each $α_{n_{k}} (t)$ lies in $J^{+} (Σ)$ (it is on the causal curve $β_{n_{k}}$ from $Σ$ to $q$ ) and in $J^{-} (q)$ ; by closedness [L1] $α (t) \in K_{q}$ , so $α ((- \infty, 0]) \subseteq J^{+} (Σ)$ .

3.1step 2.2L1L4L5contradiction

(Contradiction in the unbounded case.) Let $α$ be as in step 2.2. First, $α$ misses $Σ$ : if $α (t_{0}) \in Σ$ for some $t_{0}$ , then for every $t < t_{0}$ one has $α (t) \leq α (t_{0}) \in Σ$ and, by step 2.2, $α (t) \in J^{+} (Σ)$ ; hence $α (t) \in J^{+} (Σ) \cap J^{-} (Σ) = Σ$ by [L1], so $α$ maps the nondegenerate interval $(- \infty, t_{0}]$ into $Σ$ ; two distinct values would be causally related points of the acausal set $Σ$ ([L1]), and the only alternative is that $α$ is constant on a nondegenerate interval, which [L4] excludes. Now extend $α$ to an inextendible causal curve $\hat{α} : I \to M$ with $(- \infty, 0] \subseteq I$ by [L5]; as an inextendible causal curve it meets $Σ$ in exactly one parameter value $c$ ([L1]). Since $α$ misses $Σ$ , $c \notin (- \infty, 0]$ . If $c > 0$ , then $q = \hat{α} (0) \leq \hat{α} (c) \in Σ$ with $q \in I^{+} (Σ)$ : choosing $σ \in Σ$ with $σ ≪ q$ gives $σ \leq \hat{α} (c) = : ζ \in Σ$ , and acausality forces $σ = ζ$ , so $ζ ≪ q \leq ζ$ is a nonconstant closed causal curve, contradicting causality [L1]. Hence the unbounded length case cannot occur.

4.1step 1.1step 1.2step 2.1step 3.1L6∎

(Conclusion.) By steps 2.1 and 2.2 every sequence in $K_{q}$ has a convergent subsequence in $M$ with limit in $K_{q}$ ; with step 1.2 and [L6] this makes $K_{q}$ compact. The remaining assertions are step 1.1.

Remarks

The statement is the compactness of "the past of $q$ truncated by the initial surface", used in An exposed boundary point: the last boundary point of a boundary null geodesic has no other boundary point in its past and The exposed boundary point controls the complement: J^-(q) cap U^c cap J^+(Sigma) is confined to a prescribed neighbourhood. The proof shows in addition that the $h$ -arclength of causal curves from $Σ$ to a fixed $q$ is bounded, since boundedness of the length was exactly the alternative that survived.

The causal past of a point truncated by the causal future of the initial Cauchy surface is compact

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources