ParallelTransported
plain-language theorem explainer
The definition encodes the first-order ODE for a vector field V to be parallel transported along a spacetime curve γ under metric g. Workers on holonomy, geodesic deviation, or metric compatibility in the Recognition framework cite it when building transport certificates or flat-space reductions. It is introduced as a direct predicate that assembles the ordinary derivative of components with the Christoffel contraction supplied by the Euler-Lagrange action module.
Claim. A vector field $V:ℝ→(Fin 4→ℝ)$ along a spacetime curve $γ$ with metric tensor $g$ is parallel transported when, for all affine parameter values $λ$ and components $μ$, the equation holds: $dV^μ/dλ + ∑_{α,β} Γ^μ_{αβ}(γ(λ)) · (dγ^α/dλ) · V^β = 0$, where $Γ$ denotes the Christoffel symbols of $g$.
background
The module sets up parallel transport in 4D spacetime via the Levi-Civita connection. SpacetimeCurve supplies a smooth path together with its tangent vector obtained by differentiation. MetricTensor is the local non-sealed bilinear form interface. Christoffel symbols are taken from the Euler-Lagrange module, where they arise as the connection coefficients of the Hessian metric $g(x)=1/x^3$ used throughout the Recognition framework.
proof idea
The declaration is a definition that directly assembles the covariant derivative condition. It inserts the christoffel term from the Action.EulerLagrange module into the standard parallel-transport ODE and equates the sum to zero for every component.
why it matters
ParallelTransported supplies the core predicate for the four downstream declarations in the same module: ParallelTransportCert (which records flat triviality and inner-product preservation), parallel_transport_flat (which reduces to constancy when Christoffel symbols vanish), ParallelTransportPreservesInnerProduct, and ParallelTransportSolution. It therefore anchors the module's treatment of holonomy as the geometric expression of J-cost defect imbalance, consistent with the framework's derivation of curvature from non-uniform ledger factors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.