minkowski_ricci_zero
plain-language theorem explainer
The Ricci tensor vanishes identically for the Minkowski metric. Researchers establishing the flat-space limit of curvature tensors in the Recognition framework would cite this result. The proof reduces the claim to the prior vanishing of the Riemann tensor by unfolding the contraction and applying a summation identity.
Claim. Let $R$ denote the Ricci tensor obtained by contracting the Riemann tensor of the Minkowski metric tensor. Then $R(x) = 0$ at every point $x$.
background
The Ricci tensor is the contraction $R_{mu nu} = sum_rho R^rho_{mu rho nu}$ of the Riemann curvature tensor. The Minkowski metric is the constant diagonal tensor with signature (-1,1,1,1). The module first derives Christoffel symbols from the metric and then shows that the Riemann tensor vanishes identically for this choice. The upstream result states that the Riemann tensor vanishes for Minkowski space.
proof idea
Unfold the definition of the Ricci tensor to express it as a sum over Riemann components. Apply the theorem that the Riemann tensor is zero for the Minkowski metric. The resulting sum is identically zero by the constant-zero summation rule.
why it matters
This theorem is used to prove that the Einstein tensor vanishes for Minkowski space and that the Ricci scalar is zero. It is assembled into the flat chain statement that collects all flat-space curvature results. The result confirms the consistency of the Minkowski background with the zero-curvature expectation when no sources are present.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.