ParallelTransported
plain-language theorem explainer
A vector field V along a spacetime curve gamma with metric g satisfies the parallel transport equation when its covariant derivative along the curve vanishes identically. Researchers deriving holonomy from curvature or proving preservation of inner products in curved spacetime cite this predicate. It is introduced as the explicit first-order ODE involving the Christoffel symbols contracted with the curve tangent and the vector components.
Claim. A vector field $V : ℝ → (Fin 4 → ℝ)$ along a spacetime curve $γ$ equipped with metric tensor $g$ is parallel-transported when, for every affine parameter $λ$ and component index $μ$, $dV^μ/dλ + Γ^μ_{αβ}(γ(λ)) (dγ^α/dλ) V^β = 0$, where $Γ$ are the Christoffel symbols of $g$.
background
SpacetimeCurve is a structure consisting of a smooth path function from the reals to 4D coordinates together with its tangent vector obtained by componentwise differentiation. MetricTensor supplies the local non-sealed bilinear form on tangent spaces. The Christoffel symbols are those of the Levi-Civita connection induced by the metric, taken from the Euler-Lagrange action module.
proof idea
The declaration is a direct definition. It encodes the parallel transport ODE by requiring that the ordinary derivative of each component of V plus the double sum over Christoffel symbols contracted with the tangent vector and V itself equals zero for every parameter value and index.
why it matters
This predicate is the core definition used by ParallelTransportCert, parallel_transport_flat, ParallelTransportPreservesInnerProduct and ParallelTransportSolution. It supplies the geometric content for the module's main results on holonomy and curvature. In the Recognition Science framework it marks the point where non-uniform J-cost defect density appears as curvature, with parallel-transport failure around closed loops manifesting ledger imbalance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.