RicciCert
plain-language theorem explainer
The RicciCert structure bundles four identities confirming that the flat Minkowski metric yields a vanishing Ricci tensor, scalar curvature, Einstein tensor, and satisfies the vacuum Einstein field equation with zero cosmological constant. Researchers checking exact vacuum solutions or the consistency of the Einstein tensor would cite this certificate when confirming Minkowski space as a trivial solution. The structure is assembled by direct reference to the flat-space simplifications already proved for the Riemann contractions.
Claim. Let $g_{mu nu}$ be the Minkowski metric and $g^{mu nu}$ its inverse. The structure RicciCert asserts that the Ricci tensor $R_{mu nu}$ vanishes identically, the scalar curvature $R$ vanishes, the Einstein tensor $G_{mu nu}$ vanishes, and the vacuum Einstein field equation holds with cosmological constant zero.
background
The module defines the Ricci tensor by contracting the Riemann tensor over one index, the scalar curvature as the trace of the Ricci tensor with the inverse metric, and the Einstein tensor as $G_{mu nu} = R_{mu nu} - (1/2) R g_{mu nu}$. The Minkowski metric is the flat metric diag(-1, +1, +1, +1) with its inverse equal to itself. Upstream results establish that the Riemann tensor vanishes when Christoffel symbols are zero, which immediately forces the Ricci tensor, scalar curvature, and Einstein tensor to vanish in flat space.
proof idea
The structure is defined by packaging the four component identities. Each field is supplied directly by the corresponding flat-space theorem already proved in the module: the Ricci-flat identity, the scalar-flat identity, the Einstein-flat identity, and the vacuum EFE theorem for Minkowski.
why it matters
This certificate underpins the ricci_cert theorem that explicitly constructs an instance of RicciCert. It closes the verification that the Einstein tensor vanishes for the flat metric, consistent with the Recognition Science derivation of gravity from the J-cost functional and the eight-tick octave in three spatial dimensions. The result confirms Minkowski space as the canonical vacuum solution with Lambda = 0.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.