pith. sign in
module module moderate

IndisputableMonolith.Relativity.Geometry.Connection

show as:
view Lean formalization →

The Connection module stubs the Christoffel symbol bundle for the affine connection in relativity geometry. Developers extending covariant derivatives would reference it during framework assembly. It supplies placeholder zero defaults as temporary scaffolding rather than a completed implementation.

claimThe Christoffel symbols $Γ^ρ_{μν}$ of the Levi-Civita connection on a manifold equipped with metric $g_{μν}$, realized as a stub bundle whose entries default to zero.

background

This module belongs to the Relativity.Geometry package and imports the Metric module (for the metric tensor) together with the Tensor module (for tensor operations). The Tensor import carries an explicit note that it is a scaffold module outside the certificate chain. The local theoretical setting is the construction of an affine connection compatible with the metric, with the Christoffel symbols serving as the primary object alongside covariant derivatives and metric-compatibility conditions.

proof idea

This is a definition module, no proofs. It supplies stub entries for the Christoffel symbol bundle and related functions with zero defaults.

why it matters in Recognition Science

The module is imported by the Geometry aggregator, whose doc-comment states it re-exports all geometry components for convenient importing. It supplies the connection layer required for the relativity geometry domain, though the scaffold status keeps it outside the main certificate chain.

scope and limits

falsifier

A non-scaffold implementation of the Christoffel symbols derived from the metric would discharge the stub.

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (9)