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 warped product of a two-dimensional Lorentzian base with a round sphere: Christoffel symbols and Ricci tensor

Statement

Let $V \subseteq R^{2}$ be a nonempty open set with global coordinates $y = (y^{0}, y^{1})$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, $C^{r}$ and smooth maps between smooth manifolds), let $(q_{A B})$ be a smooth symmetric $2 \times 2$ matrix of functions on $V$ with

$Δ_{q} (y) : = \det (q_{A B} (y)) < 0 (y \in V),$

so that $q$ is a smooth symmetric covariant $2$ -tensor field on $V$ whose value at every point is nondegenerate with inertia $(1, 1, 0)$ (Smooth covariant 2-tensor fields on a smooth manifold, Lorentz forms of inertia (3,1,0) on a 4-dimensional real vector space), and let $r : V \to (0, \infty)$ be a smooth function. Indices $A, B, C, D$ run over ${0, 1}$ and indices $i, j, k, l$ over the sphere directions below. Define on $V$ :

$(q^{A B}) : = (q_{A B})^{- 1}, Γ^{A}_{B C} : = \frac{1}{2} \sum_{D} q^{A D} (\partial_{B} q_{D C} + \partial_{C} q_{B D} - \partial_{D} q_{B C}),$

${Hess}_{A B} r : = \partial_{A} \partial_{B} r - \sum_{C} Γ^{C}_{A B} \partial_{C} r, Δ_{q} r : = \sum_{A, B} q^{A B} {Hess}_{A B} r, z : = \sum_{A, B} q^{A B} \partial_{A} r \partial_{B} r .$

Further define

$R^{A}_{B C D} : = \partial_{C} Γ^{A}_{D B} - \partial_{D} Γ^{A}_{C B} + \sum_{E} (Γ^{A}_{C E} Γ^{E}_{D B} - Γ^{A}_{D E} Γ^{E}_{C B}), R_{A B C D} : = \sum_{E} q_{A E} R^{E}_{B C D},$

$Ric (q)_{B D} : = \sum_{A, C} q^{A C} R_{A B C D}, S_{q} : = \sum_{B, D} q^{B D} Ric (q)_{B D} .$

Let $S^{2} : = {y \in R^{3} : ∥ y ∥_{2} = 1}$ be the unit Euclidean sphere with its induced smooth structure and round metric $γ_{S^{2}}$ (Euclidean spheres and closed balls as subspaces of $R^{n}$ , The round metric on the sphere as an induced metric), let $M : = V \times S^{2}$ carry the product smooth structure (Products of smooth manifolds have a canonical product smooth structure), and let $π : M \to V$ and $ι : M \to S^{2}$ be the projections. Define the global symmetric covariant $2$ -tensor

$g : = π^{*} q + r^{2} ι^{*} γ_{S^{2}}$

on $M$ , where $r$ in this formula is pulled back from $V$ . In any product chart $(y^{0}, y^{1}, ξ^{2}, ξ^{3})$ , let $γ_{i j}$ be the round-metric components of the angular chart. The components of $g$ are

$g_{A B} : = q_{A B}, g_{A i} : = 0, g_{i j} : = r^{2} γ_{i j} (A, B \in {0, 1}, i, j \in {2, 3}),$

Then:

(a) The metric. The global pullback formula defines a smooth symmetric covariant $2$ -tensor field $g$ on $M$ ; at every point it is nondegenerate with inertia $(3, 1, 0)$ , so $(M, g)$ is a smooth Lorentzian four-manifold of signature $(-, +, +, +)$ (Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model).

(b) Christoffel symbols. Let $\nabla$ be the metric-selected connection of $g$ , unique by Existence and uniqueness of the metric-selected connection of a nondegenerate metric, and its extension to tensor fields clause (b) (Metric compatibility, torsion freedom and the metric-selected connection class), and let $Γ^{μ}_{ν ρ}$ be its Christoffel symbols in a product chart. Then the only nonzero symbols, beyond the displayed lower-index symmetry $Γ^{μ}_{ν ρ} = Γ^{μ}_{ρ ν}$ , are

$Γ^{A}_{B C} of the first display, Γ^{i}_{A j} = \frac{\partial_{A} r}{r} δ^{i}_{j}, Γ^{A}_{i j} = - r q^{A B} \partial_{B} r γ_{i j}, Γ^{i}_{j k} the round-sphere symbols in the chosen chart,$

In a spherical-polar chart these are $Γ^{2}_{33} = - \sin ϑ \cos ϑ$ and $Γ^{3}_{23} = Γ^{3}_{32} = \cot ϑ$ , with all other $Γ^{i}_{j k}$ vanishing. Pole charts use their own round-metric symbols.

(c) Ricci tensor. With $Ric$ the Ricci tensor of $\nabla$ (The Riemann curvature operator and the derived Ricci, scalar and Einstein tensors clause (c)), in every product chart

${Ric}_{A B} = Ric (q)_{A B} - \frac{2}{r} {Hess}_{A B} r, {Ric}_{A i} = 0, {Ric}_{i j} = (1 - z - r Δ_{q} r) γ_{i j} .$

(d) Scope. The statements are identities of the displayed component functions in product charts and use no field equation, no vacuum condition and no sign or positivity assumption on $s$ ; nothing is asserted about completeness, geodesics, extensions or the physical reading of the coordinates. The hypothesis $Δ_{q} < 0$ is used for nondegeneracy and inertia of $g$ ; it is the only signature input.

Facts & Assumptions

Given: An open set $V \subseteq R^{2}$ , a smooth symmetric matrix $q_{A B}$ with $\det q < 0$ on $V$ , a smooth $r : V \to (0, \infty)$ , the product manifold $M = V \times S^{2}$ , the assigned components $g_{A B} = q_{A B}$ , $g_{A i} = 0$ , $g_{i j} = r^{2} γ_{i j}$ in product charts, and the auxiliary functions of the statement.

[L1]

A smooth symmetric covariant $2$ -tensor field on a smooth manifold is a family of smooth bilinear forms whose chart components transform by the covariant $2$ -tensor law on overlaps (Smooth covariant 2-tensor fields on a smooth manifold, Chart independence and the transformation law of a smooth covariant 2-tensor field, Tensor fields of type (r,s) on a Lorentzian four-manifold and their components).

[L2]

The product $M = V \times S^{2}$ with the product smooth structure is a smooth four-manifold without boundary; its projections are smooth and product charts cover $M$ , including charts about the two poles. On the dense regular angular locus the polar round-metric components are $γ_{22} = 1$ , $γ_{23} = γ_{32} = 0$ , $γ_{33} = \sin^{2} ϑ$ ; in every sphere chart the components transform as a $(0, 2)$ -tensor (Products of smooth manifolds have a canonical product smooth structure, Smooth manifolds and their smooth charts, Euclidean spheres and closed balls as subspaces of $R^{n}$ , The round metric on the sphere as an induced metric).

[L3]

The Levi-Civita theorem for a smooth four-manifold with a smooth nondegenerate symmetric covariant $2$ -tensor field supplies the unique metric-selected connection and its 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 every chart (Existence and uniqueness of the metric-selected connection of a nondegenerate metric, and its extension to tensor fields clauses (a)-(b), Metric compatibility, torsion freedom and the metric-selected connection class, Christoffel symbols of an affine connection).

[L4]

Sums, products, quotients, powers and compositions of smooth functions are smooth and satisfy the usual derivative rules; $r > 0$ on $V$ and $\sin ϑ > 0$ on the polar-chart domain $0 < ϑ < π$ ( $C^{r}$ and smooth maps between smooth manifolds, 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, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, Rational powers $a^{r}$ of a positive base).

[L5]

The inverse of the block matrix $diag (q_{A B}, r^{2} γ_{i j})$ is the block matrix $diag (q^{A B}, r^{- 2} γ^{i j})$ with $γ^{i j}$ the inverse of the round metric; the components of the Ricci tensor are those of The Riemann curvature operator and the derived Ricci, scalar and Einstein tensors clause (c) with components $R^{a}_{b c d}$ of clause (b) and the coordinate formula of Tensoriality of the curvature, its coordinate formula and its point-normal metric formula clause (b), applied on the locally time-oriented restrictions constructed in step 3.1 (The inverse metric, musical isomorphisms and index raising, The Riemann curvature operator and the derived Ricci, scalar and Einstein tensors, Tensoriality of the curvature, its coordinate formula and its point-normal metric formula).

[L6]

The coordinate derivations $\partial_{a}$ form a basis of each tangent space in a chart, the Christoffel symbols are those functions with $\nabla_{\partial_{b}} \partial_{c} = \sum_{a} Γ^{a}_{b c} \partial_{a}$ , and all index sums in the displays are finite (Coordinate derivations form a basis of the tangent space, Christoffel symbols of an affine connection, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

technique · define the warped metric globally with the round-metric pullback, compute in local sphere charts (using polar coordinates for the explicit Ricci calculation), and extend the smooth tensor identities to the poles by continuity

1.1L1L2L4given

(Global smooth tensor.) The product projection $π : M \to V$ and sphere projection $ι : M \to S^{2}$ are smooth by [L2]. Thus $π^{*} q + r^{2} ι^{*} γ_{S^{2}}$ is a globally defined smooth symmetric covariant $2$ -tensor field; its product-chart components are exactly $g_{A B} = q_{A B}$ , $g_{A i} = 0$ , $g_{i j} = r^{2} γ_{i j}$ . This proves the global tensor assertion, including the pole charts.

1.2L2L4L5givenalgebra

(Preliminary identities.) On $V$ , differentiating $\sum_{B} q^{A B} q_{B C} = δ^{A}_{C}$ gives $\partial_{D} q^{A B} = - \sum_{E, F} q^{A E} q^{B F} \partial_{D} q_{E F}$ , and substituting the definition of $Γ^{A}_{B C}$ shows that the identity $\partial_{C} q_{A B} = \sum_{D} (Γ^{D}_{C A} q_{D B} + Γ^{D}_{C B} q_{A D})$ holds, because its right-hand side equals $\frac{1}{2} (\partial_{C} q_{A B} + \partial_{A} q_{C B} - \partial_{B} q_{C A}) + \frac{1}{2} (\partial_{C} q_{B A} + \partial_{B} q_{C A} - \partial_{A} q_{C B}) = \partial_{C} q_{A B}$ ; moreover $\partial_{C} (r^{2} γ_{i j}) = 2 r \partial_{C} r γ_{i j}$ , and the inverse-metric block $diag (q^{A B}, r^{- 2} γ^{i j})$ has no mixed entries.

2.1L2L3L5L6step 1.1givenalgebra

(Nondegeneracy and inertia.) At a point $(y, ω) \in M$ the coordinate derivations form a basis of the tangent space by [L6], and the matrix of $g$ in the product chart frame is block diagonal with the $2 \times 2$ block $q_{A B} (y)$ and the $2 \times 2$ block $r (y)^{2} γ_{i j} (ω)$ . The first block has determinant $Δ_{q} (y) < 0$ , hence two eigenvalues of opposite signs and no zero eigenvalue; the second block is positive definite because $r (y)^{2} > 0$ and the round metric is positive definite. Accordingly $g$ has one negative and three positive eigenvalues, that is, inertia $(3, 1, 0)$ , and is nondegenerate, so by [L3] its metric-selected connection exists and is unique.

2.2L3L4step 1.2algebra

(Base-type symbols.) In the Christoffel formula of [L3] with all three indices $A, B, C \in {0, 1}$ , all entries $g_{A B} = q_{A B}$ are independent of the angular coordinates and $g_{A i} = 0$ , so the formula reduces to $Γ^{A}_{B C} = \frac{1}{2} q^{A D} (\partial_{B} q_{D C} + \partial_{C} q_{B D} - \partial_{D} q_{B C})$ , the displayed base symbols. If exactly one lower index is angular, then either the differentiations produce only $g_{A i} = 0$ terms or the angular derivative annihilates the base block, and the resulting expression vanishes; this gives $Γ^{A}_{B i} = 0$ and $Γ^{i}_{A B} = 0$ .

2.3L3L4step 1.2algebra

(Mixed and sphere-type symbols.) With both lower indices angular, the formula gives $Γ^{A}_{i j} = \frac{1}{2} g^{A D} (\partial_{i} g_{D j} + \partial_{j} g_{D i} - \partial_{D} g_{i j}) = - \frac{1}{2} q^{A D} \partial_{D} (r^{2} γ_{i j}) = - r q^{A D} \partial_{D} r γ_{i j}$ , using $g_{A i} = 0$ , $\partial_{i} g_{A B} = 0$ and step 1.2. With one lower index angular and one base, $Γ^{i}_{A j} = \frac{1}{2} g^{i k} (\partial_{A} g_{k j} + \partial_{j} g_{k A} - \partial_{k} g_{A j}) = \frac{1}{2} r^{- 2} γ^{i k} \partial_{A} (r^{2} γ_{k j}) = (\partial_{A} r / r) δ^{i}_{j}$ , and $Γ^{i}_{j A}$ is the same by symmetry. Finally, with all three indices angular the formula is $\frac{1}{2} γ^{i k} (\partial_{j} γ_{k l} + \partial_{l} γ_{k j} - \partial_{k} γ_{j l})$ , the round-sphere symbols of the statement. This proves (b).

3.1L3L5step 2.1givenalgebra

(Local time orientations and intrinsic curvature.) Fix $y_{0} \in V$ . Since $q (y_{0})$ has inertia $(1, 1, 0)$ , there is a vector $v \in R^{2}$ with $q (y_{0}) (v, v) < 0$ . Continuity gives an open neighborhood $W \subset V$ of $y_{0}$ on which the constant base field $v^{A} \partial_{A}$ is timelike. Its lift $N_{W}$ to $W \times S^{2}$ is smooth and satisfies $g (N_{W}, N_{W}) = q (v, v) < 0$ , so [L5]'s time-oriented curvature suppliers apply there. The global connection supplied by [L3] restricts to the same unique metric-selected connection on each such open set. The curvature operator, lowering and contraction formulas of [L5] contain no $N_{W}$ , so their tensors agree on overlaps and define smooth global curvature and Ricci tensors even when no global time orientation exists. No simultaneous choice of local orientations is needed: this argument is at an arbitrary point.

3.2L4step 1.2step 2.2algebra

(The trace identity.) Metric compatibility in step 1.2 gives $\partial_{A} q^{A B} = - Γ^{A}_{A D} q^{D B} - Γ^{B}_{A D} q^{A D} .$ Consequently $\partial_{A} (q^{A B} \partial_{B} r) = q^{A B} \partial_{A} \partial_{B} r - Γ^{A}_{A D} q^{D B} \partial_{B} r - Γ^{B}_{A D} q^{A D} \partial_{B} r .$ Adding $Γ^{A}_{A B} q^{B D} \partial_{D} r$ cancels the first connection term after relabelling dummy indices. Relabel the remaining term and use symmetry of $q^{A B}$ and of the lower connection indices to obtain $Δ_{q} r = q^{A B} \partial_{A} \partial_{B} r - q^{A B} Γ^{C}_{A B} \partial_{C} r = \partial_{A} (q^{A B} \partial_{B} r) + Γ^{A}_{A B} q^{B D} \partial_{D} r .$ This is the trace identity used in the Ricci contraction below.

4.1L3L5step 2.2step 2.3step 3.1algebra

(Preparation of the Ricci computation.) By [L5] and step 3.1, locally at every base point the Ricci components are ${Ric}_{b d} = \sum_{a} \partial_{a} Γ^{a}_{d b} - \sum_{a} \partial_{d} Γ^{a}_{a b} + \sum_{a, e} Γ^{a}_{a e} Γ^{e}_{d b} - \sum_{a, e} Γ^{a}_{d e} Γ^{e}_{a b}$ , with all indices running over ${0, 1, 2, 3}$ . In the sums we separate the base values $a, e \in {0, 1}$ from the sphere values; by the symbol list of (b) the nonvanishing symbols are the base symbols, the sphere symbols, $Γ^{i}_{A j} = (1 / r) \partial_{A} r δ^{i}_{j}$ and $Γ^{A}_{i j} = - r q^{A D} \partial_{D} r γ_{i j}$ , and every symbol of mixed type with both lower indices base and upper index sphere, or exactly one lower index sphere and upper index base, vanishes; moreover the base symbols, $q$ , $r$ and their derivatives are independent of the angular coordinates, and $\sum_{l} Γ^{l}_{l i} = \partial_{i} \log \sqrt{\det γ} = \cot ϑ δ^{2}_{i}$ .

5.1L3step 1.2step 4.1algebra

(The components ${Ric}_{A B}$ .) Take $b = B$ , $d = A$ base. The terms with all summed indices base give $Ric (q)_{A B}$ . Among the sphere-index terms, the first Ricci sum vanishes because $Γ^{i}_{A B} = 0$ ; the second contributes $- \partial_{A} \sum_{i} Γ^{i}_{i B} = - 2 \partial_{A} (\partial_{B} r / r) = - 2 r^{- 1} \partial_{A} \partial_{B} r + 2 r^{- 2} \partial_{A} r \partial_{B} r$ . The third contributes $2 r^{- 1} \partial_{D} r Γ^{D}_{A B}$ from $\sum_{i} Γ^{i}_{i D} Γ^{D}_{A B}$ ; its other possible sphere-index term is zero because $Γ^{l}_{A B} = 0$ . The fourth contributes $- 2 r^{- 2} \partial_{A} r \partial_{B} r$ from $- \sum_{i, l} Γ^{i}_{A l} Γ^{l}_{i B}$ ; its other mixed terms vanish because $Γ^{i}_{A D} = Γ^{D}_{i B} = 0$ . Adding these contributions gives $- 2 r^{- 1} (\partial_{A} \partial_{B} r - Γ^{D}_{A B} \partial_{D} r) = - 2 r^{- 1} {Hess}_{A B} r$ . Thus ${Ric}_{A B} = Ric (q)_{A B} - 2 r^{- 1} {Hess}_{A B} r$ .

5.2L5step 2.3step 4.1algebra

(The mixed components vanish.) The four sums below are those of the component formula of [L5]. Take $b = i$ , $d = A$ . The first sum $\sum_{a} \partial_{a} Γ^{a}_{i A} = \sum_{l} \partial_{l} ((1 / r) \partial_{A} r δ^{l}_{i})$ vanishes because $r$ is independent of the angular coordinates and the only angular dependence sits in the constant coefficient $δ^{l}_{i}$ ; the second sum $\sum_{a} \partial_{A} Γ^{a}_{a i} = \partial_{A} (\sum_{C} Γ^{C}_{C i} + \sum_{l} Γ^{l}_{l i})$ vanishes because $Γ^{C}_{C i} = 0$ and $\sum_{l} Γ^{l}_{l i} = \cot ϑ δ^{2}_{i}$ is angular. In the third sum the nonvanishing terms are $\sum_{l} Γ^{l}_{l i} ((1 / r) \partial_{A} r) = \cot ϑ δ^{2}_{i} \partial_{A} \log r$ ; in the fourth sum the nonvanishing terms are $- \sum_{l} Γ^{l}_{i l} ((1 / r) \partial_{A} r) = - \cot ϑ δ^{2}_{i} \partial_{A} \log r$ , since the remaining possibilities have at least one symbol of a vanishing mixed type. The two contributions cancel and ${Ric}_{A i} = 0$ .

5.3L6step 2.3step 4.1step 3.2algebra

(The components ${Ric}_{i j}$ .) Take $b = j$ , $d = i$ sphere indices. The terms of the four sums of step 4.1 whose indices are all sphere are exactly the curvature and Ricci computation of the round unit sphere; with the symbols of step 2.3 the direct components are $Ric (γ_{S^{2}})_{22} = 0 + \frac{1}{\sin^{2} ϑ} - \cot^{2} ϑ = 1$ , $Ric (γ_{S^{2}})_{33} = \sin^{2} ϑ - \cos^{2} ϑ - \cos^{2} ϑ + 2 \cos^{2} ϑ = \sin^{2} ϑ$ and $Ric (γ_{S^{2}})_{23} = 0$ , so these terms contribute $Ric (γ_{S^{2}})_{i j} = γ_{i j}$ . The remaining, base-involving terms are: the value $a = A$ of the first sum, $- γ_{i j} \partial_{A} (r q^{A B} \partial_{B} r)$ ; the terms $Γ^{k}_{k A} Γ^{A}_{j i} = - 2 z γ_{i j}$ and $Γ^{A}_{A B} Γ^{B}_{j i} = - r γ_{i j} (\sum_{A} Γ^{A}_{A B}) q^{B D} \partial_{D} r$ of the third sum, where $\sum_{k} Γ^{k}_{k A} = 2 \partial_{A} \log r$ ; and the terms $- Γ^{A}_{j l} Γ^{l}_{A i} - Γ^{l}_{j A} Γ^{A}_{l i} = 2 z γ_{i j}$ of the fourth sum, each of the two equal to $γ_{i j} \sum_{A, B} q^{A B} \partial_{A} r \partial_{B} r = z γ_{i j}$ . Since $\partial_{A} (r q^{A B} \partial_{B} r) = z + r \partial_{A} (q^{A B} \partial_{B} r)$ , these base-involving terms sum to $- γ_{i j} (z + r \partial_{A} (q^{A B} \partial_{B} r)) - 2 z γ_{i j} - r γ_{i j} (\sum_{A} Γ^{A}_{A B}) q^{B D} \partial_{D} r + 2 z γ_{i j} = - γ_{i j} (z + r Δ_{q} r)$ by the trace identity of step 3.1. Adding the sphere contribution gives ${Ric}_{i j} = (1 - z - r Δ_{q} r) γ_{i j}$ .

6.1step 1.1step 2.1step 2.2step 2.3step 5.1step 5.2step 5.3L1L2given∎

(Extension to pole charts and conclusion.) The explicit polar-chart calculations in steps 2.2-5.3 establish the Christoffel and Ricci formulas on the dense regular angular locus. The formulas in clause (b) are the general product-coordinate formulas with the sphere connection of the chosen chart. Each Ricci side in clause (c) is a smooth tensor field: the base block is smooth, the mixed block is zero, and the sphere block is a smooth scalar multiple of $γ_{S^{2}}$ . Since both sides agree on a dense subset, their components agree in every pole chart by continuity. Thus (a)-(c) hold globally; (d) records that no equation on $g$ and no sign of $s$ was used, and $\det q < 0$ entered only through the inertia computation of step 2.1.

Remarks

Where the hypothesis $\det q < 0$ is used. It gives the two-dimensional base the Lorentzian inertia $(1, 1, 0)$ and hence $g$ the inertia $(3, 1, 0)$ of step 2.1; all other computations are algebraic and would hold verbatim for any nondegenerate symmetric $q$ .
The sign convention. The signs of $R^{a}_{b c d}$ and of the Ricci tensor are those of The Riemann curvature operator and the derived Ricci, scalar and Einstein tensors, which fixes $R (\partial_{c}, \partial_{d}) \partial_{b} = R^{a}_{b c d} \partial_{a}$ and ${Ric}_{b d} = \sum_{a, c} g^{a c} R_{a b c d}$ . With the opposite curvature convention, every curvature and Ricci component changes sign; the right-hand sides of clause (c), evaluated with the convention used here, must therefore be negated. The Christoffel symbols, Hessian, $z$ and $Δ_{q} r$ do not change.
Why $q$ is not assumed to come from a global two-manifold. The statement is local in the base coordinates; it applies to every warped-form expression of a smooth Lorentzian metric in a product chart of the form $V \times S^{2}$ , which is the form in which the vacuum computation of the spherical model is performed.

The warped product of a two-dimensional Lorentzian base with a round sphere: Christoffel symbols and Ricci tensor

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources