minkowski_einstein_zero
plain-language theorem explainer
Minkowski spacetime has vanishing Einstein tensor. Workers on flat-space reductions in general relativity or on the Recognition Science discrete bridge would cite this. The proof reduces the Einstein tensor definition directly to the already-proved vanishing of the Ricci tensor and scalar via algebraic simplification.
Claim. For the Minkowski metric $eta$, the Einstein tensor satisfies $G_{mu nu} = 0$.
background
The module derives Christoffel symbols from the metric tensor. The Einstein tensor is defined as $G_{mu nu} = R_{mu nu} - (1/2) g_{mu nu} R$, where $R_{mu nu}$ is the Ricci tensor obtained by contraction of the Riemann tensor and $R$ is the Ricci scalar. Upstream results establish that the Riemann tensor vanishes for Minkowski space, which forces the Ricci tensor and scalar to zero as well.
proof idea
The proof unfolds the Einstein tensor definition and simplifies using the lemmas minkowski_ricci_zero and minkowski_ricci_scalar_zero together with the arithmetic identity that any quantity times zero is zero.
why it matters
This result completes the verification that all curvature quantities vanish in flat space, feeding directly into the flat_chain_holds theorem in the DiscreteBridge module. It confirms consistency of the Recognition framework with the Minkowski limit of general relativity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.