minkowski_ricci_zero
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish curvature properties for non-Minkowski metrics.
- Does not derive explicit components of the Riemann tensor beyond vanishing.
- Does not address coupling to matter or stress-energy sources.
Lean usage
simp only [minkowski_ricci_zero]formal statement (Lean)
145theorem minkowski_ricci_zero (x : Fin 4 → ℝ) (up : Fin 0 → Fin 4) (low : Fin 2 → Fin 4) :
146 ricci_tensor minkowski_tensor x up low = 0 := by
proof body
Term-mode proof.
147 unfold ricci_tensor
148 simp [minkowski_riemann_zero, Finset.sum_const_zero]
149
150/-- Ricci scalar vanishes for Minkowski space. -/