riemann_lowered_antisym_first
plain-language theorem explainer
The theorem proves antisymmetry of the lowered Riemann tensor in the first index pair, so that R_ρσμν equals negative R_σρμν. Differential geometers working in general relativity cite this when reducing curvature expressions or deriving further identities such as pair exchange. The term proof rewrites both sides to the explicit Christoffel form via the equivalence hypothesis and applies the manifest antisymmetry of that expression.
Claim. Let $g$ be a metric tensor and $x$ a point in coordinates. For indices $ρ, σ, μ, ν$, if the lowered Riemann tensor equals its explicit expression for the pairs $(ρ,σ)$ and $(σ,ρ)$, then $R_{ρσμν} = -R_{σρμν}$.
background
This module derives the algebraic symmetries of the Riemann curvature tensor from its definition via Christoffel symbols of the metric. The MetricTensor structure supplies the local non-sealed bilinear form on Fin 4. The lowered Riemann tensor R_ρσμν is the fully covariant version. Upstream, the explicit expression lemma equates the tensor to its coordinate formula, and the explicit antisymmetry lemma shows the sign flip under index swap in that formula. The setting follows standard general relativity as outlined in the module documentation referencing Wald and MTW.
proof idea
The proof is a term-mode wrapper. It rewrites the left and right sides using the explicit equivalence applied to the respective hypotheses. It then applies exact to the lemma that directly gives the antisymmetry on the explicit form.
why it matters
This antisymmetry is the first of three properties used to derive the pair exchange symmetry in the downstream theorem that establishes R_ρσμν = R_μνρσ. The module documentation states that pair exchange follows algebraically from the two antisymmetries and the first Bianchi identity. It corresponds to the standard property in Wald's General Relativity, Section 3.2. Within the framework, it confirms that the geometry reproduces the curvature symmetries of classical general relativity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.