pith. sign in
module module high

IndisputableMonolith.Relativity.Geometry.Curvature

show as:
view Lean formalization →

This module supplies the Christoffel symbols and the standard curvature tensors derived from a metric tensor. It is cited by any construction that needs the Levi-Civita connection, covariant derivatives, or the lattice-to-curvature bridge. The module consists of explicit definitions together with immediate algebraic identities and Minkowski-space special cases.

claimThe Christoffel symbols are given by $Γ^λ_{μν} = ½ g^{λσ}(∂_μ g_{νσ} + ∂_ν g_{μσ} - ∂_σ g_{μν})$, from which the Riemann tensor $R^ρ{}_{σμν}$, Ricci tensor $R_{μν}$, Ricci scalar $R$, and Einstein tensor $G_{μν}$ are constructed by the usual contractions and commutators.

background

The module rests on the Metric and Tensor modules for the pseudo-Riemannian metric $g_{μν}$ and on the Derivatives module for the partial derivative operator on tensor components. It introduces the standard objects of local Riemannian geometry: the Christoffel symbols as connection coefficients, the Riemann curvature tensor measuring non-commutativity of covariant derivatives, and the successive contractions that yield the Ricci tensor and scalar. The setting is four-dimensional pseudo-Riemannian geometry with the Minkowski metric as the flat reference case.

proof idea

This is a definition module. The central definition extracts the Christoffel symbols directly from first derivatives of the metric. Symmetry of the lower indices follows at once from the definition. The Riemann tensor is assembled from derivatives of the symbols plus quadratic terms; the Ricci tensor and scalar are obtained by contraction. Minkowski specializations are verified by direct substitution of the flat metric and its vanishing derivatives.

why it matters in Recognition Science

The module is required by LeviCivitaTheorem for the uniqueness of the torsion-free metric-compatible connection, by DiscreteBridge for mapping lattice J-cost defects onto the Ricci scalar and Einstein tensor, and by CovariantDerivative, ParallelTransport, and RiemannSymmetries for all subsequent differential operations. It closes the passage from the RS-derived metric in MetricUnification to the curvature terms that enter the Einstein field equations.

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)