ricci_tensor
plain-language theorem explainer
The Ricci tensor arises as the contraction of the Riemann tensor on its first and third indices, producing the bilinear form R_mu nu from a given metric. Relativists deriving the Einstein field equations or the Hilbert action cite this step when reducing the full curvature to the trace needed for the Einstein tensor. The definition implements the contraction by direct summation over the four index values using the supplied Riemann tensor on the input metric.
Claim. For a metric tensor $g$, the Ricci tensor is the bilinear form $R(x, low) = sum_{rho=0}^3 R^rho{}_{mu rho nu}(x)$ where $mu$ and $nu$ are read from the two-index vector $low$ and $R^rho{}_{sigma mu nu}$ is the Riemann tensor constructed from $g$.
background
The module treats curvature quantities derived from the metric in four-dimensional spacetime. The MetricTensor structure supplies a local bilinear form $g$ on vectors indexed by Fin 4, while BilinearForm provides the codomain type for the resulting curvature objects. Christoffel symbols are obtained from the metric and its derivatives; the Riemann tensor is then built from those symbols before contraction yields the Ricci tensor.
proof idea
The definition is a direct functional wrapper. It extracts mu and nu from the low argument, then sums the Riemann tensor over rho in Fin 4 by constructing the appropriate three-index vector for each term.
why it matters
This supplies the Ricci tensor to the Einstein tensor definition and the HilbertVariationCert structure that certifies the vacuum Einstein equations for Minkowski space. It appears in the RicciCert that confirms flat spacetime satisfies the vacuum field equations with zero cosmological constant. The construction sits inside the geometric layer that ultimately connects to the eight-tick octave and D=3 spatial dimensions in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.