IndisputableMonolith.Relativity.Geometry.ParallelTransport
Defines parallel transport of vectors along smooth curves in 4D spacetime, including initial-value solutions, inner-product preservation, and holonomy around closed loops. Relativists and geometers cite it when linking Christoffel connection data to curvature via holonomy defect. The module packages definitions plus flat-space vanishing and curvature-correspondence statements built on the metric and curvature layers.
claimA smooth spacetime curve $\gamma(\lambda)$ in $4$D; a vector field $V$ along $\gamma$ is parallel-transported when $\nabla_{\dot\gamma} V = 0$. The module records the IVP, proves that the Minkowski (flat) connection preserves the metric inner product and has vanishing holonomy on closed loops, and relates holonomy defect to curvature.
background
Parallel transport is the first-order ODE that moves a tangent vector along a curve without intrinsic rotation relative to the Levi-Civita connection of a metric $g$. In coordinates the condition is $\dot V^\rho + \Gamma^\rho_{\mu\nu}\dot\gamma^\mu V^\nu = 0$, with Christoffel symbols taken from the upstream Curvature module ("Christoffel Symbols derived from the metric").
The module sits on Tensor, Metric, Curvature, and the calculus Derivatives layer (standard basis $e_\mu$). It introduces spacetime curves parameterized by $\lambda$, smooth fields along those curves, initial conditions, and solution predicates for the transport ODE. Closed loops and a holonomy defect measure how much a vector fails to return to itself after a circuit; that defect is the geometric avatar of curvature.
Notation is the standard GR one: four spacetime indices, affine parameter $\lambda$, and the metric-compatible connection. Flat (Minkowski) geometry is the baseline case where $\Gamma = 0$ and holonomy vanishes.
proof idea
Definition-heavy module with a short theorem spine. Curves, parallel-transport predicates, smooth fields, IVP data, and solution types are introduced first. Flat-space transport is discharged by vanishing Christoffel symbols. Inner-product preservation along the flow uses metric compatibility of the connection (specialized to Minkowski as a named corollary). Holonomy defect is defined on closed loops; a lemma shows the defect is zero whenever the geometry is flat. A correspondence statement ties nonzero holonomy to curvature, completing the classical loop-to-Riemann link at the level of this scaffold.
why it matters in Recognition Science
Feeds the Geometry aggregator (IndisputableMonolith.Relativity.Geometry), which re-exports all geometry components for convenient importing. Without parallel transport and holonomy, curvature remains an algebraic tensor; this module supplies the path-dependent geometric meaning used downstream in relativistic kinematics and any Recognition-Science reading of geometric phase or defect.
In the broader RS stack, curvature and connection data support the continuum limit of discrete recognition structure (eight-tick / $D=3$ forcing sit upstream in the foundation chain). Holonomy defect is the natural continuum counterpart of path-dependent recognition mismatch. The Tensor import is flagged as scaffold and not part of the certificate chain, so results here inherit that provisional status until the tensor layer is closed.
scope and limits
- Does not construct existence/uniqueness of parallel transport for arbitrary smooth metrics beyond the stated predicates.
- Does not prove the full Ambrose–Singer theorem; only a local holonomy–curvature correspondence stub.
- Does not treat non-Levi-Civita or torsionful connections.
- Does not certify numerical transport schemes or discrete lattice holonomy.
- Does not escape scaffold status inherited from the Tensor layer.
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