riemann_lowered_antisym_last
plain-language theorem explainer
The fully covariant Riemann tensor satisfies antisymmetry under swap of its final index pair. Relativists and geometers cite this when reducing curvature expressions that involve the lowered form. The proof unfolds the lowered definition, invokes the matching antisymmetry on the mixed tensor, and closes by ring simplification.
Claim. Let $R_{ρσμν}$ be the fully covariant Riemann tensor obtained from metric $g$ at point $x$. Then $R_{ρσμν} = -R_{ρσνμ}$.
background
The module derives the algebraic symmetries of the Riemann curvature tensor from its definition via Christoffel symbols of a metric-compatible, torsion-free connection on four-dimensional spacetime. MetricTensor supplies the local non-degenerate bilinear form used to lower indices. The lowered Riemann tensor is the version with all indices covariant, obtained by contracting the mixed tensor with the metric components.
proof idea
Unfold the lowered definition to expose the sum over the mixed tensor. Distribute negation across the sum and apply congruence. Substitute the known antisymmetry of the mixed tensor via the upstream lemma riemann_antisymmetric_last_two. Reduce the resulting expression with ring normalization followed by rewriting and final ring simplification.
why it matters
This supplies the second-pair antisymmetry required by the algebraic derivation of pair-exchange symmetry in the downstream theorem riemann_lowered_pair_exchange. The module strategy lists exactly three ingredients for that result: first-pair antisymmetry, this second-pair antisymmetry, and the first Bianchi identity. The lemma therefore closes one link in the chain that recovers the standard curvature symmetries used in the Hamiltonian and forcing-chain constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.