parallel_transport_flat
plain-language theorem explainer
In Minkowski spacetime a vector field satisfying the parallel transport ODE along any curve must have vanishing ordinary derivative and hence be constant. Researchers deriving flat-space limits or initial data for holonomy calculations cite this result. The proof is a direct simplification of the defining ODE via the vanishing Christoffel symbols of the Minkowski metric together with the arithmetic lemmas zero_mul and add_zero.
Claim. Let $γ$ be a smooth curve in 4D spacetime and let $V:ℝ→(Fin 4→ℝ)$ be a vector field along $γ$. If $V$ satisfies the parallel-transport condition $dV^μ/dλ + Γ^μ_{αβ}(dγ^α/dλ)V^β=0$ for the Minkowski metric (whose Christoffel symbols vanish), then $dV^μ/dλ=0$ for every component $μ$.
background
The module defines parallel transport on 4D spacetime via the Levi-Civita connection. SpacetimeCurve is a smooth path $λ↦x(λ)$ equipped with its tangent; ParallelTransported g γ V is the predicate that $V$ obeys the first-order ODE $DV^μ/dλ + Γ^μ_{αβ} (dγ^α/dλ) V^β =0$ for metric $g$. The local setting is the Recognition Science interpretation that curvature is the geometric signature of non-uniform J-cost defect density, so the Minkowski case corresponds to uniform ledger balance and therefore zero curvature.
proof idea
The term proof introduces the parameters lam and μ, extracts the parallel-transport equation from the hypothesis h_pt, then rewrites it by the lemma minkowski_christoffel_zero_proper together with zero_mul, Finset.sum_const_zero and add_zero, reducing the left-hand side to the ordinary derivative and yielding the required equality.
why it matters
The result supplies the flat-space case needed by minkowski_preserves_inner, no_holonomy_if_flat and parallel_transport_cert_minkowski. It closes the trivial-holonomy branch of the holonomy-curvature correspondence and aligns with the T5–T8 forcing chain in which flat geometry is the zero-defect limit. No open scaffolding remains for this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.