ParallelTransportSolution
plain-language theorem explainer
ParallelTransportSolution defines a vector field along a spacetime curve that obeys the parallel transport ODE from the Levi-Civita connection while matching prescribed initial data. Researchers analyzing holonomy or curvature effects in Recognition Science cite this structure when constructing defects around closed loops. The declaration is a bare structure that assembles the field, the transport predicate, and the initial-condition match with no further steps.
Claim. Let $g$ be a metric tensor and let $γ$ be a smooth curve in 4D spacetime. Given initial data consisting of a parameter value $λ_0$ and a 4-vector $V_0$, a parallel transport solution is a map $V:ℝ→ℝ^4$ such that the covariant derivative of $V$ along $γ$ vanishes and $V(λ_0)=V_0$.
background
The module sets up parallel transport on 4D spacetime via the Levi-Civita connection. A spacetime curve consists of a smooth path together with its tangent vector. The predicate ParallelTransported requires that the ordinary derivative of each component plus the sum of Christoffel symbols contracted with the tangent and the vector itself equals zero for every component and every parameter value.
proof idea
This is a structure definition with an empty proof body. It packages three fields: the vector map, the ParallelTransported predicate applied to the given metric and curve, and the equality that enforces the initial condition at the supplied parameter.
why it matters
HolonomyDefect depends on this structure to witness the vector mismatch after transport around a closed loop, which equals the Riemann tensor contracted with the enclosed area element. The construction therefore supplies the geometric carrier for the ledger imbalance that Recognition Science attributes to non-uniform J-cost defect density. It occupies the slot between the metric interface and the curvature-holonomy correspondence in the relativity layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.