ExampleConstruction: AI-adaptedVerification: 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.

Curvature, Ricci, scalar and Einstein tensors of a metric with a round two-sphere factor

Example

Let $S^{2} : = {(X, Y, Z) \in R^{3} : X^{2} + Y^{2} + Z^{2} = 1}$ with the round metric induced by the Euclidean inner product, and let $M : = R^{2} \times S^{2}$ with the product Lorentzian metric whose first factor has line element $- (d x^{0})^{2} + (d x^{3})^{2}$ . Use the sphere chart $σ : (0, π) \times (0, 2 π) \to S^{2}$ given by $σ (θ, φ) = (\sin θ \cos φ, \sin θ \sin φ, \cos θ),$ and put $U : = R^{2} \times σ ((0, π) \times (0, 2 π)) \subset M$ . In the product chart with coordinate order $x = (x^{0}, x^{1}, x^{2}, x^{3}) = (x^{0}, θ, φ, x^{3})$ , the metric is $g : = - (d x^{0})^{2} + (d x^{1})^{2} + \sin^{2} (x^{1}) (d x^{2})^{2} + (d x^{3})^{2}, N : = \partial_{0} .$ This chart contains the equatorial geodesic segment used in An equator geodesic of the round-sphere factor: conjugate instant at distance pi with multiplicity one; the underlying manifold has an actual $S^{2}$ factor, not an unwrapped angular cover. The metric is smooth and Lorentzian on $M$ with time orientation $N$ (Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model). Let $\nabla$ be its metric-selected connection and $R$ , $R_{a b c d}$ , ${Ric}_{a b}$ , $S$ and $G_{a b}$ its curvature data (Metric compatibility, torsion freedom and the metric-selected connection class, Existence and uniqueness of the metric-selected connection of a nondegenerate metric, and its extension to tensor fields, The Riemann curvature operator and the derived Ricci, scalar and Einstein tensors). Then:

The only nonzero Christoffel symbols in this chart are $Γ^{1}_{22} = - \sin x^{1} \cos x^{1}, Γ^{2}_{12} = Γ^{2}_{21} = \cot x^{1} .$
The curvature has exactly one independent nonzero lowered component up to the algebraic symmetries, namely $R_{1212} = \sin^{2} (x^{1});$ equivalently $R (\partial_{1}, \partial_{2}) \partial_{2} = \sin^{2} (x^{1}) \partial_{1}$ and $R (\partial_{1}, \partial_{2}) \partial_{1} = - \partial_{2}$ , and every component containing an index $0$ or $3$ vanishes.
The Ricci tensor, scalar curvature and Einstein tensor are ${Ric}_{11} = 1, {Ric}_{22} = \sin^{2} (x^{1}), S = 2, G = diag (1, 0, 0, - 1) .$
The contracted second Bianchi identity $\nabla^{a} G_{a b} = 0$ holds. In the displayed chart $U$ , $\nabla_{e} G_{a b} = 0$ identically, so the divergence vanishes term by term there.

Facts & Assumptions

Given: The product $M = R^{2} \times S^{2}$ with its product metric and time orientation $N$ , and its local chart $U$ with $0 < x^{1} < π$ and $0 < x^{2} < 2 π$ as specified above. Let $\nabla$ be the metric-selected connection and $R$ , $R_{a b c d}$ , $Ric$ , $S$ , and $G$ its curvature data.

[L1]

The product metric is smooth Lorentzian of signature $(-, +, +, +)$ on $M$ with time orientation $N = \partial_{0}$ ; its components on $U$ are $diag (- 1, 1, \sin^{2} (x^{1}), 1)$ . The metric-selected connection exists and is unique, and on $U$ its Christoffel symbols are $Γ^{a}_{b c} = \frac{1}{2} g^{a d} (\partial_{b} g_{d c} + \partial_{c} g_{b d} - \partial_{d} g_{b c})$ , with $g^{a d}$ the matrix inverse of $g_{a b}$ (Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model, Metric compatibility, torsion freedom and the metric-selected connection class, Existence and uniqueness of the metric-selected connection of a nondegenerate metric, and its extension to tensor fields clause (a), Christoffel symbols of an affine connection, The inverse metric, musical isomorphisms and index raising).

[L2]

The curvature components in a chart are $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})$ , and $R$ is a tensor: its components transform between charts, while tensor identities and vanishing are chart-independent; the displayed nonzero component values below refer to the specified product chart (Tensoriality of the curvature, its coordinate formula and its point-normal metric formula clauses (a)-(b), The Riemann curvature operator and the derived Ricci, scalar and Einstein tensors clause (b)).

[L3]

The lowered curvature satisfies $R_{a b c d} = - R_{b a c d} = - R_{a b d c} = R_{c d a b}$ and $R_{a b c d} + R_{a c d b} + R_{a d b c} = 0$ ; equivalently $R (X, Y) Z = - R (Y, X) Z$ and $g (R (X, Y) Z, W) = - g (R (X, Y) W, Z)$ (The algebraic symmetries of the curvature tensor and the symmetry of the Ricci and Einstein tensors clauses (a)-(c)).

[L4]

The Ricci tensor, scalar curvature and Einstein tensor are ${Ric}_{b d} = g^{a c} R_{a b c d}$ , $S = g^{b d} {Ric}_{b d}$ and $G_{a b} = {Ric}_{a b} - \frac{1}{2} S g_{a b}$ (The Riemann curvature operator and the derived Ricci, scalar and Einstein tensors clause (c)).

[L5]

The contracted second Bianchi identity reads $\nabla^{a} G_{a b} = 0$ , where $\nabla^{a} G_{a b} = g^{a e} \nabla_{e} G_{a b}$ and $\nabla$ acts on tensor components by the metric-compatible derivative (The second Bianchi identity and the vanishing divergence of the Einstein tensor clause (b), Existence and uniqueness of the metric-selected connection of a nondegenerate metric, and its extension to tensor fields clause (c)).

Verification

technique · direct

1.1L1algebra

(Christoffel symbols.) Only $g_{22} = \sin^{2} (x^{1})$ is nonconstant, with $\partial_{1} g_{22} = 2 \sin x^{1} \cos x^{1}$ and $g^{22} = \sin^{- 2} (x^{1})$ ; by [L1] the only possible nonzero symbols are $Γ^{1}_{22} = \frac{1}{2} g^{11} (- \partial_{1} g_{22}) = - \sin x^{1} \cos x^{1}$ and $Γ^{2}_{12} = Γ^{2}_{21} = \frac{1}{2} g^{22} \partial_{1} g_{22} = \cot x^{1}$ , every other symbol vanishing because it contains $\partial_{a} g_{b c}$ with $a \neq 1$ or a constant component.

2.1L2step 1.1L3algebra

(Candidate components.) In the coordinate formula of [L2] every term contains a factor $Γ^{a}_{\cdot \cdot}$ or a derivative of one; by step 1.1 a term can be nonzero only if all its symbol indices lie in ${1, 2}$ . Hence $R^{a}_{b c d} = 0$ whenever one of $a, b, c, d$ equals $0$ or $3$ : the derivative terms contain $Γ^{a}_{d b}$ or $Γ^{a}_{c b}$ with a forbidden index in the lower pair, or are annihilated by $\partial_{0}, \partial_{3}$ , and each product term contains a symbol with a forbidden index. Of the four remaining candidates $R^{1}_{112}$ , $R^{1}_{212}$ , $R^{2}_{112}$ , $R^{2}_{212}$ , the first and the last have a repeated index in the first lower pair, so their lowered components vanish by the skew-symmetry of [L3], and $R^{2}_{112}$ is the negative of $R^{2}_{121}$ ; it therefore suffices to check $R^{1}_{212}$ and $R^{2}_{121}$ , which are equal up to lowering and sign.

2.2step 1.1L2L3L4algebra

(The curvature component.) By [L2] and step 1.1, the products in $R^{1}_{212}$ contribute only through $- \sum_{e} Γ^{1}_{2 e} Γ^{e}_{12} = - Γ^{1}_{22} Γ^{2}_{12}$ , because $Γ^{1}_{1 e} = 0$ for every $e$ kills the first product and the only nonzero term of the second has $e = 2$ ; hence $R^{1}_{212} = \partial_{1} Γ^{1}_{22} - \partial_{2} Γ^{1}_{12} - Γ^{1}_{22} Γ^{2}_{12} = - \partial_{1} (\sin x^{1} \cos x^{1}) + \sin x^{1} \cos x^{1} \cot x^{1} .$ Substituting and using $\cos x^{1} \cot x^{1} = \cos^{2} x^{1} / \sin x^{1}$ , $R^{1}_{212} = - (\cos^{2} x^{1} - \sin^{2} x^{1}) + \cos^{2} x^{1} = \sin^{2} (x^{1})$ . Lowering with $g_{11} = 1$ gives $R_{1212} = \sin^{2} (x^{1})$ ; by [L3], $R_{2121} = R_{1212}$ and the skew-symmetry gives $R^{2}_{121} = \sin^{- 2} (x^{1}) R_{2121} = 1$ , and the vector-valued forms follow from $R (\partial_{c}, \partial_{d}) \partial_{b} = R^{a}_{b c d} \partial_{a}$ .

3.1step 2.1step 2.2L4algebra

(Ricci tensor.) By [L4] and step 2.1, the only components of $R_{a b c d}$ that can contribute to a contraction are those with all indices in ${1, 2}$ : ${Ric}_{11} = g^{22} R_{2121} = \sin^{- 2} (x^{1}) \sin^{2} (x^{1}) = 1$ and ${Ric}_{22} = g^{11} R_{1212} = \sin^{2} (x^{1})$ , while ${Ric}_{b d} = 0$ whenever $b$ or $d$ is $0$ or $3$ , because every term of the sum $g^{a c} R_{a b c d}$ then contains a component with a forbidden index.

4.1step 3.1L4algebra

(Scalar curvature and Einstein tensor.) By [L4] and step 3.1, $S = g^{11} {Ric}_{11} + g^{22} {Ric}_{22} = 1 + \sin^{- 2} (x^{1}) \sin^{2} (x^{1}) = 2$ . Hence $G_{11} = 1 - \frac{1}{2} \cdot 2 \cdot 1 = 0$ , $G_{22} = \sin^{2} (x^{1}) - \frac{1}{2} \cdot 2 \cdot \sin^{2} (x^{1}) = 0$ , $G_{00} = 0 - \frac{1}{2} \cdot 2 \cdot (- 1) = 1$ , $G_{33} = 0 - \frac{1}{2} \cdot 2 \cdot 1 = - 1$ , and all off-diagonal components vanish: $G = diag (1, 0, 0, - 1)$ .

5.1step 4.1L5algebra∎

(Divergence of the Einstein tensor in the chart.) By [L5] and the formula for the covariant derivative of a tensor, $\nabla_{e} G_{a b} = \partial_{e} G_{a b} - \sum_{d} (Γ^{d}_{e a} G_{d b} + Γ^{d}_{e b} G_{a d})$ on $U$ . Step 4.1 gives $\partial_{e} G_{a b} = 0$ ; and each product vanishes because a nonzero $Γ^{d}_{e a}$ has all three indices in ${1, 2}$ , while $G_{d b}$ or $G_{a d}$ is nonzero only when both its indices are $0$ or both are $3$ , so no index value is available for $d$ . Hence $\nabla_{e} G_{a b} = 0$ throughout $U$ , and the contracted divergence vanishes term by term there, in accordance with the globally valid identity [L5].

Remarks

What the example checks. The computation verifies on an explicit curved metric the definitions of the Ricci, scalar and Einstein tensors, the algebraic symmetries in the form $R_{1212} = R_{2121}$ and $R_{1212} + R_{1122} + R_{1221} = 0$ , and the contracted second Bianchi identity. The metric is not Ricci flat and is not flat: $R_{1212} = \sin^{2} (x^{1})$ is nonzero throughout the chart $U$ , so $Ric \neq 0$ by step 3.1.
Relation to the tidal page. On the equator $x^{1} = π / 2$ , the geodesic and field of An equator geodesic of the round-sphere factor: conjugate instant at distance pi with multiplicity one have $T = \partial_{2}$ and $J (s) = \sin (s) \partial_{1}$ . The component $R (\partial_{1}, \partial_{2}) \partial_{2} = \sin^{2} (x^{1}) \partial_{1}$ computed above, together with skew-symmetry, gives the curvature term $R (T, J) T = - \sin (s) \partial_{1}$ . That item verifies the Jacobi equation and the conjugate instant it entails.

Curvature, Ricci, scalar and Einstein tensors of a metric with a round two-sphere factor

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources