Pith. sign in
module module high

IndisputableMonolith.Relativity.Geometry.Curvature

show as:
view Lean formalization →

The Curvature module supplies the Christoffel symbols and the standard curvature tensors built from an arbitrary metric in the IndisputableMonolith relativity stack. Workers on the discrete-to-continuum bridge or on the Levi-Civita connection cite these objects when passing from lattice J-cost to the Einstein tensor. The module consists entirely of definitions and immediate algebraic identities with no independent proofs.

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}$, Ricci scalar $R$, and Einstein tensor $G_{\\mu\\nu}$ are obtained by the usual contractions and antisymmetrizations.

background

The module lives inside Relativity.Geometry and imports Tensor, Metric, and Derivatives. Derivatives supplies the coordinate basis vectors $e_\mu$ and partial derivatives that appear in every expression. Tensor and Metric provide the abstract index notation and the metric tensor $g_{\mu\nu}$ whose first derivatives determine the connection.

The sibling declarations implement the classical objects of pseudo-Riemannian geometry: christoffel, its symmetry christoffel_symmetric, riemann_tensor, ricci_tensor, ricci_scalar, and einstein_tensor, together with the flat-space specializations eta_deriv_zero, minkowski_christoffel_zero_proper, minkowski_riemann_zero, and minkowski_ricci_zero.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions are imported by LeviCivitaTheorem (which proves the connection is the unique torsion-free metric-compatible one), by CovariantDerivative (which inserts the Christoffel symbols into the covariant derivative formula), by DiscreteBridge (which routes lattice J-cost through the Ricci scalar to the Einstein tensor), by MetricUnification (which identifies the RS-derived Minkowski metric with the present eta), and by ParallelTransport and RiemannSymmetries. The module therefore supplies the curvature layer required by the discrete-to-continuum architecture described in DiscreteBridge.

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)