parallel_transport_flat
plain-language theorem explainer
In flat Minkowski spacetime, any vector field satisfying the parallel transport equation along a curve must have vanishing ordinary derivatives in each component. Researchers establishing the flat limit before analyzing holonomy defects from J-cost imbalances cite this result. The term-mode proof unfolds the transport predicate and cancels all connection terms once the Minkowski Christoffel symbols are substituted.
Claim. Let $γ$ be a smooth curve in 4D spacetime and $V:ℝ→ℝ^4$ a vector field along $γ$. If $V$ obeys the parallel transport condition with the Minkowski metric, then $dV^μ/dλ=0$ for every component $μ$ and parameter $λ$.
background
SpacetimeCurve packages a path $ℝ→ℝ^4$ together with its tangent obtained by differentiation. ParallelTransported encodes the first-order ODE requiring that the ordinary derivative of each component plus the contraction of the Christoffel symbols with the tangent and the vector itself equals zero. The module develops these notions via the Levi-Civita connection and interprets curvature as the geometric signature of non-uniform J-cost defect density.
proof idea
Term-mode proof. Introduce the parameters lam and μ, obtain the transport equation from the hypothesis, then rewrite it in place using the vanishing of the Minkowski Christoffel symbols together with zero_mul, Finset.sum_const_zero and add_zero; the resulting identity is exactly the claim.
why it matters
The theorem is invoked directly by minkowski_preserves_inner, no_holonomy_if_flat and parallel_transport_cert_minkowski. It supplies the flat-space anchor for the module claim that holonomy vanishes precisely when the Riemann tensor vanishes, aligning with the Recognition Science identification of curvature with ledger imbalance. It closes the baseline case needed before curvature sourced by J-cost defects is introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.