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.

Christoffel symbols 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 Σ$ , metric $g$ and comoving congruence $n = c^{- 1} \partial_{t}$ (FLRW model data: warped product metric, cosmic time, comoving congruence, scale factor and Hubble parameter), and let $\nabla$ be the metric-selected connection of $g$ (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). Let $(x^{0}, x^{1}, x^{2}, x^{3})$ be a product chart with $x^{0} = t$ , where $(x^{1}, x^{2}, x^{3})$ is a smooth chart of $Σ$ , and let $^{(3)} Γ^{i}_{j k}$ be the Christoffel symbols of the Riemannian metric $γ$ in that three-dimensional chart (Christoffel formula for the levi civita connection). Write $\dot{a}$ for the derivative of the scale factor and $H = \dot{a} / a$ for the Hubble parameter. Then in the product chart the Christoffel symbols $Γ^{a}_{b c}$ of $\nabla$ (Christoffel symbols of an affine connection) are:

(a) $Γ^{0}_{00} = Γ^{0}_{0 i} = Γ^{0}_{i 0} = 0$ and $Γ^{i}_{00} = 0$ for $i = 1, 2, 3$ ;

(b) $Γ^{0}_{i j} = Γ^{0}_{j i} = \frac{a \dot{a}}{c^{2}} γ_{i j}$ for $i, j \in {1, 2, 3}$ ;

(c) $Γ^{i}_{0 j} = Γ^{i}_{j 0} = H δ^{i}_{j}$ for $i, j \in {1, 2, 3}$ ;

(d) $Γ^{i}_{j k} =^{(3)} Γ^{i}_{j k}$ for $i, j, k \in {1, 2, 3}$ .

All components not listed vanish; equivalently, the only potentially nonzero Christoffel-symbol families are those in (b)-(d).

Facts & Assumptions

Given: An FLRW model datum with $c > 0$ , its spacetime $M = I \times Σ$ with the metric $g$ of FLRW model data: warped product metric, cosmic time, comoving congruence, scale factor and Hubble parameter, the metric-selected connection $\nabla$ of $g$ , and a product chart $(x^{0}, x^{1}, x^{2}, x^{3})$ with $x^{0} = t$ and $(x^{1}, x^{2}, x^{3})$ a chart of $Σ$ .

[L1]

In the product chart the components of $g$ are $g_{00} = - c^{2}$ , $g_{0 i} = g_{i 0} = 0$ and $g_{i j} = a (t)^{2} γ_{i j}$ , with $γ_{i j}$ the components of the $Σ$ -chart and $a$ smooth and strictly positive (FLRW model data: warped product metric, cosmic time, comoving congruence, scale factor and Hubble parameter); the field $g$ is a smooth Lorentzian metric on $M$ , so its metric-selected connection $\nabla$ is the unique torsion-free $g$ -compatible affine connection (The FLRW metric is smooth Lorentzian; the comoving field is unit timelike and cosmic time parametrizes comoving curves by proper time; the slices carry the scaled spatial metric, Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model, 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).

[L2]

Because $g$ is nondegenerate, the inverse-metric components $g^{a b}$ are characterized by $\sum_{b} g^{a b} g_{b c} = δ^{a}_{c}$ and are smooth; in the product chart $g^{00} = - c^{- 2}$ , $g^{0 i} = g^{i 0} = 0$ and $g^{i j} = a (t)^{- 2} γ^{i j}$ , where $(γ^{i j})$ is the inverse of the positive-definite matrix $(γ_{i j})$ (The inverse metric, musical isomorphisms and index raising, Riemannian metric and riemannian manifold).

[L3]

In every smooth chart the Christoffel symbols of the metric-selected connection are $Γ^{a}_{b c} = \frac{1}{2} \sum_{d} g^{a d} (\partial_{b} g_{d c} + \partial_{c} g_{b d} - \partial_{d} g_{b c})$ , and they are symmetric in the lower pair, $Γ^{a}_{b c} = Γ^{a}_{c b}$ (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, Torsion freedom and metric compatibility in chart components).

[L4]

In the three-dimensional chart of $Σ$ , the Levi-Civita symbols of $γ$ are $^{(3)} Γ^{i}_{j k} = \frac{1}{2} \sum_{l} γ^{i l} (\partial_{j} γ_{k l} + \partial_{k} γ_{j l} - \partial_{l} γ_{j k})$ (Christoffel formula for the levi civita connection). In the product chart, functions of $x$ alone are independent of $t$ and $\partial_{i} a = 0$ for $i = 1, 2, 3$ , while $\partial_{0} a = \dot{a}$ is the derivative of the real function $a$ of one variable; these are the partial-derivative and derivative conventions of Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ and 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 in the Christoffel formula, organized by the index families

1.1L1L2algebra

(Metric and inverse components.) In the product chart [L1] gives $g_{00} = - c^{2}$ , $g_{0 i} = 0$ , $g_{i j} = a (t)^{2} γ_{i j}$ . Solving $\sum_{b} g^{a b} g_{b c} = δ^{a}_{c}$ block by block: the $1 \times 1$ block gives $g^{00} = - c^{- 2}$ ; the vanishing off-diagonal block gives $g^{0 i} = 0$ ; and the spatial block gives $g^{i j} = a (t)^{- 2} γ^{i j}$ , since $(a^{2} γ_{i j})^{- 1} = a^{- 2} (γ_{i j})^{- 1}$ and $γ^{i j}$ is the inverse of the positive-definite matrix $γ_{i j}$ by [L2].

2.1L3step 1.1algebra

(The family $Γ^{0}_{\cdot \cdot}$ and $Γ^{i}_{00}$ .) For $a = i$ and $b = c = 0$ , every differentiated metric component in [L3] vanishes: $\partial_{0} g_{d 0} = \partial_{0} g_{0 d} = 0$ and $\partial_{d} g_{00} = 0$ , so $Γ^{i}_{00} = 0$ . For $a = 0$ and $(b, c) = (0, 0), (0, j), (j, 0)$ , the coefficients $g^{0 i}$ vanish and the remaining derivatives are of the constant component $g_{00} = - c^{2}$ or the zero components $g_{0 j} = g_{j 0} = 0$ ; hence $Γ^{0}_{00} = Γ^{0}_{0 j} = Γ^{0}_{j 0} = 0$ . This is claim (a).

2.2L3L4step 1.1algebra

(The family $Γ^{0}_{i j}$ .) Substituting $a = 0$ , $b = i$ , $c = j$ in [L3]: the terms $\partial_{i} g_{0 j} = 0$ and $\partial_{j} g_{0 i} = 0$ vanish because $g_{0 i} = g_{0 j} = 0$ , leaving $Γ^{0}_{i j} = \frac{1}{2} g^{00} (- \partial_{0} g_{i j}) = \frac{1}{2} (- c^{- 2}) (- \partial_{0} (a (t)^{2} γ_{i j})) = \frac{1}{2} c^{- 2} \cdot 2 a \dot{a} γ_{i j} = \frac{a \dot{a}}{c^{2}} γ_{i j}$ , where $\partial_{0} γ_{i j} = 0$ because $γ_{i j}$ is a function of $x$ alone and $\partial_{0} (a^{2}) = 2 a \dot{a}$ by [L4]. Symmetry in the lower pair gives $Γ^{0}_{j i} = Γ^{0}_{i j}$ . This is claim (b).

2.3L2L3L4step 1.1algebra

(The family $Γ^{i}_{0 j}$ .) Substitute $a = i$ , $b = 0$ , $c = j$ in [L3]. The $d = 0$ summand vanishes because $g^{i 0} = 0$ by step 1.1, so the remaining sum is over $d = 1, 2, 3$ . For those spatial indices, $\partial_{0} g_{j d} = \partial_{0} (a^{2} γ_{j d}) = 2 a \dot{a} γ_{j d}$ , $\partial_{j} g_{0 d} = 0$ and $\partial_{d} g_{0 j} = 0$ because $g_{0 d} = g_{0 j} = 0$ . Hence $Γ^{i}_{0 j} = \frac{1}{2} \sum_{d = 1}^{3} a^{- 2} γ^{i d} \cdot 2 a \dot{a} γ_{j d} = a^{- 1} \dot{a} \sum_{d = 1}^{3} γ^{i d} γ_{j d} = \frac{\dot{a}}{a} δ^{i}_{j} = H δ^{i}_{j}$ , using the spatial inverse identity $\sum_{d = 1}^{3} γ^{i d} γ_{j d} = δ^{i}_{j}$ by [L2] and the definition $H = \dot{a} / a$ . Symmetry gives $Γ^{i}_{j 0} = H δ^{i}_{j}$ . This is claim (c).

2.4L2L3L4step 1.1algebra

(The family $Γ^{i}_{j k}$ .) Substituting $a = i$ , $b = j$ , $c = k$ in [L3]: $\partial_{j} g_{k d} = a^{2} \partial_{j} γ_{k d}$ , $\partial_{k} g_{j d} = a^{2} \partial_{k} γ_{j d}$ and $\partial_{d} g_{j k} = a^{2} \partial_{d} γ_{j k}$ for spatial $d$ , while for $d = 0$ the combination $\partial_{j} g_{k 0} + \partial_{k} g_{j 0} - \partial_{0} g_{j k}$ has vanishing first two terms and its $g^{i 0} = 0$ coefficient annihilates the remaining term; hence $Γ^{i}_{j k} = \frac{1}{2} \sum_{l} a^{- 2} γ^{i l} a^{2} (\partial_{j} γ_{k l} + \partial_{k} γ_{j l} - \partial_{l} γ_{j k}) =^{(3)} Γ^{i}_{j k}$ by [L4]. This is claim (d).

3.1L3step 2.1step 2.2step 2.3step 2.4∎

(Conclusion and identification.) The index triples $(a, b, c)$ with $a, b, c \in {0, 1, 2, 3}$ fall into the families (a)-(d) treated in steps 2.1-2.4: index $a = 0$ splits into $(0, 0, 0)$ , $(0, 0, i)$ , $(0, i, 0)$ , $(0, i, j)$ and index $a = i$ splits into $(i, 0, 0)$ , $(i, 0, j)$ , $(i, j, k)$ , with the symmetry $Γ^{a}_{b c} = Γ^{a}_{c b}$ of [L3] covering the transposed triples. Each family was computed from the same connection $\nabla$ , namely the unique metric-selected connection of the smooth Lorentzian metric $g$ supplied by [L1]; the displays (b)-(d) therefore list all potentially nonzero symbol families, and the proof is complete.

Remarks

Independence of the spatial chart. Claim (d) says that the spatial symbols of the spacetime connection are exactly the Christoffel symbols of the three-dimensional metric $γ$ in the chosen spatial chart, with no explicit dependence on $a$ ; this is why the spatial part of the connection is the Levi-Civita connection of $γ$ (compare Christoffel formula for the levi civita connection).
Normalization check. With $x^{0} = c t$ in place of $t$ as the time coordinate, the components of the same connection carry factors of $c$ from the coordinate change $x^{0} = c t$ ; the displays above are stated in the time coordinate $t$ in seconds and are not to be mixed with the length-coordinate convention for components. The curvature tensors computed in the next lemma are intrinsic geometric objects, whereas their component functions depend on the chosen chart (Tensor fields of type (r,s) on a Lorentzian four-manifold and their components clause (b)).

Christoffel symbols of the FLRW metric in product charts

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources