Pith. sign in
module module moderate

IndisputableMonolith.Relativity.Geometry.Connection

show as:
view Lean formalization →

The Connection module supplies a stub Christoffel symbol bundle with zero defaults inside the Recognition Science relativity geometry layer. It would be referenced by anyone extending covariant derivatives or curvature once the placeholders are filled. The module consists of imports from Metric and Tensor plus sibling definitions that remain inactive.

claimChristoffel symbols bundle with default value zero, denoted $Γ^ρ_{μν}=0$.

background

This module belongs to the Relativity.Geometry hierarchy and imports the Metric module (spacetime structure) together with the Tensor module (multilinear maps). The Tensor module carries an explicit scaffold warning that it lies outside the certificate chain. Sibling declarations introduce ChristoffelSymbols, christoffel_from_metric, covariant_deriv_vector, metric_compatibility and minkowski_christoffel_zero, all currently zero-valued placeholders.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the IndisputableMonolith.Relativity.Geometry aggregator, which re-exports every geometry component for convenient use. It occupies the scaffold slot for the affine connection required by later relativity constructions, as flagged in its own documentation.

scope and limits

falsifier

Implementation of christoffel_from_metric that derives nonzero symbols from the metric tensor while satisfying metric_compatibility.

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)