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.

Local Birkhoff theorem: a vacuum warped product with a round sphere factor is locally Schwarzschild with an extra Killing field

Statement

Let $V \subseteq R^{2}$ be a connected nonempty open set with global coordinates $y$ , let $(q_{A B})$ be a smooth symmetric matrix of functions on $V$ with $D_{q} : = \det (q_{A B}) < 0$ everywhere, let $r : V \to (0, \infty)$ be smooth and let $z = \sum_{A, B} q^{A B} \partial_{A} r \partial_{B} r$ be nonzero everywhere; let $M = V \times S^{2}$ and let $g$ be the warped metric of The warped product of a two-dimensional Lorentzian base with a round sphere: Christoffel symbols and Ricci tensor, whose Ricci tensor is given there in clause (c) by ${Ric}_{A B} = Ric (q)_{A B} - (2 / r) {Hess}_{A B} r$ , ${Ric}_{A i} = 0$ , ${Ric}_{i j} = (1 - z - r Δ_{q} r) γ_{i j}$ . Assume the vacuum condition

$Ric (g) = 0 on M,$

that is, the vanishing of all components of the Ricci tensor of $g$ in every product chart. Then:

(a) Mass parameter. There is a constant $s \in R$ such that $z = 1 - \frac{s}{r}$ on $V$ ; equivalently $r (1 - z) = s$ .

(b) Local Schwarzschild coordinates. For every $p \in V$ there are an open neighborhood $W \subseteq V$ of $p$ and a smooth function $T : W \to R$ such that $(T, r)$ is a smooth coordinate system on $W$ , the vector field $\partial_{T}$ coincides on $W$ with the volume-form field $K$ of Two-dimensional base identities for the warped spherical metric: pure-trace Ricci, the vacuum reduction and the extra Killing field, and in these coordinates

$q = - (1 - \frac{s}{r}) d T \otimes d T + (1 - \frac{s}{r})^{- 1} d r \otimes d r on W,$

where $(1 - s / r)^{- 1}$ is the smooth function $1 / z$ on $W$ .

(c) Local Schwarzschild form of the metric. In the product chart $(T, r, ϑ, φ)$ over $W \times S^{2}$ the components of $g$ are

$g_{T T} = - (1 - \frac{s}{r}), g_{r r} = (1 - \frac{s}{r})^{- 1}, g_{ϑ ϑ} = r^{2}, g_{φ φ} = r^{2} \sin^{2} ϑ,$

with all mixed components zero; that is, $g = - (1 - \frac{s}{r}) d T \otimes d T + (1 - \frac{s}{r})^{- 1} d r \otimes d r + r^{2} γ_{S^{2}}$ on the chart domain.

(d) Extra Killing field. $\partial_{T} = K$ is a Killing field of $g$ on the chart domain in the sense of Killing fields of a Lorentzian metric; it satisfies $\partial_{T} (r) = 0$ and $g (\partial_{T}, \partial_{T}) = - z = - (1 - s / r)$ . On a subregion where $z > 0$ , this field is timelike and orthogonal to the hypersurfaces $T = c o n s t a n t$ ; this is the local staticity asserted here. Where $z < 0$ , it is spacelike and no staticity is asserted. In either case it is an additional symmetry not assumed among the hypotheses.

(e) Scope. The statement is local in $V$ : a neighborhood of each point is produced, and $s$ is a constant on the connected set $V$ but need not be positive, need not be the same for a different connected component of a larger region, and no asymptotic flatness, regular-center, completeness, maximality or global uniqueness statement is made. The hypotheses $D_{q} < 0$ and $z \neq 0$ are exactly those of the two quoted lemmas, and $r > 0$ is used to divide by $r$ .

Facts & Assumptions

Given: A connected open set $V \subseteq R^{2}$ , a smooth symmetric matrix $q_{A B}$ with $\det q < 0$ , a smooth $r : V \to (0, \infty)$ with $z \neq 0$ everywhere, the warped metric $g$ on $M = V \times S^{2}$ in product charts, and the vacuum condition $Ric (g) = 0$ .

[L1]

The functions $Γ^{A}_{B C}$ , ${Hess}_{A B} r$ , $Δ_{q} r$ , $z$ , $R^{A}_{B C D}$ , $Ric (q)_{A B}$ are those of The warped product of a two-dimensional Lorentzian base with a round sphere: Christoffel symbols and Ricci tensor, where clause (c) gives the Ricci components of $g$ in every product chart; the components of a smooth tensor field vanish identically if they vanish in every chart of an atlas (Smooth covariant 2-tensor fields on a smooth manifold, Chart independence and the transformation law of a smooth covariant 2-tensor field).

[L2]

Under the hypotheses of the statement, Two-dimensional base identities for the warped spherical metric: pure-trace Ricci, the vacuum reduction and the extra Killing field applies to the two equations ${Ric}_{A B} = 0$ and ${Ric}_{i j} = 0$ , and its clauses (c)-(e) give the constant $s$ with $z = 1 - s / r$ , the volume-form field $K$ with $K \neq 0$ , $K (r) = 0$ , $K$ pointwise independent of $\nabla r$ , the Killing property $\nabla_{A} K_{B} + \nabla_{B} K_{A} = 0$ and the component formulas $K^{0} = - \partial_{1} r / λ$ , $K^{1} = \partial_{0} r / λ$ with $λ = \sqrt{- D_{q}}$ .

[L3]

The flow-box theorem applies to the smooth vector field $K$ on the smooth surface $V$ : at every point $p$ with $K_{p} \neq 0$ there are coordinates $(u^{1}, u^{2})$ on a neighborhood of $p$ in which $K = \partial_{u^{1}}$ (The flow-box theorem, A smooth vector field is a smooth section of the tangent bundle).

[L4]

In a chart, coordinate derivations form a basis of each tangent space, and a list of $n$ smooth functions on an $n$ -manifold is a coordinate system near a point when its Jacobian determinant is nonzero there (Coordinate derivations form a basis of the tangent space, $C^{r}$ and smooth maps between smooth manifolds, Choice-free smooth inverse function theorem in Euclidean space, with $n = 2$ in the chart domain).

[L5]

Smoothness, the chain and product rules, the inverse of an invertible $2 \times 2$ matrix and the fact that a smooth function of one variable with nonzero derivative is a local coordinate are available (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, 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)$ , Invertible matrices and the general linear group ${GL}_{n} (F)$ , Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, Choice-free smooth inverse function theorem in Euclidean space). On a connected open real interval, a smooth function with zero derivative is constant (A differentiable map on a connected open Euclidean set has zero derivative exactly when it is constant, $m = q = 1$ ).

[L6]

A smooth function on a real interval has the primitive $H (r) = \int_{r_{0}}^{r} h (u) d u$ with derivative $H^{'} = h$ (The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ , The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive).

Proof

technique · read the two vacuum equations off the warped Ricci formula, invoke the base reduction for the constant $s$ and the Killing field $K$, straighten $K$ by the flow-box theorem, use $K(r)=0$ to make $(T,r)$ coordinates, remove the cross term, and read off the metric and the Killing property

1.1L1givenalgebra

(Vacuum equations in warped form.) By [L1] the components of $Ric (g)$ in a product chart are those displayed in the statement; the vacuum condition therefore gives $Ric (q)_{A B} = (2 / r) {Hess}_{A B} r$ and $1 - z - r Δ_{q} r = 0$ on $V$ , since $γ_{i j}$ is a nondegenerate matrix and $r > 0$ .

2.1step 1.1L2given

(The constant $s$ .) The hypotheses of Two-dimensional base identities for the warped spherical metric: pure-trace Ricci, the vacuum reduction and the extra Killing field are exactly the connectedness of $V$ , $D_{q} < 0$ , $r > 0$ , $z \neq 0$ and the two equations of step 1.1, so its clause (c) gives a constant $s \in R$ with $r (1 - z) = s$ , that is, $z = 1 - s / r$ ; this is (a).

3.1step 2.1L2L3L4L5algebra

(Coordinates adapted to $K$ .) By [L2], $K$ is a nonvanishing smooth field, so [L3] supplies a flow-box chart $(u^{1}, u^{2})$ near $p$ with $K = \partial_{u^{1}}$ . In this chart the smooth map $F (u^{1}, u^{2}) = (u^{1}, r (u^{1}, u^{2}))$ has derivative matrix $(\begin{array}{cc} 1 & 0 \\ 0 & \partial_{u^{2}} r \end{array})$ , since $\partial_{u^{1}} r = K (r) = 0$ . Its determinant is nonzero: otherwise $d r$ would vanish, contrary to $z \neq 0$ . Apply the smooth Euclidean inverse-function theorem [L4] at $p$ to obtain an open neighborhood $W$ with coordinates $(T, r) = (u^{1}, r)$ . The identities $K (T) = 1$ and $K (r) = 0$ show $K = \partial_{T}$ there.

4.1step 2.1step 3.1L2L5L6algebra

(The base metric in coordinates adapted to $K$ .) In the coordinates $(T, r)$ from step 3.1, $K = \partial_{T}$ and $q_{T T} = q (K, K) = - z$ by [L2]. Since $K$ is Killing, $L_{\partial_{T}} q = 0$ , so the coordinate components $q_{T T}, q_{T r}, q_{r r}$ are independent of $T$ . After shrinking $W$ to a coordinate rectangle, write $E (r) = q_{T T}$ and $F (r) = q_{T r}$ . The assumption $z \neq 0$ gives $E = - z \neq 0$ . Define locally $H (r) : = \int_{r_{0}}^{r} \frac{F (u)}{E (u)} d u .$ The integrand is smooth, and [L6] gives $H^{'} = F / E$ . Replace the time coordinate by $\hat{T} = T + H (r)$ , leaving $r$ fixed; because the old coordinate is $T = \hat{T} - H (r)$ , the new cross coefficient is $F - E H^{'} = 0$ , while $\partial_{\hat{T}} = \partial_{T} = K$ and $q_{\hat{T} \hat{T}} = E = - z$ . In these diagonal coordinates $z = q^{r r} = 1 / q_{r r}$ by its definition, so $q_{r r} = 1 / z$ . Substituting $z = 1 - s / r$ from step 2.1 gives $q = - (1 - \frac{s}{r}) d \hat{T} \otimes d \hat{T} + (1 - \frac{s}{r})^{- 1} d r \otimes d r$ . Renaming $\hat{T}$ as $T$ proves (b).

5.1step 3.1step 4.1L1L2algebra

(The metric and the Killing field.) In the product chart $(T, r, ϑ, φ)$ the components of $g$ are $g_{T T} = q_{T T}$ , $g_{r r} = q_{r r}$ , $g_{ϑ ϑ} = r^{2}$ , $g_{φ φ} = r^{2} \sin^{2} ϑ$ and all mixed components zero, by the definition of $g$ in The warped product of a two-dimensional Lorentzian base with a round sphere: Christoffel symbols and Ricci tensor; substituting step 4.1 gives (c). After shrinking to a connected coordinate rectangle, $z$ has a constant nonzero sign. On this product domain choose $N = \partial_{T}$ when $z > 0$ and $N = \partial_{r}$ when $z < 0$ ; its squared norm is respectively $- z < 0$ or $1 / z < 0$ , so the time-oriented domain required by Killing fields of a Lorentzian metric is available. Every displayed component is independent of $T$ , and $\partial_{T}$ has components $(1, 0, 0, 0)$ in this chart, so the Lie derivative $L_{\partial_{T}} g$ has all components $\partial_{T} g_{a b} = 0$ and vanishes; by [L2] we also know $K$ is a Killing field of $q$ with $K (r) = 0$ and $q (K, K) = - z$ , and $\partial_{T} = K$ by step 3.1, so $\partial_{T} (r) = 0$ and $g (\partial_{T}, \partial_{T}) = - z = - (1 - s / r)$ . This proves (d).

6.1step 2.1step 4.1step 5.1given∎

(Conclusion.) Step 2.1 proves (a), step 4.1 proves (b), step 5.1 proves (c) and (d); clause (e) records the local scope, the role of the hypotheses and the fact that $s$ is constant only on the connected set $V$ .

Remarks

What the theorem does and does not say. It converts the two-component vacuum condition on a warped chart into the local Schwarzschild form and an extra local Killing symmetry; it does not assert that every vacuum solution is spherically symmetric, that the region is an exterior region, that $s > 0$ , or that the coordinates extend beyond $W$ . The hypothesis $z \neq 0$ excludes every point with $r = s$ ; because $V$ is connected and $r - s$ is continuous, a region satisfying it lies wholly on one side of that level. It does not merely exclude a chart on which $r$ is constantly $s$ .
Relation to the global sources. The cited treatments derive the same conclusion under stronger global or static hypotheses and in coordinates adapted to the spherical symmetry; the version proved here is the local warped-product statement, with all hypotheses displayed, and it is the form used by the spherical vacuum model of this page.

Local Birkhoff theorem: a vacuum warped product with a round sphere factor is locally Schwarzschild with an extra Killing field

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources