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.

Ricci, scalar and Einstein tensors of the FLRW metric in product charts

Statement

Let $(I, Σ, γ, k, a)$ be an FLRW model datum with conversion constant $c > 0$ , with spacetime $M = I \times Σ$ and metric $g$ (FLRW model data: warped product metric, cosmic time, comoving congruence, scale factor and Hubble parameter, The constant-curvature spatial model of a homogeneous cosmology), let $\nabla$ be its metric-selected connection, and let $R^{a}_{b c d}$ , ${Ric}_{a b}$ , $S$ and $G_{a b}$ be the curvature components, Ricci tensor, scalar curvature and Einstein tensor of $\nabla$ (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, Metric compatibility, torsion freedom and the metric-selected connection class). In a product chart $(x^{0}, x^{1}, x^{2}, x^{3})$ with $x^{0} = t$ , with $\dot{a}$ the derivative of the scale factor and $H = \dot{a} / a$ :

(a) ${Ric}_{00} = - \frac{3 \ddot{a}}{a}$ , ${Ric}_{0 i} = 0$ , and ${Ric}_{i j} = (\frac{a \ddot{a} + 2 {\dot{a}}^{2}}{c^{2}} + 2 k) γ_{i j}$ for $i, j \in {1, 2, 3}$ ;

(b) $S = 6 (\frac{\ddot{a}}{a c^{2}} + \frac{H^{2}}{c^{2}} + \frac{k}{a^{2}})$ ;

(c) $G_{00} = \frac{3 ({\dot{a}}^{2} + k c^{2})}{a^{2}}$ , $G_{0 i} = 0$ , and $G_{i j} = - (\frac{2 a \ddot{a} + {\dot{a}}^{2}}{c^{2}} + k) γ_{i j}$ for $i, j \in {1, 2, 3}$ .

All displayed component functions are smooth on the chart domain; the identities are equalities of the components of the respective tensor fields in the product chart and hold at every point.

Facts & Assumptions

Given: An FLRW model datum with $c > 0$ , its spacetime, metric, connection $\nabla$ , curvature data and a product chart $(x^{0}, x^{1}, x^{2}, x^{3})$ with $x^{0} = t$ .

[L1]

In the product chart the Christoffel symbols are $Γ^{0}_{00} = Γ^{0}_{0 i} = Γ^{i}_{00} = 0$ , $Γ^{0}_{i j} = a \dot{a} γ_{i j} / c^{2}$ , $Γ^{i}_{0 j} = H δ^{i}_{j}$ and $Γ^{i}_{j k} =^{(3)} Γ^{i}_{j k}$ , where $^{(3)} Γ$ are the symbols of the spatial metric $γ$ (Christoffel symbols of the FLRW metric in product charts).

[L2]

The curvature components are given by $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 smooth $(1, 3)$ -tensor whose curvature data are independent of the chart used (Tensoriality of the curvature, its coordinate formula and its point-normal metric formula clause (b), The Riemann curvature operator and the derived Ricci, scalar and Einstein tensors, The algebraic symmetries of the curvature tensor and the symmetry of the Ricci and Einstein tensors).

[L3]

${Ric}_{b d} = \sum_{a, c} g^{a c} R_{a b c d}$ with $R_{a b c d} = \sum_{e} g_{a e} R^{e}_{b c d}$ ; equivalently, in every orthonormal frame ${Ric}_{b d} = \sum_{c} R^{c}_{b c d}$ , which is the trace $tr (Z \mapsto R (Z, \partial_{d}) \partial_{b})$ of the curvature endomorphism (The Riemann curvature operator and the derived Ricci, scalar and Einstein tensors clause (c), Ricci curvature, Ricci curvature is symmetric and basis independent, The inverse metric, musical isomorphisms and index raising). Moreover $S = \sum_{a, b} g^{a b} {Ric}_{a b}$ 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)).

[L4]

The remaining components of the inverse metric in the product chart are $g^{00} = - c^{- 2}$ and $g^{i j} = a (t)^{- 2} γ^{i j}$ , and $\sum_{j} γ^{i j} γ_{j l} = δ^{i}_{l}$ (Christoffel symbols of the FLRW metric in product charts [L2], The inverse metric, musical isomorphisms and index raising).

[L5]

The spatial metric $γ$ has constant sectional curvature $k$ , so its three-dimensional Ricci tensor is $Ric (γ)_{i j} = 2 k γ_{i j}$ ; in the component convention shared with [L2] this reads $\sum_{l}^{(3)} R^{l}_{i l j} = 2 k γ_{i j}$ , where $^{(3)} R$ are the curvature components of $γ$ computed from the symbols $^{(3)} Γ$ (Constant-curvature three-manifolds: equivalence of constant sectional curvature, the tensor identity and the Ricci condition, Ricci curvature, Riemannian metric and riemannian manifold).

[L6]

$\dot{a}$ is the derivative of the smooth function $a$ of $t$ , $H = \dot{a} / a$ , $\ddot{a}$ its second derivative, and $\partial_{i} a = 0$ for $i = 1, 2, 3$ in the product chart (FLRW model data: warped product metric, cosmic time, comoving congruence, scale factor and Hubble parameter, 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).

Proof

technique · direct substitution of the Christoffel symbols in the curvature formula, organized by the index families, followed by the traces

1.1L1L2L3L6algebra

(The ${Ric}_{00}$ component.) By [L3], ${Ric}_{00} = \sum_{c} R^{c}_{0 c 0}$ . In the sum, the term $c = 0$ is $R^{0}_{000} = 0$ because every term of [L2] contains a symbol $Γ^{\cdot}_{00}$ or $Γ^{0}_{0 \cdot}$ , all of which vanish by [L1]. For $c = i$ the same formula gives $R^{i}_{0 i 0} = \partial_{i} Γ^{i}_{00} - \partial_{0} Γ^{i}_{i 0} + \sum_{e} (Γ^{i}_{i e} Γ^{e}_{00} - Γ^{i}_{0 e} Γ^{e}_{i 0}) = 0 - \dot{H} - \sum_{e} Γ^{i}_{0 e} Γ^{e}_{i 0}$ , using $Γ^{i}_{00} = 0$ and $Γ^{i}_{i 0} = H δ^{i}_{i} = H$ from [L1]; the remaining quadratic term is $- \sum_{e} Γ^{i}_{0 e} Γ^{e}_{i 0} = - \sum_{m} (H δ^{i}_{m}) (H δ^{m}_{i}) = - H^{2}$ , because the terms with $e = 0$ contain the vanishing symbol $Γ^{0}_{i 0}$ . Summing over $c = 0, 1, 2, 3$ gives ${Ric}_{00} = 3 (- \dot{H} - H^{2}) = - 3 \ddot{a} / a$ , where $\dot{H} = \ddot{a} / a - (\dot{a} / a)^{2} = \ddot{a} / a - H^{2}$ by [L6].

1.2L1L2L3L5algebra

(The spatial components.) By [L3], ${Ric}_{i j} = \sum_{c} R^{c}_{i c j} = R^{0}_{i 0 j} + \sum_{k} R^{k}_{i k j}$ . For the term $c = 0$ , [L2] and [L1] give $R^{0}_{i 0 j} = \partial_{0} Γ^{0}_{j i} - \partial_{j} Γ^{0}_{0 i} + \sum_{e} (Γ^{0}_{0 e} Γ^{e}_{j i} - Γ^{0}_{j e} Γ^{e}_{0 i}) = \partial_{0} (a \dot{a} γ_{i j} / c^{2}) + 0 - \sum_{m} (a \dot{a} γ_{j m} / c^{2}) (H δ^{m}_{i})$ , since $Γ^{0}_{0 e} = 0$ and $Γ^{0}_{j e} = 0$ for $e = 0$ ; with $\partial_{0} (a \dot{a}) = a \ddot{a} + {\dot{a}}^{2}$ and $a \dot{a} H = {\dot{a}}^{2}$ this is $(a \ddot{a} + {\dot{a}}^{2} - {\dot{a}}^{2}) γ_{i j} / c^{2} = a \ddot{a} γ_{i j} / c^{2}$ . For the spatial terms, substituting [L1] into [L2] and summing over $k$ separates the $γ$ -symbols from the time-dependent symbols exactly as in the third family of Christoffel symbols of the FLRW metric in product charts: the terms with some index $0$ contribute the total $3 H a \dot{a} γ_{i j} / c^{2} - H a \dot{a} γ_{i j} / c^{2} = 2 {\dot{a}}^{2} γ_{i j} / c^{2}$ , and the remaining terms are $\sum_{k} (\partial_{k}^{(3)} Γ^{k}_{j i} - \partial_{j}^{(3)} Γ^{k}_{k i} + \sum_{m} (^{(3)} Γ^{k}_{k m}^{(3)} Γ^{m}_{j i} -^{(3)} Γ^{k}_{j m}^{(3)} Γ^{m}_{k i})) = \sum_{k}^{(3)} R^{k}_{i k j} = 2 k γ_{i j}$ by [L5]. Adding the two contributions gives ${Ric}_{i j} = (a \ddot{a} + 2 {\dot{a}}^{2}) γ_{i j} / c^{2} + 2 k γ_{i j}$ , which is claim (a).

2.1L1L2L3algebra

(The mixed components vanish.) By [L3], ${Ric}_{0 i} = \sum_{c} R^{c}_{0 c i}$ . The term $c = 0$ vanishes as in step 1.1. For $c = j$ , [L2] and [L1] give $R^{j}_{0 j i} = \partial_{j} Γ^{j}_{i 0} - \partial_{i} Γ^{j}_{j 0} + \sum_{e} (Γ^{j}_{j e} Γ^{e}_{i 0} - Γ^{j}_{i e} Γ^{e}_{j 0}) = 0 - 0 + \sum_{m} (^{(3)} Γ^{j}_{j m} H δ^{m}_{i} -^{(3)} Γ^{j}_{i m} H δ^{m}_{j})$ , since the terms with $e = 0$ contain $Γ^{0}_{i 0} = Γ^{0}_{j 0} = 0$ and the spatial derivatives of the functions $H (t) δ^{j}_{i}$ vanish; substituting $δ^{m}_{i}$ and $δ^{m}_{j}$ and summing over $j$ gives $H \sum_{j} (^{(3)} Γ^{j}_{j i} -^{(3)} Γ^{j}_{i j}) = 0$ by the symmetry of the spatial symbols. Hence ${Ric}_{0 i} = 0$ .

2.2L3L4L6step 1.1step 1.2algebra

(Scalar curvature.) By [L3] and [L4], $S = g^{00} {Ric}_{00} + g^{i j} {Ric}_{i j} = - c^{- 2} (- 3 \ddot{a} / a) + a^{- 2} γ^{i j} (\frac{a \ddot{a} + 2 {\dot{a}}^{2}}{c^{2}} γ_{i j} + 2 k γ_{i j})$ . Using $γ^{i j} γ_{i j} = 3$ by [L4], $S = 3 \ddot{a} / (a c^{2}) + 3 (a \ddot{a} + 2 {\dot{a}}^{2}) / (a^{2} c^{2}) + 6 k / a^{2} = 6 (\ddot{a} / (a c^{2}) + H^{2} / c^{2} + k / a^{2})$ , since $a \ddot{a} / a^{2} = \ddot{a} / a$ and ${\dot{a}}^{2} / a^{2} = H^{2}$ by [L6]. This is claim (b).

3.1L3L4step 1.1step 2.1step 1.2step 2.2algebra∎

(Einstein tensor and conclusion.) By [L3] and [L4], $G_{00} = {Ric}_{00} - \frac{1}{2} S g_{00} = - 3 \ddot{a} / a + \frac{1}{2} c^{2} S = - 3 \ddot{a} / a + 3 \ddot{a} / a + 3 H^{2} + 3 k c^{2} / a^{2} = 3 ({\dot{a}}^{2} + k c^{2}) / a^{2}$ by step 2.2; $G_{0 i} = {Ric}_{0 i} - \frac{1}{2} S g_{0 i} = 0$ by step 2.1; and $G_{i j} = {Ric}_{i j} - \frac{1}{2} S g_{i j} = (\frac{a \ddot{a} + 2 {\dot{a}}^{2}}{c^{2}} + 2 k) γ_{i j} - 3 (\frac{\ddot{a}}{a c^{2}} + \frac{H^{2}}{c^{2}} + \frac{k}{a^{2}}) a^{2} γ_{i j} = - (\frac{2 a \ddot{a} + {\dot{a}}^{2}}{c^{2}} + k) γ_{i j}$ by steps 1.2 and 2.2. This is claim (c), and it completes the proof of all three claims.

Remarks

Conventions. The curvature sign convention is the one fixed by The Riemann curvature operator and the derived Ricci, scalar and Einstein tensors and Tensoriality of the curvature, its coordinate formula and its point-normal metric formula: $R (\partial_{c}, \partial_{d}) \partial_{b} = R^{a}_{b c d} \partial_{a}$ and ${Ric}_{b d} = \sum_{c} R^{c}_{b c d}$ . With this convention the round unit two-sphere has positive Ricci curvature and the spatial constant $k = + 1$ gives $Ric (γ) = + 2 γ$ , as recorded in Constant-curvature three-manifolds: equivalence of constant sectional curvature, the tensor identity and the Ricci condition. Other sources order the loop indices differently; no formula of another source is used here without checking it against this convention.
Flat check. For $k = 0$ and $γ$ the Euclidean metric the spatial symbols $^{(3)} Γ$ vanish, so steps 1.1-1.3 reduce to the textbook flat-slice expressions; the derivation covers this case without extra hypotheses and displays the $k$ -dependence explicitly.

Ricci, scalar and Einstein tensors of the FLRW metric in product charts

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources