pith. sign in
module module high

IndisputableMonolith.Relativity.Geometry.Curvature

show as:
view Lean formalization →

The Curvature module supplies explicit definitions of the Christoffel symbols from the metric tensor together with the derived Riemann, Ricci, and Einstein tensors. Researchers constructing covariant derivatives or bridging discrete J-cost lattices to continuum GR cite these formulas. It consists of direct definitions plus algebraic symmetry checks on the connection coefficients.

claimThe Christoffel symbols are $\Gamma^\lambda_{\mu\nu} = \frac12 g^{\lambda\sigma}(\partial_\mu g_{\nu\sigma} + \partial_\nu g_{\mu\sigma} - \partial_\sigma g_{\mu\nu})$, from which the Riemann tensor $R^\rho{}_{\sigma\mu\nu}$, Ricci tensor $R_{\mu\nu}$, and scalar $R$ are constructed in the standard manner on a pseudo-Riemannian manifold with metric $g$.

background

The module sits inside the relativity geometry stack and imports the metric tensor, tensor algebra, and partial derivatives from the sibling modules Metric, Tensor, and Derivatives. Derivatives supplies the standard basis vectors $e_\mu$ used to express coordinate derivatives. The setting is the standard pseudo-Riemannian geometry of Mathlib, with the metric assumed smooth and non-degenerate.

proof idea

This is a definition module, no proofs. Individual sibling declarations supply the explicit formulas and verify algebraic identities such as symmetry of the Christoffel symbols.

why it matters in Recognition Science

The module supplies the Christoffel symbols referenced by the Levi-Civita theorem, which states that on any pseudo-Riemannian manifold there exists a unique torsion-free metric-compatible connection whose coefficients are defined here. It also feeds the covariant derivative, parallel transport, discrete bridge from lattice J-cost to Einstein tensor, and metric unification showing the RS-derived Minkowski metric matches the IM eta tensor.

scope and limits

used by (7)

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

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (13)