einstein_flat
plain-language theorem explainer
Einstein tensor vanishes identically for the Minkowski metric with zero connection coefficients. Vacuum solution verifications and the Hilbert variation certificate cite this to confirm flat spacetime solves the vacuum Einstein equations. The proof is a direct simplification using the definitions of the Einstein tensor together with the flat Ricci tensor and flat scalar curvature.
Claim. The Einstein tensor $G_{mu nu}$ for the Minkowski metric $eta_{mu nu}$ with vanishing Christoffel symbols satisfies $G_{mu nu} = 0$ for all spacetime indices $mu, nu$.
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 the 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}$. The Minkowski metric is the flat diagonal form diag(-1, +1, +1, +1) whose inverse coincides with itself. Upstream results establish that both the Ricci tensor and scalar curvature vanish for this metric with zero connection coefficients.
proof idea
One-line wrapper that applies the definition of the Einstein tensor and substitutes the lemmas for the flat Ricci tensor and flat scalar curvature.
why it matters
This theorem is invoked inside the RicciCert and HilbertVariationCert structures to certify that Minkowski spacetime satisfies the vacuum Einstein field equations. It completes the flat-case verification in the gravity sector, consistent with the Recognition Science derivation of three spatial dimensions. It supports the claim that the vacuum sector holds without curvature or sources.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.