riemann_tensor
plain-language theorem explainer
The declaration supplies the coordinate formula for the Riemann curvature tensor R^ρ_{σμν} built directly from Christoffel symbols and their first partial derivatives. Relativists and gravity modelers cite it when they need an explicit expression for curvature from a given connection before contracting to the Ricci tensor or checking algebraic identities. The implementation is a literal transcription of the classical expression with explicit summation over the dummy index.
Claim. The Riemann curvature tensor is given by $R^ρ_{σμν} = ∂_μ Γ^ρ_{νσ} - ∂_ν Γ^ρ_{μσ} + Γ^ρ_{μλ} Γ^λ_{νσ} - Γ^ρ_{νλ} Γ^λ_{μσ}$, where Γ^ρ_{μν} are the Christoffel symbols supplied by gamma and ∂_λ Γ^ρ_{μν} are their partial derivatives supplied by dgamma.
background
The Gravity.RiemannTensor module introduces the Riemann tensor from the Christoffel connection to support curvature calculations in local coordinates. gamma encodes the Christoffel symbols Γ^ρ_{μν} while dgamma encodes their first derivatives ∂λ Γ^ρ{μν}; Idx is the index type imported from the Connection module. The module doc states that the file defines the tensor and proves its algebraic symmetries together with the algebraic Bianchi identity and the vanishing result for flat spacetime.
proof idea
This is a definition rather than a theorem. The body directly transcribes the classical formula by subtracting the two first-derivative terms and adding the two quadratic Christoffel products, with summation over the repeated index lambda performed by the ∑ notation.
why it matters
The definition is the base object for the Ricci tensor contraction, the algebraic Bianchi theorem, the antisymmetry theorem, the RiemannCert structure, and the flat-space vanishing theorem inside the same module. It is also referenced by the Relativity.Geometry.Curvature results that recover the Minkowski case. In the Recognition Science setting it supplies the coordinate realization of curvature that links the upstream connection to the forcing chain steps T5–T8 and the spatial dimension D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.