IndisputableMonolith.Gravity.RiemannTensor
This module supplies the explicit local-coordinate formula for the Riemann curvature tensor from Christoffel symbols and their first derivatives. Researchers deriving general relativity inside Recognition Science would cite it as the curvature definition step. The module is a pure definition block that imports the Levi-Civita connection and the RS time quantum without performing any derivations.
claimThe Riemann curvature tensor in local coordinates is defined by $R^ρ_{σμν} = ∂_μ Γ^ρ_{νσ} - ∂_ν Γ^ρ_{μσ} + Γ^ρ_{μλ} Γ^λ_{νσ} - Γ^ρ_{νλ} Γ^λ_{μσ}$, where Γ denotes the Christoffel symbols of the Levi-Civita connection.
background
The module sits inside the Recognition Science gravity development and imports the fundamental time quantum τ₀ = 1 tick from Constants together with the Levi-Civita connection formalized in local coordinates. The Connection module works in a coordinate patch where the metric is a smooth matrix-valued function g : R^4 → R^{4×4} and avoids the Mathlib abstract-manifold gap. The supplied DOC_COMMENT gives the standard coordinate expression for the Riemann tensor directly in terms of Γ and dΓ.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
The module supplies the Riemann tensor that the downstream RicciTensor module consumes to define the Ricci tensor, scalar curvature, and Einstein tensor while proving symmetry and (stated) divergence-free properties. It therefore occupies the curvature-definition slot in the Recognition Science gravity chain that ultimately produces the Einstein tensor.
scope and limits
- Does not treat global manifold structure or coordinate-free tensor definitions.
- Does not derive any curvature identities or Bianchi relations.
- Does not link the tensor to the phi-ladder or RS mass formulas.
- Does not address coordinate transformations or tensorial character proofs.