riemann_flat_vanishes
plain-language theorem explainer
In flat spacetime the Riemann curvature tensor vanishes identically when the Christoffel symbols and their first derivatives are zero. This fact is invoked in derivations that the Ricci tensor is zero for Minkowski space and in the certification of algebraic curvature identities. The proof is a one-line simplification that substitutes the zero connection into the coordinate expression for the tensor.
Claim. In flat spacetime, where the Christoffel symbols vanish and their partial derivatives vanish, the Riemann curvature tensor satisfies $R^ρ{}_{σμν}=0$ for all coordinate indices $ρ,σ,μ,ν$.
background
The module supplies the coordinate definition of the Riemann curvature tensor from the Christoffel symbols of a torsion-free connection. The expression contains first partial derivatives of the symbols together with quadratic products of the symbols themselves. Flat spacetime is the special case in which every Christoffel symbol is the zero function and every first derivative is likewise zero.
proof idea
The proof is a one-line wrapper that applies the simplification tactic directly to the coordinate definition of the Riemann tensor.
why it matters
The result is invoked by the theorem that the Ricci tensor vanishes for flat spacetime and by the structure that collects the algebraic symmetries of the curvature tensor. It supplies the base case confirming that curvature is absent when the connection is flat, consistent with the zero-curvature limit expected from the Recognition Science geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.