riemann_pair_exchange_proof
plain-language theorem explainer
The theorem establishes the pair-exchange symmetry of the lowered Riemann tensor in explicit coordinates under the explicit-form hypothesis. Relativists and differential geometers cite it when confirming R_ρσμν = R_μνρσ from the Christoffel definition. The proof is a one-line wrapper that applies the lowered pair-exchange lemma and unfolds the lowered-tensor definition.
Claim. Let $g$ be a metric tensor and let $R^α{}_{σμν}$ denote the Riemann tensor. Under the hypothesis that the lowered Riemann tensor satisfies its explicit coordinate expression, $∑_α g_{ρ α}(x) R^α{}_{σ μ ν}(x) = ∑_α g_{μ α}(x) R^α{}_{ν ρ σ}(x)$.
background
The module proves algebraic symmetries of the Riemann curvature tensor derived from its definition via Christoffel symbols. MetricTensor supplies the local bilinear form $g$ on Fin 4 indices at each point $x$. The riemann_tensor is the standard expression $∂μ Γ^ρ{νσ} - ∂ν Γ^ρ{μσ} + Γ^ρ_{μλ} Γ^λ_{νσ} - Γ^ρ_{νλ} Γ^λ_{μσ}$. The local setting is four-dimensional spacetime; the pair-exchange property R_ρσμν = R_μνρσ is obtained from antisymmetry in each pair together with the first Bianchi identity, as stated in the module documentation.
proof idea
The proof calls riemann_lowered_pair_exchange g x ρ σ μ ν h_eq to obtain the lowered symmetry, then unfolds the definition of riemann_lowered to recover the explicit summed form with metric factors and Riemann components. It is a term-mode one-line wrapper.
why it matters
The result supplies the explicit pair-exchange identity that matches the riemann_pair_exchange axiom and is invoked by riemann_pair_exchange_from_definition. It supports the antisymmetry theorems in the Curvature module. In the Recognition framework it completes the algebraic closure of Riemann symmetries in the relativity geometry layer, aligning with the standard properties referenced from Wald and MTW.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.