riemann_lowered_explicit
plain-language theorem explainer
The explicit coordinate formula for the lowered Riemann curvature tensor R_ρσμν is supplied as a definition in terms of second derivatives of the metric components and quadratic Christoffel terms. A relativist performing coordinate-basis calculations would cite it to verify algebraic symmetries or expand curvature expressions. The definition is a direct transcription of the standard formula, implemented by applying secondDeriv to metric components and contracting Christoffel products with the metric.
Claim. The lowered Riemann tensor is given explicitly by $R_{ρσμν} = (1/2)(∂_σ ∂_μ g_{ρν} + ∂_ρ ∂_ν g_{σμ} - ∂_σ ∂_ν g_{ρμ} - ∂_ρ ∂_μ g_{σν}) + ∑_{α,β} g_{αβ}(Γ^α_{σμ} Γ^β_{ρν} - Γ^α_{σν} Γ^β_{ρμ})$, where g is the metric tensor, Γ denotes the Christoffel symbols of g, and all quantities are evaluated at the spacetime point x.
background
The RiemannSymmetries module establishes the algebraic properties of the Riemann curvature tensor starting from its definition in terms of Christoffel symbols. The MetricTensor structure supplies the metric components as a function of coordinates and index selectors. The christoffel definition computes the connection coefficients from metric derivatives, while secondDeriv extracts the required second partials. This explicit form is introduced to make the first-pair antisymmetry manifest without abstract index gymnastics.
proof idea
The definition directly encodes the standard coordinate expression. It assembles the four second-derivative terms of the metric components with the indicated signs and prefactor 1/2, then adds the double sum over α and β of the metric component times the difference of Christoffel products. No lemmas are invoked; the body is the literal transcription of the formula.
why it matters
This definition supplies the concrete expression required by the downstream theorems riemann_lowered_eq_explicit and riemann_lowered_explicit_antisym_first, which equate the abstract lowered Riemann tensor to this form and prove its antisymmetry in the first index pair. It supports the module's strategy for deriving pair-exchange symmetry from antisymmetry plus the first Bianchi identity, consistent with the references to Wald Chapter 3 and MTW Chapter 13. In the Recognition framework it anchors the geometric curvature sector that follows from the metric and connection structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.