pith. sign in
module module high

IndisputableMonolith.Relativity.Geometry.Curvature

show as:
view Lean formalization →

Curvature module defines Christoffel symbols and the derived Riemann, Ricci, and Einstein tensors from a given metric. Researchers building the discrete-to-continuum bridge or proving the fundamental theorem of pseudo-Riemannian geometry cite these objects. The module consists of definitions plus symmetry and Minkowski-vanishing lemmas.

claimChristoffel symbols are given by $Γ^ρ_{μν} = ½ g^{ρσ}(∂_μ g_{νσ} + ∂_ν g_{μσ} − ∂_σ g_{μν})$. The Riemann tensor, Ricci tensor, Ricci scalar, and Einstein tensor are obtained by the usual contractions and covariant derivatives of these symbols.

background

The module sits inside the pseudo-Riemannian geometry layer of the IndisputableMonolith stack. It imports the metric tensor, the tensor algebra, and the derivative operators that supply the coordinate basis vectors $e_μ$. Tensor itself is marked as a scaffold outside the certificate chain.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

It supplies the connection coefficients required by CovariantDerivative, ParallelTransport, and LeviCivitaTheorem. Downstream, DiscreteBridge routes the definitions into the lattice-to-Einstein-tensor map, while MetricUnification uses them to identify the RS-derived Minkowski metric with 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)