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 cone, the escape horizon and decreasing areal radius in the Kruskal model

Statement

Let $(K, r, g_{K}, N_{K})$ be the Kruskal model datum of mass parameter $m_{*} > 0$ with Schwarzschild radius $s = 2 G_{N} m_{*} / c^{2} > 0$ (The Kruskal model datum: domain, implicit radial function, metric and time orientation, Kruskal model properties: smooth radial function, Lorentzian metric, four-region isometries, vacuum and Kretschmann scalar), let $(U, V, ξ^{2}, ξ^{3})$ be any Kruskal product chart, and let $γ_{i j}$ be the round-sphere components in its angular chart. In a spherical-polar Kruskal chart, $(ξ^{2}, ξ^{3}) = (ϑ, φ)$ and $γ_{i j} = diag (1, \sin^{2} ϑ)$ . Define $A : K \to (0, \infty)$ by

$A : = \frac{4 s^{3} e^{- r / s}}{r},$

so that in a product chart $g_{U V} = g_{V U} = - A / 2$ , $g_{i j} = r^{2} γ_{i j}$ and the mixed base-angular components vanish. In a spherical-polar chart this reads $g_{ϑ ϑ} = r^{2}$ , $g_{φ φ} = r^{2} \sin^{2} ϑ$ . For a $C^{1}$ curve $η : J \to K$ with $J$ a nonempty interval write $\dot{η} = (\dot{U}, \dot{V}, {\dot{ξ}}^{2}, {\dot{ξ}}^{3})$ for its coordinate components, and call $η$ future-directed causal when $g_{K} (\dot{η}, \dot{η}) \leq 0$ and $g_{K} (\dot{η}, N_{K}) < 0$ at every parameter value. Then:

(a) Causal cone criterion. At every $p \in K$ and for every $X \in T_{p} K$ with chart components $(X^{U}, X^{V}, X^{ω})$ one has: $X$ is causal and future-directed if and only if

$X^{U} \geq 0, X^{V} \geq 0, X^{U} + X^{V} > 0, A (p) X^{U} X^{V} \geq r (p)^{2} γ_{p} (X^{ω}, X^{ω}),$

where $γ_{p} (X^{ω}, X^{ω})$ is the round-sphere squared norm of the angular part. In particular every future-directed causal tangent has both $X^{U} \geq 0$ and $X^{V} \geq 0$ .

(b) Monotonicity. Along every future-directed causal $C^{1}$ curve the functions $U$ and $V$ are nondecreasing, and along every past-directed causal $C^{1}$ curve (where $g (\dot{η}, \dot{η}) \leq 0$ and $g (\dot{η}, N_{K}) > 0$ ) they are nonincreasing.

(c) Radial null geodesics and their affine parameters. For every $(U_{0}, V_{0}, ω_{0}) \in K$ there is a unique maximal solution $λ \mapsto (U (λ), V_{0}, ω_{0})$ of $\frac{d U}{d λ} = \frac{1}{A (U (λ), V_{0})}$ , $U (0) = U_{0}$ ; it is an affinely parametrized null geodesic of $g_{K}$ with $g (\dot{η}, \dot{η}) = 0$ . The same holds for $λ \mapsto (U_{0}, V (λ), ω_{0})$ with $\frac{d V}{d λ} = \frac{1}{A (U_{0}, V (λ))}$ . Both are future-directed, and $λ$ increases strictly with $U$ , respectively with $V$ , because $A > 0$ . Moreover $\partial_{U} r = - \frac{s^{2} V e^{- r / s}}{r}$ and $\partial_{V} r = - \frac{s^{2} U e^{- r / s}}{r}$ at every point of $K$ .

(d) Escape horizon. Call a future-directed causal $C^{1}$ curve $η$ escaping to the right exterior when there is a parameter value after which $η$ stays in the open quadrant ${U < 0, V > 0}$ and $r (η (t)) \to + \infty$ as $t \to + \infty$ (a point with $U \geq 0$ cannot reach the quadrant ${U < 0, V > 0}$ at all, by (b), and this is the sense in which the horizon is a one-way membrane here). Then:

no future-directed causal curve issued at a point $p$ with $U (p) \geq 0$ escapes to the right exterior;
every point $p$ with $U (p) < 0$ admits such a curve: for $t > 0$ the curve $η_{p} (t) : = (U (p), V (p) + t, ω (p))$ is a future-directed null $C^{1}$ curve, it stays in ${U < 0, V > 0}$ for $t > 1 + ∣ V (p) ∣$ and satisfies $r (η_{p} (t)) \to + \infty$ as $t \to + \infty$ .

Consequently the exact nonescaping set of the datum is ${U \geq 0}$ with boundary the null surface ${U = 0}$ , and the past-directed dual statement singles out ${V = 0}$ as the boundary of the region admitting past-directed escape to the right exterior: here escape means eventual residence in ${U < 0, V > 0}$ with $r \to + \infty$ as the past-directed parameter tends to $+ \infty$ .

(e) Decreasing areal radius. If $U (p) > 0$ and $V (p) > 0$ , then along both future directions of the radial null geodesics of (c) through $p$ the function $r$ is strictly decreasing as their affine parameter $λ$ increases: on $λ \mapsto (U_{0}, V (λ), ω_{0})$ and on $λ \mapsto (U (λ), V_{0}, ω_{0})$ .

(f) Scope. All statements are geometric properties of the smooth Kruskal datum on $K$ ; no maximality, geodesic completeness or uniqueness is claimed, the set ${U V = 1}$ (where $r = 0$ ) is not part of $K$ , and no statement is made about the physical interpretation of any curve. The escape notion of (d) is defined by the displayed conditions on $U, V$ and $r$ and does not presuppose a conformal infinity.

Facts & Assumptions

Given: The Kruskal model datum with $s > 0$ , a Kruskal chart, the function $A = 4 s^{3} e^{- r / s} / r > 0$ , and the component assignments $g_{U V} = g_{V U} = - A / 2$ , $g_{ϑ ϑ} = r^{2}$ , $g_{φ φ} = r^{2} \sin^{2} ϑ$ .

[L1]

$K = {(U, V) : U V < 1} \times S^{2}$ is a smooth four-manifold without boundary; $r : K \to (0, \infty)$ is the unique smooth function with $U V = - (r / s - 1) e^{r / s}$ , the metric $g_{K}$ is smooth Lorentzian of signature $(-, +, +, +)$ , and $N_{K} = \partial_{U} + \partial_{V}$ is a time orientation with $g_{K} (N_{K}, N_{K}) = - A < 0$ (The Kruskal model datum: domain, implicit radial function, metric and time orientation, Kruskal model properties: smooth radial function, Lorentzian metric, four-region isometries, vacuum and Kretschmann scalar clauses (a)-(b)).

[L2]

The metric-selected connection of $g_{K}$ exists, is unique and has Christoffel symbols $Γ^{a}_{b c} = \frac{1}{2} g^{a d} (\partial_{b} g_{d c} + \partial_{c} g_{b d} - \partial_{d} g_{b c})$ in a product chart; a curve is a geodesic with affine parameter $λ$ precisely when its coordinate components satisfy ${\ddot{x}}^{a} + \sum_{b, c} Γ^{a}_{b c} {\dot{x}}^{b} {\dot{x}}^{c} = 0$ (Existence and uniqueness of the metric-selected connection of a nondegenerate metric, and its extension to tensor fields, Metric compatibility, torsion freedom and the metric-selected connection class, Christoffel symbols of an affine connection, Geodesic of an affine connection, Coordinate geodesic equation).

[L3]

A nonzero tangent vector $X$ is causal when $g_{K} (X, X) \leq 0$ , future-directed when $g_{K} (X, N_{K}) < 0$ and past-directed when $g_{K} (X, N_{K}) > 0$ (Timelike, null, spacelike and causal vectors of a Lorentz vector space, Time orientation, future and past timelike/null/causal vectors, and the closed cones, Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model).

[L4]

The inverse of the $2 \times 2$ block $(\begin{array}{cc} 0 & - A / 2 \\ - A / 2 & 0 \end{array})$ is $(\begin{array}{cc} 0 & - 2 / A \\ - 2 / A & 0 \end{array})$ , and the inverse metric has no mixed $U$ -angular or $V$ -angular entries; the round metric is positive definite on the angular directions (Kruskal model properties: smooth radial function, Lorentzian metric, four-region isometries, vacuum and Kretschmann scalar, The round metric on the sphere as an induced metric).

[L5]

The function $F (r) : = (1 - r / s) e^{r / s}$ satisfies $F^{'} (r) = - (r / s^{2}) e^{r / s} < 0$ on $r > 0$ and is a smooth strictly decreasing bijection onto $(- \infty, 1)$ with smooth inverse; consequently $U V \to - \infty$ holds exactly when $r \to + \infty$ , and implicit differentiation of $U V = F (r)$ gives $\partial_{U} r = - s^{2} V e^{- r / s} / r$ , $\partial_{V} r = - s^{2} U e^{- r / s} / r$ (Kruskal model properties: smooth radial function, Lorentzian metric, four-region isometries, vacuum and Kretschmann scalar clause (a), Choice-free smooth inverse function theorem in Euclidean space, The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set, Rational powers $a^{r}$ of a positive base).

[L6]

A $C^{1}$ function on an interval whose derivative is $\geq 0$ everywhere is nondecreasing, and a $C^{1}$ function with derivative $> 0$ is strictly increasing; the chain, product and quotient rules hold (The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set, Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, $C^{r}$ and smooth maps between smooth manifolds).

[L7]

The exponential function is smooth and satisfies $\partial_{r} e^{r / s} = s^{- 1} e^{r / s}$ ; the displayed functions involving $r$ are smooth on $K$ because $r$ is smooth and $r > 0$ (Kruskal model properties: smooth radial function, Lorentzian metric, four-region isometries, vacuum and Kretschmann scalar, The real exponential function and the number $e$ by a power series, The exponential function is smooth and $(\exp)^{'} = \exp$ , Rational powers $a^{r}$ of a positive base, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

technique · evaluate the metric on a general tangent vector to get the cone criterion, compute the Christoffel symbols along the coordinate fields, differentiate the defining relation of $r$, read monotonicity off the sign of the tangent components, and verify the geodesic, escape and trapping claims directly

1.1L1L3L4algebra

(Cone criterion.) Writing $X = X^{U} \partial_{U} + X^{V} \partial_{V} + X^{ω}$ with $X^{ω}$ angular and using the components of [L1], $g_{K} (X, X) = - A X^{U} X^{V} + r^{2} γ (X^{ω}, X^{ω})$ and $g_{K} (N_{K}, X) = g_{K} (\partial_{U} + \partial_{V}, X) = - \frac{A}{2} (X^{U} + X^{V})$ . By [L3] $X$ is causal and future-directed exactly when $- A X^{U} X^{V} + r^{2} γ (X^{ω}, X^{ω}) \leq 0$ and $X^{U} + X^{V} > 0$ . The causal inequality gives $A X^{U} X^{V} \geq r^{2} γ (X^{ω}, X^{ω}) \geq 0$ , hence $X^{U} X^{V} \geq 0$ ; if one of $X^{U}, X^{V}$ were negative the other would be $\leq 0$ and $X^{U} + X^{V} \leq 0$ , contradicting $X^{U} + X^{V} > 0$ , so both are $\geq 0$ and one is positive. Conversely, $X^{U}, X^{V} \geq 0$ with $X^{U} + X^{V} > 0$ and $A X^{U} X^{V} \geq r^{2} γ (X^{ω}, X^{ω})$ give both required inequalities. This proves (a).

1.2L2L4L5L7algebra

(Christoffel symbols along the radial coordinate fields.) The inverse $U, V$ block is $g^{U V} = g^{V U} = - 2 / A$ . Since $g_{U V} = - A / 2$ and $g_{U U} = 0$ , the Christoffel formula of [L2] gives $Γ^{U}_{U U} = \frac{1}{2} g^{U V} (\partial_{U} g_{V U} + \partial_{U} g_{U V}) = (- 2 / A) (- \frac{1}{2} \partial_{U} A) = \partial_{U} A / A$ ; similarly $Γ^{V}_{V V} = \partial_{V} A / A$ . The same substitution gives $Γ^{U}_{V V} = Γ^{V}_{U U} = 0$ , all angular components of $\nabla_{\partial_{U}} \partial_{U}$ and $\nabla_{\partial_{V}} \partial_{V}$ equal zero, and $Γ^{U}_{U V} = Γ^{V}_{U V} = 0$ . Thus $\nabla_{\partial_{U}} \partial_{U} = (\partial_{U} A / A) \partial_{U}$ and $\nabla_{\partial_{V}} \partial_{V} = (\partial_{V} A / A) \partial_{V}$ .

1.3L5algebra

(Radial derivatives of $r$ .) The relation $U V = F (r)$ with $F (r) = (1 - r / s) e^{r / s}$ of [L5] has $F^{'} (r) = - (r / s^{2}) e^{r / s} \neq 0$ on $r > 0$ , so implicit differentiation gives $V = F^{'} (r) \partial_{U} r$ , that is, $\partial_{U} r = - s^{2} V e^{- r / s} / r$ , and $U = F^{'} (r) \partial_{V} r$ , that is, $\partial_{V} r = - s^{2} U e^{- r / s} / r$ . This proves the derivative formulas of (c).

2.1step 1.1L3L6algebra

(Monotonicity.) If $η$ is future-directed causal, then by step 1.1 its tangent has $\dot{U} \geq 0$ and $\dot{V} \geq 0$ at every parameter; by [L6] applied to subintervals, $U \circ η$ and $V \circ η$ are nondecreasing. For past-directed causal curves the same argument with $N_{K}$ replaced by $- N_{K}$ gives $\dot{U} \leq 0$ , $\dot{V} \leq 0$ and hence nonincreasing functions. This proves (b).

2.2step 1.1step 1.2L2L6algebra

(Radial null geodesics and maximality.) The supplier The geodesic initial-value problem and the exponential map of the metric-selected connection gives the unique maximal geodesic through $p$ with initial tangent $A (U_{0}, V_{0})^{- 1} \partial_{U}$ . On the open scalar domain ${U : U V_{0} < 1}$ , the smooth equation $U^{'} = 1 / A (U, V_{0})$ has a unique local solution at every initial value by Picard-Lindelöf local existence and uniqueness for first-order systems. Fixing $V = V_{0}$ and the sphere point, this solution satisfies all geodesic equations: by step 1.2, $U^{''} + Γ^{U}_{U U} (U^{'})^{2} = - A^{- 3} \partial_{U} A + (\partial_{U} A / A) A^{- 2} = 0,$ and all other component equations vanish. Uniqueness makes it agree locally with the maximal geodesic. On the latter's connected parameter interval, the set where $V = V_{0}$ , the sphere point is $ω_{0}$ , $V^{'} = 0$ , the angular tangent vanishes, and $U^{'} = 1 / A (U, V_{0})$ is nonempty, closed by continuity, and open by this same local construction and geodesic uniqueness. Thus the conditions hold throughout that interval. This yields a scalar solution on the whole maximal geodesic domain. Conversely, any scalar extension would give a geodesic extension by the verified equations, contradicting maximality; hence the scalar and geodesic domains are both maximal. The curve is null because $g (\partial_{U}, \partial_{U}) = 0$ , future-directed by step 1.1, and its affine parameter $λ$ increases with $U$ because $1 / A > 0$ . Exchanging $U, V$ proves the second family, in any angular chart including pole charts.

3.1step 1.3step 2.2L5L6algebra

(Decreasing radius in the interior quadrant.) If $U (p) > 0$ and $V (p) > 0$ , then step 1.3 gives $\partial_{V} r = - s^{2} U e^{- r / s} / r < 0$ and $\partial_{U} r = - s^{2} V e^{- r / s} / r < 0$ at $p$ ; along either future branch, the varying coordinate is nondecreasing from its positive initial value and the other coordinate remains fixed and positive; hence both remain positive throughout that future branch. The derivative formulas therefore stay strictly negative, so by [L6], $r$ is strictly decreasing along the geodesics of step 2.2 through $p$ in the directions of increasing $V$ , respectively increasing $U$ , which are the future directions in the affine parameters of step 2.2. This proves (e).

3.2step 1.1step 2.1L1L5algebra

(Escape and nonescape.) Let $η$ be future-directed causal with $U (η (0)) = U (p) \geq 0$ . By step 2.1, $U \circ η \geq U (p) \geq 0$ ; hence $η$ never enters the quadrant ${U < 0, V > 0}$ and cannot escape to the right exterior, proving (d)1. Conversely let $U (p) < 0$ and consider $η_{p} (t) : = (U (p), V (p) + t, ω (p))$ for $t > 0$ . Since $U (p) < 0$ , its product $U (p) (V (p) + t)$ decreases from a value below $1$ and remains below $1$ , so this $C^{1}$ curve stays in $K$ for all $t > 0$ . Its tangent is $(0, 1, 0, 0)$ ; by step 1.1 it is future-directed null. Since $U$ is constant and negative, the curve is in ${U < 0}$ , and for $t > 1 + ∣ V (p) ∣$ it is in ${U < 0, V > 0}$ . Along it $U V = U (p) (V (p) + t) \to - \infty$ , so by [L5] $r \to + \infty$ . This proves (d)2 and identifies the nonescaping set as ${U \geq 0}$ with boundary ${U = 0}$ , a null surface because $\partial_{V}$ is null there. For the past-directed dual, $V$ is nonincreasing, so no point with $V \leq 0$ can enter the right exterior. If $V (p) > 0$ , the past-directed null curve $(U (p) - t, V (p), ω (p))$ , $t \geq 0$ , stays in $K$ , eventually enters the right exterior and has $U V \to - \infty$ , hence $r \to + \infty$ . Thus its admitting region is exactly ${V > 0}$ , with boundary ${V = 0}$ , whose null generator is $\partial_{U}$ .

4.1step 1.1step 1.3step 2.1step 2.2step 3.1step 3.2given∎

(Conclusion.) Step 1.1 proves (a), step 2.1 proves (b), steps 1.3 and 2.2 prove (c), step 3.1 proves (e), and step 3.2 proves (d). Clause (f) records that all statements are geometric, that maximality and completeness are not claimed and that the escape notion is the explicit one of the statement.

Remarks

One-way membrane, not a singularity. The nonescape statement uses only $\dot{U} \geq 0, \dot{V} \geq 0$ along future causal curves; the metric and its curvature remain smooth at $U = 0$ by the Kruskal properties lemma of this page, so the horizon's one-way character is a global causal property of the smooth model, not a defect of the metric at the surface.
Trapping without the expansion machinery. Clause (e) states the strictly decreasing areal radius along both future radial null directions at points with $U, V > 0$ , which is the geometric content of the statement that the spheres $r =$ const in that quadrant are future-trapping; the phrase of the sources is not used as a definition, since the expansion of a null congruence is not defined on this page.

The causal cone, the escape horizon and decreasing areal radius in the Kruskal model

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources