riemann_tensor
plain-language theorem explainer
The definition supplies the coordinate components of the Riemann curvature tensor from a given metric tensor in four-dimensional spacetime. Researchers deriving curvature invariants or performing contractions to Ricci and Einstein tensors cite it as the base object. It is implemented as an explicit formula that extracts index slots, applies partial derivatives to the Christoffel symbols, and assembles the two quadratic sums.
Claim. $R^ρ_{σμν} = ∂_μ Γ^ρ_{νσ} - ∂_ν Γ^ρ_{μσ} + ∑_λ Γ^ρ_{μλ} Γ^λ_{νσ} - ∑_λ Γ^ρ_{νλ} Γ^λ_{μσ}$, where Γ denotes the Christoffel symbols obtained from the metric tensor g.
background
The module constructs Christoffel symbols from the metric tensor, which is introduced as a symmetric bilinear form on four-dimensional spacetime. The MetricTensor structure supplies the local components g_μν(x) at each point together with the symmetry condition. Upstream results include the explicit Christoffel formula for the Hessian metric g(x) = 1/x³ and the placeholder partialDeriv_v2 that stands in for coordinate differentiation in the recognition scaffold.
proof idea
The definition is a direct coordinate formula. It binds the output tensor slots to rho, sigma, mu, nu, calls christoffel g to obtain Γ, applies partialDeriv_v2 to produce the two derivative terms, and adds the two Finset sums over the intermediate index lambda.
why it matters
This definition feeds the Ricci tensor contraction in Gravity.RicciTensor.ricci_tensor and supplies the object whose algebraic properties are recorded in RiemannCert, including antisymmetry in the final pair of indices and vanishing on flat metrics. It completes the curvature construction step in the geometry module before the Einstein tensor appears. In the Recognition framework it bridges the metric to curvature invariants used in the Hamiltonian and forcing-chain constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.