ricci_flat
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not treat spacetimes with nonzero curvature.
- Does not prove the Bianchi identities or divergence-free property of the Einstein tensor.
- Does not incorporate the Recognition Science constants such as the phi-ladder or alpha band.
- Does not extend to sourced Einstein equations.
Lean usage
simp [ricci_flat]formal statement (Lean)
41theorem ricci_flat (mu nu : Idx) :
42 ricci_tensor (fun _ _ _ => 0) (fun _ _ _ _ => 0) mu nu = 0 := by
proof body
Term-mode proof.
43 simp [ricci_tensor, riemann_flat_vanishes]
44
45/-! ## Scalar Curvature -/
46
47/-- Scalar curvature: trace of the Ricci tensor with the inverse metric.
48 R = g^{mu nu} R_{mu nu} = sum_{mu,nu} g^{mu nu} R_{mu nu} -/