pith. sign in
module module moderate

IndisputableMonolith.Relativity.Geometry.Connection

show as:
view Lean formalization →

The Connection module supplies a stub implementation for the Christoffel symbol bundle in the relativity geometry layer, defaulting every entry to zero. It organizes placeholder definitions for covariant derivatives and metric compatibility ahead of full connection calculus. This is a scaffolding module with no theorems or proofs, imported only to structure the geometry components.

claimThe module provides the Christoffel connection bundle with entries defaulting to zero: $Γ^λ_{μν}=0$ for all indices in the stub.

background

This module sits inside the Relativity.Geometry section and imports the Metric and Tensor modules to support connection structures. Sibling definitions such as ChristoffelSymbols, christoffel_from_metric, covariant_deriv_vector, and metric_compatibility introduce the standard objects of differential geometry on a manifold equipped with a metric. The Tensor import carries the explicit note that it is a scaffold module outside the certificate chain.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the parent Geometry aggregator, which re-exports all geometry components for convenient importing. It supplies the scaffold stub for Christoffel symbols noted in the module documentation, completing the basic connection layer before any active theorems are added.

scope and limits

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)