IndisputableMonolith.Gravity.RicciTensor
Defines the Ricci tensor as the contraction of the Riemann tensor, plus scalar curvature and the Einstein tensor in local coordinates. States vacuum and sourced Einstein equations in coordinate form and records that Minkowski space is a vacuum solution. Downstream gravity modules (Einstein-Hilbert action, full EFE, Regge limit, stress-energy) import this layer. Content is mostly coordinate definitions and direct checks on the already-built Riemann tensor.
claimRicci tensor $R_{\mu\nu}=\sum_{\rho} R^{\rho}{}_{\mu\rho\nu}$; scalar curvature $R=g^{\mu\nu}R_{\mu\nu}$; Einstein tensor $G_{\mu\nu}=R_{\mu\nu}-\frac{1}{2}g_{\mu\nu}R$. Vacuum EFE in coordinates: $G_{\mu\nu}=0$. Sourced form: $G_{\mu\nu}$ equals the matter source term. Minkowski metric is a vacuum solution ($G_{\mu\nu}=0$).
background
Part of the RS gravity stack that targets classical GR from the discrete ledger via continuum limits. Upstream, Connection formalizes the Levi-Civita connection in a coordinate patch where the metric is a smooth map $g:\mathbb{R}^4\to\mathbb{R}^{4\times 4}$, sidestepping Mathlib's missing abstract connections while keeping the calculus rigorous. RiemannTensor defines $R^{\rho}{}_{\sigma\mu\nu}$ from Christoffel symbols and proves algebraic symmetries and the algebraic Bianchi identity.
This module contracts that Riemann tensor to Ricci, $R_{\mu\nu}=R^{\rho}{}{\mu\rho\nu}$, then forms the Ricci scalar and Einstein tensor $G{\mu\nu}=R_{\mu\nu}-\frac12 g_{\mu\nu}R$. Named flatness predicates and Einstein-tensor symmetry are recorded for later use. Constants supplies RS-native units used elsewhere in the gravity chain.
proof idea
Definition-first module, not a deep proof development. Ricci is the index contraction of Riemann on the first and third slots. Scalar curvature is the metric trace of Ricci. Einstein tensor is the standard linear combination of Ricci and scalar. Vacuum and sourced EFE are coordinate statements equating $G_{\mu\nu}$ to zero or to a source. Minkowski-as-vacuum is a direct vanishing check for the constant Minkowski metric. A small certificate bundle packages the main identities for clean import.
why it matters in Recognition Science
Supplies the geometric tensors required by four parent modules: EinsteinHilbertAction (variation of the EH action yields the Einstein tensor; proves Axiom 2), FullEFE (complete nonlinear sourced field equations from the RS lattice), ReggeConvergence (Regge action converges to EH; proves Axiom 1), and StressEnergyTensor (matter coupling and $\nabla^\mu T_{\mu\nu}=0$ from contracted Bianchi plus EFE; proves Axiom 3). Without a coordinate Ricci/Einstein layer, the continuum side of the lattice-to-EFE chain has no classical target. Bridges the RS ledger story to standard GR curvature.
scope and limits
- Does not define abstract-manifold Ricci; works in local coordinates on R^4.
- Does not prove the differential Bianchi identity or covariant conservation here.
- Does not derive the lattice continuum limit; that lives in ReggeConvergence.
- Does not construct the stress-energy tensor or matter action.
- Does not treat quantum gravity or higher-curvature corrections.