TheoremStatement: 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 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

Statement

Assume the Axiom of Countable Choice ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $(M, g, N)$ be a time-oriented smooth Lorentzian four-manifold (Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model) and put $n : = \frac{N}{\sqrt{- g (N, N)}} (pointwise), h : = g + 2 n^{♭} \otimes n^{♭},$ with the flat map $♭$ of The inverse metric, musical isomorphisms and index raising, so that $h$ is a smooth covariant $2$ -tensor field (Smooth covariant 2-tensor fields on a smooth manifold). Then:

For each connected component $M_{0} \subseteq M$ and smooth Riemannian metric $H$ , let $d_{H}$ denote the Riemannian distance of $H ∣_{M_{0}}$ . For the following absolutely continuous length assertion, also assume Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain), as required by the cited fundamental theorem. For any locally absolutely continuous curve $γ : [a, b] \to M_{0}$ , use the length $ℓ_{H} (γ) : = \int_{a}^{b} \sqrt{H_{γ (t)} (γ^{'} (t), γ^{'} (t))} d t,$ with the Lebesgue integral and almost-everywhere derivative. This extends the piecewise- $C^{1}$ length of Riemannian speed and length. The distance from Riemannian distance on a connected manifold satisfies $d_{H} (γ (a), γ (b)) \leq ℓ_{H} (γ)$ ; the proof is included below.

(a) $h$ is a smooth Riemannian (positive definite) metric on $M$ .

(b) There is a smooth nonnegative proper function $f : M \to [0, \infty)$ such that the metric $h^{'} : = (1 + ∣ d f ∣_{h}^{2}) h$ is a smooth Riemannian metric with $∣ d f ∣_{h^{'}} \leq 1$ everywhere.

(c) For each connected component $M_{0}$ of $M$ , the metric space $(M_{0}, d_{h^{'}})$ is complete, where $d_{h^{'}}$ is the Riemannian distance of $h^{'} ∣_{M_{0}}$ (Riemannian distance on a connected manifold, Riemannian distance is a metric).

(d) Consequently, for every connected component $M_{0}$ , every subset of $M_{0}$ that is closed in $M_{0}$ and bounded in $d_{h^{'}}$ is compact, and every closed ball ${q \in M_{0} : d_{h^{'}} (q, p) \leq r}$ is compact.

Facts & Assumptions

Given: The Axiom of Countable Choice, a time-oriented smooth Lorentzian four-manifold $(M, g, N)$ , the fields $n$ , $h$ , and a connected component $M_{0}$ of $M$ .

[L1]

$n$ is smooth, nowhere vanishing, with $g (n, n) = - 1$ and $g (n, N) < 0$ ; the flat map is the smooth bundle isomorphism $X \mapsto g (X, \cdot)$ and $n^{♭}$ is the smooth covector field $g (n, \cdot)$ ; tensor products and sums of smooth tensor fields are smooth (Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model, Observers, rest spaces and the spatial projection at an event, The inverse metric, musical isomorphisms and index raising, Smooth covariant 2-tensor fields on a smooth manifold).

[L2]

For a timelike vector $u$ the orthogonal complement $u^{⊥} = {w : g (w, u) = 0}$ is a three-dimensional positive definite subspace, and every $v \in T_{q} M$ decomposes uniquely as $v = α n_{q} + w$ with $w \in n_{q}^{⊥}$ and $α = - g_{q} (v, n_{q})$ ; then $g_{q} (v, v) = - α^{2} + g_{q} (w, w)$ (The observer rest-space decomposition and the spatial projection clauses 1 and 3, eta-orthogonality and orthogonal complements in a Lorentz vector space, Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model).

[L3]

For a smooth positive definite metric $H$ and a smooth function $u$ , the metric $H^{'} = (1 + ∣ d u ∣_{H}^{2}) H$ has inverse $H^{' - 1} = (1 + ∣ d u ∣_{H}^{2})^{- 1} H^{- 1}$ and satisfies $∣ d u ∣_{H^{'}}^{2} = ∣ d u ∣_{H}^{2} / (1 + ∣ d u ∣_{H}^{2}) \leq 1$ ; this is multilinear algebra applied at each point (The inverse metric, musical isomorphisms and index raising).

[L4]

Assuming ${A C}_{ω}$ , there is a smooth nonnegative proper function $f : M \to [0, \infty)$ , that is, every closed sublevel $f^{- 1} ([0, c])$ is compact (Every smooth manifold admits a smooth proper exhaustion function).

[L5]

If $H$ is a smooth positive definite metric on a connected smooth manifold $M_{0}$ and $γ : [a, b] \to M_{0}$ is a locally absolutely continuous curve, then $∣ u (γ (b)) - u (γ (a)) ∣ \leq \int_{a}^{b} ∣ d u ∣_{H} (γ (t)) ∣ γ^{'} (t) ∣_{H} d t$ for every smooth $u$ , by the chain rule and the Cauchy-Schwarz inequality in $H$ , together with the absolutely continuous calculus (Absolute continuity on a compact interval, Absolutely continuous functions have integrable derivatives, Fundamental theorem of calculus for absolutely continuous functions, Chart independence, concatenation, reparametrization and transitivity for causal curves clause (b)).

[L6]

The Riemannian distance $d_{H}$ of a smooth positive definite metric $H$ on a connected manifold is a metric, and it induces the manifold topology; in particular metric limits and topological limits agree, and a subset is compact for $d_{H}$ exactly when it is compact in the manifold topology (Riemannian distance on a connected manifold, Riemannian distance is a metric, The riemannian distance topology is the manifold topology, Open ball, closed ball and sphere in a metric space).

[L7]

Topological compactness for a metric topology equals metric compactness (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). In ZF a compact metric space is sequentially compact (In any metric space compactness implies countable compactness and limit point compactness, and each of countable compactness and limit point compactness implies sequential compactness; every implication here is proved without a choice principle, clauses 1 and 3). A Cauchy sequence with a convergent subsequence converges to its subsequential limit (A Cauchy sequence in a metric space with a convergent subsequence converges to that subsequence’s limit).

[L8]

Hopf-Rinow, under ${A C}_{ω}$ : for a connected Riemannian manifold $(M_{0}, H)$ , completeness of $(M_{0}, d_{H})$ is equivalent to every closed $d_{H}$ -bounded subset being compact, and closed metric balls are then compact (Hopf–Rinow theorem, conditions 1 and 5).

Proof

technique · direct

1.1L1L2givenalgebra

(Clause (a).) Let $q \in M$ and $v \in T_{q} M$ nonzero, and decompose $v = α n_{q} + w$ as in [L2]. Then $g_{q} (v, n_{q}) = - α$ , so $h_{q} (v, v) = g_{q} (v, v) + 2 g_{q} (v, n_{q})^{2} = - α^{2} + g_{q} (w, w) + 2 α^{2} = α^{2} + g_{q} (w, w) .$ If $w \neq 0$ then $g_{q} (w, w) > 0$ by positive definiteness on $n_{q}^{⊥}$ , so $h_{q} (v, v) > 0$ ; if $w = 0$ then $α \neq 0$ and $h_{q} (v, v) = α^{2} > 0$ . Symmetry of $h$ is inherited from $g$ and the symmetric product $n^{♭} \otimes n^{♭}$ , and smoothness from [L1]. This proves (a).

1.2L5L6givenalgebra

(Length and the distance for locally absolutely continuous curves.) Let $M_{0}$ be a connected component, let $H$ be a smooth Riemannian metric on it, and let $γ : [a, b] \to M_{0}$ be locally absolutely continuous. Its image is compact, so subdivide $[a, b]$ into finitely many pieces whose coordinate images lie in convex chart balls with compact closure. On each piece the smooth metric coefficients are bounded and the coordinate derivative is integrable; hence the integrand defining $ℓ_{H}$ is measurable and dominated by a constant times the Euclidean coordinate speed, so $ℓ_{H} (γ) < \infty$ . Fix $ε \in (0, 1)$ . Refine the subdivision so that on each piece the metric matrix differs from a fixed positive form $H_{i}$ by relative bounds $(1 - ε) H_{i} \leq H \leq (1 + ε) H_{i}$ , which is possible by continuity and compactness. For the coordinate endpoints $x_{i}, x_{i + 1}$ of a piece, the straight coordinate segment stays in its convex chart ball and has $H$ -length at most $\sqrt{1 + ε} ∣ x_{i + 1} - x_{i} ∣_{H_{i}}$ . Since $x_{i + 1} - x_{i} = \int x^{'} (t) d t$ , the triangle inequality for the norm induced by $H_{i}$ gives $∣ x_{i + 1} - x_{i} ∣_{H_{i}} \leq \int ∣ x^{'} (t) ∣_{H_{i}} d t \leq (1 - ε)^{- 1 / 2} \int \sqrt{H_{γ (t)} (γ^{'} (t), γ^{'} (t))} d t .$ The distance between the piece endpoints is no larger than the length of this piecewise- $C^{1}$ segment. Summing over pieces and using the triangle inequality for $d_{H}$ gives $d_{H} (γ (a), γ (b)) \leq \sqrt{(1 + ε) / (1 - ε)} ℓ_{H} (γ)$ . Letting $ε ↓ 0$ proves the asserted inequality.

2.1step 1.1L3L4given

(The conformal factor.) By [L4] choose a smooth nonnegative proper $f$ and set $h^{'} : = (1 + ∣ d f ∣_{h}^{2}) h$ . By [L3], applied at each point with $H = h$ , the field $h^{'}$ is positive definite and smooth and satisfies $∣ d f ∣_{h^{'}} \leq 1$ everywhere. This proves (b).

3.1step 2.1L5givenalgebra

(The proper function is $1$ -Lipschitz for $h^{'}$ .) Let $q, q^{'} \in M_{0}$ and let $ε > 0$ . By Riemannian distance on a connected manifold, choose a piecewise- $C^{1}$ curve $γ : [a, b] \to M_{0}$ from $q$ to $q^{'}$ whose $h^{'}$ -length is at most $d_{h^{'}} (q, q^{'}) + ε$ . On each smooth piece, [L5] and Cauchy--Schwarz give $∣ f (γ (v)) - f (γ (u)) ∣ \leq \int_{u}^{v} ∣ d f ∣_{h^{'}} ∣ γ^{'} ∣_{h^{'}} d t \leq L_{h^{'}} (γ ∣_{[u, v]})$ . Summing over the finitely many pieces yields $∣ f (q^{'}) - f (q) ∣ \leq L_{h^{'}} (γ) \leq d_{h^{'}} (q, q^{'}) + ε$ . Letting $ε ↓ 0$ gives $∣ f (q^{'}) - f (q) ∣ \leq d_{h^{'}} (q, q^{'})$ .

4.1step 3.1L4L6L7given

(Completeness.) Let $(x_{k})$ be a Cauchy sequence in $(M_{0}, d_{h^{'}})$ . There is $k_{0}$ with $d_{h^{'}} (x_{k}, x_{k_{0}}) \leq 1$ for all $k \geq k_{0}$ ; by step 3.1, $f (x_{k}) \leq f (x_{k_{0}}) + 1$ for those $k$ , so the tail lies in the closed sublevel $K : = f^{- 1} ([0, f (x_{k_{0}}) + 1])$ . The set $K$ is compact in $M$ by [L4]. Every connected component is closed (the closure of a connected set is connected), so $K_{0} : = K \cap M_{0}$ is compact in $M_{0}$ and contains the tail. By [L7] that tail has a subsequence converging in $K_{0}$ ; the limit is a manifold-topology limit and therefore a $d_{h^{'}}$ -limit by [L6]. Since $(x_{k})$ is Cauchy, the whole sequence converges to the same limit. Hence $(M_{0}, d_{h^{'}})$ is complete, which is (c).

5.1step 4.1L8given

(Clause (d).) Apply [L8] to the connected Riemannian manifold $(M_{0}, h^{'} ∣_{M_{0}})$ , which is complete by step 4.1: every closed $d_{h^{'}}$ -bounded subset of $M_{0}$ is compact, and every closed ball is compact. This proves (d).

6.1step 1.1step 2.1step 3.1step 4.1step 5.1step 1.2∎

(Conclusion.) Steps 1.1-5.1 prove (a)-(d), and step 1.2 establishes the locally absolutely continuous length convention stated above.

Remarks

Choice. The countable choice assumption is inherited from the proper-exhaustion theorem and Hopf-Rinow and is used only there; the metric $h$ itself is pointwise algebra, and the additional length assertion uses Dependent Choice through its fundamental-theorem supplier.
Why $h$ and not just some Riemannian metric. The particular combination $g + 2 n^{♭} \otimes n^{♭}$ has the additional property, recorded in Equivalence of the absolutely-continuous and continuous causal conventions, and one-sided inextendible extensions and used in the limit-curve arguments, that $h (X, X) \geq 1$ for every $g$ -unit future timelike $X$ ; this is what makes the arclength depth of prepended geodesics controlled without completeness assumptions on $g$ .
Scope. The theorem is a global existence statement about one auxiliary Riemannian metric on the smooth Lorentzian model; it asserts no completeness of $g$ , no geodesic completeness and no physical conclusion.

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

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources