riemann_lowered
plain-language theorem explainer
The lowered Riemann tensor is defined by contracting the mixed curvature tensor with the metric to obtain the fully covariant form R_ρσμν. General relativists cite this when deriving algebraic symmetries or Bianchi identities in coordinate bases. The implementation is a direct summation that lowers the first index via the metric components.
Claim. The fully covariant Riemann curvature tensor is defined by $R_{ρσμν}(x) = g_{ρα} R^α{}_{σμν}(x)$, where the contraction uses the metric tensor $g$.
background
The module derives symmetry properties of the Riemann tensor in four-dimensional spacetime from its definition via Christoffel symbols. The MetricTensor structure supplies the local bilinear form interface. Upstream results include the mixed Riemann tensor construction in the Curvature module and the MetricTensor definition as a non-sealed bilinear form on Fin 4 coordinates.
proof idea
This is a direct definition implementing index lowering as a sum over the dummy index α of the metric component times the mixed tensor component. No lemmas are applied inside the body; it is the explicit contraction operation.
why it matters
This definition supplies the base object for CurvatureAxiomsHold, which bundles the pair-exchange symmetry R_ρσμν = R_μνρσ with Ricci symmetry. It is invoked directly by the antisymmetry theorems riemann_lowered_antisym_first and riemann_lowered_antisym_last as well as the lowered first Bianchi identity. The construction aligns with the standard curvature axioms referenced in Wald Chapter 3 and supports the geometric layer of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.