pith. sign in
module module high

IndisputableMonolith.Relativity.Geometry.ParallelTransport

show as:
view Lean formalization →

The ParallelTransport module defines spacetime curves and vector transport rules in 4D geometry. It would be cited by researchers deriving covariant derivatives or holonomy from the metric. The module supplies definitions and supporting lemmas that rest on imported curvature and tensor structures.

claimA smooth curve $C: I → M$ in 4-dimensional spacetime $M$ parameterized by affine parameter $λ$, together with the parallel transport equation $∇_{C'} V = 0$ for a vector field $V$ along $C$.

background

The module sits inside the Relativity domain and imports the metric tensor, Christoffel symbols (from the Curvature module), tensor algebra, and derivative operators. Its central object is the smooth curve in 4D spacetime parameterized by λ. The upstream Curvature module supplies Christoffel symbols derived from the metric; the Tensor module is explicitly marked as scaffolding and outside the certificate chain.

proof idea

This is a definition module, no proofs.

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 curve and transport primitives required by downstream holonomy and curvature correspondence results listed among its siblings.

scope and limits

used by (1)

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

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (14)