pith. sign in
module module high

IndisputableMonolith.Relativity.Geometry.ParallelTransport

show as:
view Lean formalization →

ParallelTransport module defines parallel transport of vectors along smooth curves in 4D spacetime. Researchers extending Recognition Science relativity geometry would cite these constructions when handling covariant derivatives and holonomy. The module structures content as type definitions for curves and fields followed by preservation and flat-space lemmas.

claimA smooth curve $γ(λ)$ in 4D spacetime; a vector field $V^μ(λ)$ satisfying the parallel transport equation $∇_γ V = 0$; lemmas establishing inner-product preservation and vanishing holonomy when curvature vanishes.

background

The module sits inside the Relativity.Geometry hierarchy and imports Tensor, Metric, Curvature, and Derivatives. Curvature supplies Christoffel symbols derived from the metric; Derivatives supplies the standard basis vector $e_μ$. The supplied doc comment identifies the central object as a smooth curve in 4D spacetime parameterized by λ. Tensor is marked as a scaffold module outside the certificate chain.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies components re-exported by the IndisputableMonolith.Relativity.Geometry aggregator. It contributes the parallel-transport and holonomy machinery required by the parent geometry module.

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)