ricci_cert
plain-language theorem explainer
The RicciCert structure certifies that the flat Minkowski metric satisfies the vacuum Einstein field equations with zero cosmological constant. Researchers checking consistency of general relativity vacuum solutions would cite this as the base case. The proof is a term-mode record construction that assembles the certificate directly from the established vanishing results for the Ricci tensor, scalar curvature, and Einstein tensor.
Claim. The flat Minkowski metric satisfies the vacuum Einstein field equations with vanishing cosmological constant, witnessed by the Ricci tensor $R_{mu nu}$, scalar curvature $R$, and Einstein tensor $G_{mu nu}$ all vanishing identically on flat spacetime.
background
The module defines the Ricci tensor as the contraction $R_{mu nu} = R^rho_{mu rho nu}$ of the Riemann tensor, the scalar curvature as its trace $R = g^{mu nu} R_{mu nu}$, and the Einstein tensor as $G_{mu nu} = R_{mu nu} - (1/2) R g_{mu nu}$. These constructions sit inside the local setting that also proves symmetry of $G_{mu nu}$ and its divergence-free property. Upstream lemmas establish the flat limits: ricci_flat shows the Ricci tensor vanishes by reduction to the Riemann tensor vanishing on Minkowski, scalar_flat follows by tracing, and einstein_flat substitutes both into the Einstein tensor definition.
proof idea
The proof is a term-mode record construction that instantiates the RicciCert structure by direct assignment of the four fields: ricci_flat from the Ricci tensor vanishing theorem, scalar_flat from the scalar curvature theorem, einstein_flat from the Einstein tensor vanishing theorem, and minkowski_vacuum from the vacuum solution lemma.
why it matters
This certificate establishes Minkowski spacetime as a vacuum solution to the Einstein equations, closing the flat-case verification inside the Ricci tensor module. It supplies the base case required for any extension to curved or sourced solutions in the Recognition Science gravity derivations. The result aligns with the framework's confirmation that the flat limit satisfies the field equations derived from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.