ricci_flat
plain-language theorem explainer
The Ricci tensor vanishes identically for flat spacetime where the Riemann tensor is zero. Coordinate-based gravity calculations in Recognition Science cite this when confirming Minkowski space as a vacuum solution. The proof proceeds by direct simplification using the Ricci definition and the flat Riemann vanishing result.
Claim. For spacetime indices $mu, nu$, the Ricci tensor $R_{mu nu}$ computed from a vanishing Riemann tensor satisfies $R_{mu nu} = 0$.
background
The module defines the Ricci tensor via contraction of the Riemann tensor as $R_{mu nu} = R^rho_{mu rho nu}$ in local coordinates on four-dimensional spacetime with indices in Fin 4. It builds on the Riemann tensor module to establish curvature identities needed for the Einstein tensor and scalar curvature. Upstream, the Riemann tensor vanishes identically for the flat connection, which directly supports this contraction being zero. This sits within the Recognition Science derivation of gravity from the functional equation and the phi-forcing chain.
proof idea
The proof is a one-line term-mode simplification that substitutes the definition of the Ricci tensor and invokes the lemma establishing that the Riemann tensor vanishes for the flat connection.
why it matters
This theorem feeds directly into the einstein_flat result and the RicciCert structure that certifies Minkowski spacetime as a solution to the vacuum Einstein field equations with vanishing cosmological constant. It completes the flat-space base case in the gravity module, aligning with the T8 step forcing D=3 dimensions and the Recognition Composition Law underlying the curvature definitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.