IndisputableMonolith.Gravity.RiemannTensor
The module defines the Riemann curvature tensor via the standard coordinate formula from Christoffel symbols and their derivatives. Gravity researchers in the Recognition Science setting cite it when passing curvature to the Ricci contraction. Content consists of direct definitions matching the classical expression with no additional theorems proved.
claim$R^\rho{}_{\sigma\mu\nu} = \partial_\mu \Gamma^\rho_{\nu\sigma} - \partial_\nu \Gamma^\rho_{\mu\sigma} + \Gamma^\rho_{\mu\lambda}\Gamma^\lambda_{\nu\sigma} - \Gamma^\rho_{\nu\lambda}\Gamma^\lambda_{\mu\sigma}$, where $\Gamma$ are the Christoffel symbols of the Levi-Civita connection.
background
The module works in the local coordinate patch on R^4 introduced by the Connection module, which defines the Levi-Civita connection through Christoffel symbols as smooth matrix-valued functions to bypass the absence of connections in Mathlib. Constants supplies the base time quantum $\tau_0 = 1$ tick that sets units throughout the framework. The Riemann tensor appears here as the curvature object prior to contraction.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
Supplies the Riemann tensor to the RicciTensor module, which contracts it to obtain the Ricci tensor, scalar curvature, and Einstein tensor while establishing symmetry of $G_{\mu\nu}$ and its divergence-free property.
scope and limits
- Does not derive Christoffel symbols from a metric tensor.
- Does not prove Bianchi identities or other curvature relations.
- Does not address abstract manifolds or global structure.
- Does not incorporate Recognition Science modifications to classical curvature.