minkowski_ricci_scalar_zero
plain-language theorem explainer
The Ricci scalar of the Minkowski metric vanishes identically in four-dimensional spacetime. Relativists and Recognition Science derivations cite it to anchor the flat-space limit before introducing curvature or matter. The proof unfolds the scalar definition and reduces directly via the already-established vanishing of the Ricci tensor together with a constant-zero sum.
Claim. The Ricci scalar $R$ of the Minkowski metric satisfies $R=0$, where $R=g^{mu nu}R_{mu nu}$ is the full contraction of the Ricci tensor with the inverse metric.
background
The Ricci scalar is the metric contraction $R = g^{mu nu} R_{mu nu}$ of the Ricci tensor. The Minkowski tensor is the flat metric eta with constant components. This theorem rests on the prior result that the Ricci tensor itself is identically zero for the same metric, obtained by unfolding its definition and summing to zero. The module first constructs Christoffel symbols from the metric and then builds the full curvature hierarchy.
proof idea
One-line wrapper that unfolds the ricci_scalar definition and applies simp using the lemma that the Ricci tensor vanishes together with the fact that the sum of zeros is zero.
why it matters
The result closes the flat curvature chain and is invoked by the proofs that the Einstein tensor vanishes and that the Einstein-Hilbert action is zero in Minkowski space. It supplies the zero-curvature baseline required by the Recognition Science forcing chain at the flat limit (T8 spatial dimension three realized in four-dimensional spacetime). It appears explicitly in the flat_chain_holds certificate that collects all Minkowski geometry lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.