parallel_transport_flat
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,
claimIn 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 in Recognition Science
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.
scope and limits
- Does not treat spacetimes with nonzero Christoffel symbols.
- Does not prove existence or uniqueness of parallel transport solutions.
- Does not compute holonomy for non-flat metrics.
- Does not connect the result to specific Recognition Science constants such as the alpha band.
Lean usage
have h_const := parallel_transport_flat γ V h_ptformal statement (Lean)
85theorem parallel_transport_flat (γ : SpacetimeCurve)
86 (V : ℝ → (Fin 4 → ℝ))
87 (h_pt : ParallelTransported minkowski_tensor γ V) :
88 ∀ lam μ, deriv (fun l => V l μ) lam = 0 := by
proof body
Term-mode proof.
89 intro lam μ
90 have h := h_pt lam μ
91 simp only [minkowski_christoffel_zero_proper, zero_mul, Finset.sum_const_zero, add_zero] at h
92 exact h
93
94/-- Parallel transport preserves the metric inner product.
95 If V, W are parallel-transported along γ, then g(V,W) is constant.
96
97 g_{μν} V^μ W^ν = const along γ
98
99 This is a consequence of metric compatibility ∇g = 0. -/