IndisputableMonolith.Relativity.Geometry.ParallelTransport
ParallelTransport module defines smooth curves in 4D spacetime and parallel transport of vector fields along them, including initial conditions, solutions, and flat-space preservation lemmas. It would be cited by researchers deriving holonomy from curvature in Recognition Science relativity models. The module assembles definitions and basic lemmas atop tensor, metric, and curvature imports without a central theorem.
claimA spacetime curve $C: I → M^4$ parameterized by affine parameter $λ$, with parallel transport of a vector field $V$ satisfying $∇_{C'} V = 0$ where $∇$ is the Levi-Civita connection from the metric $g_{μν}$ and its Christoffel symbols.
background
The module sits inside Relativity.Geometry and imports standard basis vectors $e_μ$ from Derivatives, Christoffel symbols from Curvature, and tensor operations from Tensor and Metric. It introduces SpacetimeCurve as a smooth curve in 4D spacetime parameterized by λ, together with ParallelTransported fields, ParallelTransportIC, and ParallelTransportSolution. Sibling objects include ClosedLoop, HolonomyDefect, and flat-space cases such as parallel_transport_flat and no_holonomy_if_flat.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
Supplies the geometric primitives re-exported by the parent IndisputableMonolith.Relativity.Geometry aggregator. It supports downstream holonomy-curvature correspondence results such as HolonomyCurvatureCorrespondence and no_holonomy_if_flat, connecting the metric layer to observable transport along curves in the Recognition framework.
scope and limits
- Does not derive the metric or Christoffel symbols from Recognition Science primitives.
- Does not treat non-Levi-Civita connections or spinor transport.
- Does not provide explicit solutions for curved spacetimes such as Schwarzschild.
- Does not address global topology or non-simply-connected manifolds.
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