parallel_transport_flat
plain-language theorem explainer
In Minkowski spacetime the parallel transport condition reduces to the ordinary derivative vanishing because the Christoffel symbols are identically zero. A vector field V along a curve γ that satisfies ParallelTransported minkowski_tensor γ V is therefore constant along γ. Researchers establishing inner-product preservation or zero holonomy in flat space cite this result to justify that transported vectors remain unchanged. The proof is a direct simplification that substitutes the zero connection coefficients and applies the arithmetic lemmas,
Claim. In flat Minkowski spacetime, if a vector field $V:ℝ→ℝ^4$ along a curve $γ$ satisfies the parallel transport equation with respect to the Minkowski metric, then each component obeys $dV^μ/dλ=0$.
background
The predicate ParallelTransported g γ V asserts that the covariant derivative of V along γ vanishes: for all λ and μ the ordinary derivative of the μ-component plus the double sum over α,β of the Christoffel symbol Γ^μ_αβ(γ(λ)) times the tangent component γ'^α times V^β equals zero. SpacetimeCurve packages a smooth path in 4D spacetime together with its tangent vector field. The module develops parallel transport on 4D spacetime using the Levi-Civita connection, interpreting curvature as the geometric manifestation of non-uniform J-cost defect density. Upstream arithmetic results supply the identities add_zero and zero_mul that reduce sums containing zero factors.
proof idea
The proof introduces the parameters λ and μ, unfolds the hypothesis to obtain the parallel transport equation, then rewrites it by substituting the lemma that the Minkowski Christoffel symbols vanish together with zero_mul, Finset.sum_const_zero and add_zero. The resulting equation is exactly the claim that the ordinary derivative is zero.
why it matters
This theorem supplies the flat-space case required by minkowski_preserves_inner (which shows the inner product is constant) and by no_holonomy_if_flat (which concludes zero holonomy defect around closed loops). It fills the zero-curvature limit in the Recognition Science chain that derives three spatial dimensions from the forcing sequence and links curvature to ledger imbalance. The result confirms that vanishing J-cost defect gradients produce trivial transport, consistent with the module's physical interpretation of holonomy as integrated curvature.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.