IndisputableMonolith.Relativity.Geometry.ParallelTransport
Module for parallel transport of vectors along smooth curves in 4D spacetime, plus holonomy around closed loops and its link to curvature. Relativists cite it for the Levi-Civita infrastructure connecting Christoffel symbols to path-dependent transport. It packages curve and transport-ODE definitions with theorems on metric preservation, flat trivial holonomy, and holonomy-curvature correspondence.
claimA smooth curve $\gamma(\lambda)$ in 4D spacetime carries a vector field $V$ by parallel transport when $\nabla_{\dot\gamma} V = 0$. The holonomy defect around a closed loop is the failure of $V$ to return to itself; it vanishes when the curvature vanishes, and the metric inner product is preserved along the transport.
background
Parallel transport moves a tangent vector along a curve so its covariant derivative along the curve vanishes. The connection is the Levi-Civita connection of a spacetime metric; Christoffel symbols are supplied by the Curvature module ("Christoffel Symbols derived from the metric"). Tensor and Metric give the underlying tensor and metric structures; Derivatives supplies coordinate calculus.
The module works in 4D spacetime. Named objects include SpacetimeCurve (smooth curve parameterized by $\lambda$), the parallel-transport ODE and its initial-value data, SmoothField, and ClosedLoop / HolonomyDefect for the integrated effect of curvature after a loop.
proof idea
Definition-heavy geometry module rather than a single theorem. It introduces SpacetimeCurve and the parallel-transport ODE (ParallelTransported, ParallelTransportIC, ParallelTransportSolution), then records that transport preserves the metric inner product, that flat metrics yield path-independent transport and trivial holonomy, and states the holonomy-curvature correspondence linking loop defects to Riemann curvature built from Christoffel symbols.
why it matters in Recognition Science
Feeds the Geometry aggregator, which "re-exports all geometry components for convenient importing." Supplies the language for curvature acting on transported frames in the Relativity domain. HolonomyCurvatureCorrespondence and no_holonomy_if_flat connect local curvature (from the Curvature import) to global transport defects, the classical geometric fact underlying gravitational holonomy and frame dragging. In the broader RS chain this sits under spacetime geometry supporting the D=3 forcing landmark, without itself claiming that step.
scope and limits
- Does not construct the exponential map or prove geodesic completeness.
- Does not derive uniqueness of Levi-Civita beyond what Curvature already supplies.
- Does not treat spin connection or fermionic parallel transport.
- Does not specialize metrics to Recognition-native (phi-ladder) forms.
- Does not compute explicit holonomy for non-flat exact solutions.
used by (1)
depends on (4)
declarations in this module (14)
-
structure
SpacetimeCurve -
def
ParallelTransported -
def
SmoothField -
structure
ParallelTransportIC -
structure
ParallelTransportSolution -
theorem
parallel_transport_flat -
def
ParallelTransportPreservesInnerProduct -
theorem
minkowski_preserves_inner -
structure
ClosedLoop -
def
HolonomyDefect -
theorem
no_holonomy_if_flat -
def
HolonomyCurvatureCorrespondence -
structure
ParallelTransportCert -
theorem
parallel_transport_cert_minkowski