minkowski_is_vacuum_solution
plain-language theorem explainer
The Minkowski metric satisfies the vacuum Einstein field equations with zero cosmological constant. Researchers modeling flat spacetime solutions in general relativity cite this result to anchor the trivial vacuum case. The proof is a one-line wrapper that invokes the already-proven vanishing of the Einstein tensor on flat space and simplifies.
Claim. The Minkowski metric $g = {diag}(-1, +1, +1, +1)$ with inverse $g^{-1}$ and vanishing Christoffel symbols satisfies $G_{mu nu} + Lambda g_{mu nu} = 0$ for all indices $mu, nu$ when $Lambda = 0$, where $G_{mu nu}$ is the Einstein tensor.
background
The RicciTensor module defines the Ricci tensor by contraction of the Riemann tensor, the scalar curvature by further contraction 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 eta with components diag(-1,1,1,1) and its own inverse. Upstream, einstein_flat already shows that this Einstein tensor vanishes identically when the connection and its derivatives are zero.
proof idea
The proof is a one-line wrapper: introduce the indices mu and nu, then simplify using the einstein_flat theorem.
why it matters
This theorem confirms flat spacetime as a vacuum solution and is invoked directly by hilbert_variation_flat and ricci_cert. It supplies the flat-space base case inside the Recognition Science gravity construction, consistent with the eight-tick octave and the emergence of D=3 spatial dimensions from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.