ParallelTransportSolution
plain-language theorem explainer
ParallelTransportSolution bundles a vector field V along a spacetime curve that obeys the parallel transport ODE for a given metric and matches a prescribed initial vector. Workers on holonomy or curvature in Recognition Science cite it when building solutions to the transport equation for defect calculations. The declaration is a direct structure that assembles the field, the ParallelTransported predicate, and the initial-condition equality.
Claim. A parallel transport solution for metric $g$, curve $γ$, and initial data $ic = (λ_0, V_0)$ consists of a map $V : ℝ → ℝ^4$ such that $V$ satisfies the parallel transport equation $dV^μ/dλ + Γ^μ_{αβ}(γ(λ)) (dγ^α/dλ) V^β = 0$ for all $μ$ and $V(λ_0) = V_0$.
background
SpacetimeCurve is a smooth path in 4D spacetime with an associated tangent vector field. ParallelTransportIC packages a starting parameter λ₀ and initial vector V₀. ParallelTransported is the predicate that a vector field V along γ obeys the first-order ODE obtained from the Levi-Civita connection: the covariant derivative along the curve vanishes. MetricTensor supplies the local bilinear form used to define the Christoffel symbols inside that ODE. The module sets the local setting as the formalization of parallel transport via the Levi-Civita connection on 4D spacetime, with the physical reading that curvature arises from non-uniform J-cost defect density.
proof idea
This is a structure definition that directly assembles the vector field, the ParallelTransported predicate, and the initial-condition equality; no lemmas or tactics are applied.
why it matters
The structure supplies the concrete object required by HolonomyDefect, which encodes the difference between a vector and its parallel transport around a closed loop and thereby realizes the geometric meaning of the Riemann tensor. In the Recognition framework this closes the link from ledger imbalance (J-cost defect) to curvature, consistent with the module statement that parallel-transport failure is the geometric manifestation of that imbalance. It sits inside the chain that forces D = 3 and the eight-tick octave through the same defect mechanism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.