ParallelTransported
The definition encodes the condition that a vector field V along a spacetime curve gamma with metric g obeys the parallel transport ODE when its componentwise derivative plus the summed Christoffel contraction with the tangent and V vanishes identically. General-relativity modelers and Recognition Science workers on curvature from J-cost defects cite this predicate to state the transport law. The definition is a direct transcription of the covariant derivative formula using the imported christoffel symbols and the curve's tangent map.
claimA vector field $V$ along a curve $γ$ in 4-dimensional spacetime with metric tensor $g$ is parallel-transported when, for every affine parameter $λ$ and index $μ$, the ordinary derivative of the $μ$-component plus the contraction of the Christoffel symbols of $g$ with the tangent vector of $γ$ and the components of $V$ equals zero.
background
SpacetimeCurve is the structure supplying a smooth path map from the real line to 4-tuples together with its tangent vector obtained by componentwise differentiation. MetricTensor supplies the local bilinear form on 4-tuples that defines the geometry. The christoffel symbols are the connection coefficients derived from the metric via the standard formula imported from the Euler-Lagrange action module. The module document states that parallel transport is formalized with the Levi-Civita connection on 4D spacetime and that curvature arises in Recognition Science from non-uniform J-cost defect density, with transport failure around closed loops manifesting ledger imbalance.
proof idea
The definition is the direct unfolding of the parallel-transport ODE: it requires the sum over indices of the ordinary derivative of each component of V plus the double sum of christoffel g (gamma path lam) mu alpha beta times tangent alpha times V beta to vanish for every lam and mu.
why it matters in Recognition Science
This predicate supplies the core transport law used by ParallelTransportCert, parallel_transport_flat, ParallelTransportPreservesInnerProduct and ParallelTransportSolution. It fills the geometric slot in the module where holonomy around closed loops is identified with integrated Riemann curvature, which the Recognition framework traces to J-cost defect gradients. The definition therefore anchors the link between the forcing chain and observable gravitational effects via the eight-tick octave and D=3 spatial structure.
scope and limits
- Does not assert existence or uniqueness of solutions for given initial data.
- Does not extend to connections with torsion.
- Does not compute explicit holonomy for concrete metrics.
- Does not address global topology or completeness of the manifold.
formal statement (Lean)
54def ParallelTransported (g : MetricTensor) (γ : SpacetimeCurve)
55 (V : ℝ → (Fin 4 → ℝ)) : Prop :=
proof body
Definition body.
56 ∀ lam μ,
57 deriv (fun l => V l μ) lam +
58 Finset.univ.sum (fun α =>
59 Finset.univ.sum (fun β =>
60 christoffel g (γ.path lam) μ α β *
61 γ.tangent lam α *
62 V lam β)) = 0
63
64/-- Smoothness of a vector field along the affine parameter. -/