Pith. sign in
module module high

IndisputableMonolith.Gravity.RicciTensor

show as:
view Lean formalization →

The RicciTensor module contracts the Riemann curvature tensor over one index pair to define the Ricci tensor in local coordinates. It is cited by derivations of the Einstein field equations and the stress-energy conservation law. The module assembles the contraction from the imported RiemannTensor and Connection definitions with no new theorems.

claimThe Ricci tensor is the contraction $R_{\mu\nu} = \sum_\rho R^\rho{}_{\mu\rho\nu}$ of the Riemann curvature tensor $R^\rho{}_{\sigma\mu\nu}$ obtained from the Levi-Civita connection.

background

This module sits inside the coordinate formulation of general relativity. It imports the Levi-Civita connection (Christoffel symbols as functions of the metric) and the Riemann tensor (built from Christoffel symbols and their first derivatives) from the upstream modules. The Ricci tensor is obtained by the indicated index contraction.

Constants supplies the RS time quantum but plays no role in the curvature definitions. The module therefore provides the standard contraction step required before the Einstein tensor or stress-energy conservation can be stated.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the Ricci tensor to EinsteinHilbertAction (which proves the Hilbert variation that yields the Einstein tensor) and to StressEnergyTensor (which proves conservation from the contracted Bianchi identity). It therefore completes the curvature contraction step in the Recognition Science gravity chain leading to the Einstein field equations.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (12)