pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Gravity.RiemannTensor

show as:
view Lean formalization →

Module Gravity.RiemannTensor supplies the coordinate expression for the Riemann curvature tensor from Christoffel symbols and their first derivatives. Researchers building the Recognition Science derivation of general relativity cite it when advancing from the connection to curvature quantities. The module consists of direct definitions for the tensor together with its antisymmetry and algebraic Bianchi identities.

claimThe Riemann curvature tensor in local coordinates is given by $R^ρ_{σμν} = ∂_μ Γ^ρ_{νσ} - ∂_ν Γ^ρ_{μσ} + Γ^ρ_{μλ} Γ^λ_{νσ} - Γ^ρ_{νλ} Γ^λ_{μσ}$, where Γ denotes the Christoffel symbols of the Levi-Civita connection.

background

The module works inside the local coordinate patch introduced by the upstream Connection module, where the metric is realized as a smooth map g : R^4 → R^{4×4} and the Christoffel symbols are computed directly from it. The Constants module supplies the RS-native time quantum τ₀ = 1 tick that sets all units. The Riemann tensor is introduced here via the standard coordinate formula that combines first derivatives of the connection coefficients with the quadratic connection terms.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the downstream RicciTensor module, which constructs the Ricci tensor, scalar curvature, and Einstein tensor from the Riemann tensor and proves that the Einstein tensor is symmetric and divergence-free. It supplies the coordinate-level curvature step that bridges the Levi-Civita connection to the Einstein field equations in the Recognition Science gravity chain.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (6)