IndisputableMonolith.Gravity.RicciTensor
The RicciTensor module supplies the contraction defining the Ricci tensor from the Riemann curvature tensor in local coordinates. Workers deriving the Einstein field equations or stress-energy conservation laws cite this step. The module consists of definitions that contract the prior Riemann construction without internal proofs.
claimThe Ricci tensor is the contraction $R_{mu nu} = sum_rho R^rho_{mu rho nu}$ of the Riemann tensor $R^rho_{sigma mu nu}$.
background
This module sits inside the coordinate-patch treatment of gravity in Recognition Science. It imports the Levi-Civita connection, which equips a smooth metric $g : R^4 -> R^{4x4}$ with Christoffel symbols, and the Riemann tensor built from those symbols and their derivatives. The Ricci tensor is obtained by tracing the first and third indices of the Riemann tensor. Upstream, the Connection module states it avoids the Mathlib abstract manifold gap while remaining rigorous; the RiemannTensor module records the algebraic symmetries and Bianchi identity.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module feeds the Einstein-Hilbert action, which proves Axiom 2 via Hilbert variation of the action, and the stress-energy tensor module, which proves Axiom 3 by deriving conservation from the contracted Bianchi identity and the Einstein equations.
scope and limits
- Does not treat curvature on abstract manifolds.
- Does not derive the contracted Bianchi identity.
- Does not evaluate components on specific metrics.
- Does not link to the RS forcing chain or phi-ladder.