riemann_antisymmetric_last_two
plain-language theorem explainer
The Riemann curvature tensor satisfies antisymmetry in its final two indices, so that R^rho_sigma mu nu equals the negative of the same tensor with mu and nu interchanged. Differential geometers and relativists cite the identity when deriving contracted Bianchi relations or Ricci symmetries from the coordinate definition. The proof is a direct algebraic reduction: simplification of the explicit Christoffel expression followed by ring normalization.
Claim. $R^ρ_{σμν} = -R^ρ_{σνμ}$, where $R$ is the Riemann tensor constructed from Christoffel symbols Γ (denoted gamma) and their first partial derivatives (denoted dgamma).
background
The Gravity.RiemannTensor module defines the Riemann curvature tensor in local coordinates from the Christoffel symbols gamma and their derivatives dgamma. It proves the standard algebraic symmetries of this tensor together with the algebraic Bianchi identity, all without invoking a metric tensor or coordinate-free language. The riemann_tensor definition supplies the explicit combination of derivative terms minus quadratic Gamma products that the present result manipulates.
proof idea
The proof is a one-line wrapper that applies simp to unfold the definition of riemann_tensor and ring to confirm the sign change after the index swap.
why it matters
It supplies the antisymmetric component of the RiemannCert record and is invoked by algebraic_bianchi in the same module. Downstream it is reused in Relativity.Geometry.Curvature.riemann_antisymmetric_last_two and in RiemannSymmetries for the lowered-index and trace versions. The identity is a standard algebraic landmark of the curvature tensor in coordinate gravity, independent of the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.