ricci_tensor
plain-language theorem explainer
The Ricci tensor is defined by contracting the Riemann curvature tensor on its first and third indices, yielding the standard component expression R_mu nu equals sum over rho of R^rho_mu rho nu. General relativists building the Einstein field equations and Recognition Science derivations of curvature identities cite this definition when constructing the Einstein tensor or verifying flat-space solutions. The definition is a one-line wrapper that applies the summation contraction directly to the Riemann tensor.
Claim. $R_{mu nu}(Gamma, partial Gamma) := sum_rho R^rho_{mu rho nu}(Gamma, partial Gamma)$, where $R^rho_{sigma mu nu}$ is the Riemann curvature tensor built from the Christoffel symbols $Gamma$ and their first derivatives.
background
The Gravity.RicciTensor module defines the Ricci tensor, scalar curvature, and Einstein tensor from the Riemann tensor, with the explicit goal of proving that the Einstein tensor is symmetric and that flat spacetime satisfies the vacuum Einstein equations. Idx is the four-dimensional index type Fin 4. The upstream riemann_tensor supplies the curvature components via the standard combination of connection derivatives and quadratic gamma terms.
proof idea
One-line wrapper that applies the summation contraction to the riemann_tensor definition.
why it matters
This definition supplies the Ricci components required by einstein_tensor, RicciCert, and HilbertVariationCert. RicciCert uses it to certify that Minkowski spacetime is a vacuum solution; HilbertVariationCert invokes it when deriving the Einstein tensor as the variational derivative of the Einstein-Hilbert action. In the Recognition framework it completes the geometric side of the curvature definitions that must be consistent with the forcing chain before the Einstein equations are imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.