ParallelTransportPreservesInnerProduct
Parallel transport along a spacetime curve preserves the metric inner product for any pair of parallel-transported vector fields. Relativists and Recognition Science researchers cite the property when confirming metric compatibility of the Levi-Civita connection. The definition encodes the requirement that the derivative of the summed component product g(V,W) vanishes identically along the curve parameter.
claimLet $g$ be a metric tensor and let $γ$ be a spacetime curve. The property holds when, for every pair of smooth vector fields $V,W$ along $γ$ that satisfy the parallel transport ODE, the derivative with respect to the curve parameter $λ$ of $g_{μν}(γ(λ)) V^μ(λ) W^ν(λ)$ is zero for all $λ$.
background
The module defines parallel transport in 4D spacetime using the Levi-Civita connection from the Christoffel symbols. A SpacetimeCurve consists of a smooth path in ℝ^4 together with its tangent vector. MetricTensor supplies the local bilinear form that defines the inner product at each point. ParallelTransported is the predicate that a vector field V obeys the covariant derivative condition DV^μ/dλ + Γ^μ_{αβ} (dγ^α/dλ) V^β = 0. The module states that parallel transport failure around closed loops manifests ledger imbalance from non-uniform J-cost defect density.
proof idea
This is a direct definition that spells out the preservation condition using component-wise summation inside the derivative operator. No lemmas are invoked; the body simply requires that the λ-derivative of the inner-product sum is identically zero whenever V and W are parallel-transported.
why it matters in Recognition Science
The definition supplies the inner_product_preserved field of the ParallelTransportCert structure and is invoked by the Minkowski special case. It records the geometric consequence of metric compatibility ∇g = 0. In the Recognition Science setting this encodes the absence of holonomy when J-cost defect density is uniform, consistent with the module's account of curvature arising only from ledger imbalance.
scope and limits
- Does not construct solutions to the parallel transport ODE for given initial vectors.
- Does not compute the integrated holonomy around a closed loop.
- Does not relate the property to the phi-ladder or J-cost forcing chain.
- Does not assume the metric is the Minkowski tensor or any other explicit form.
formal statement (Lean)
100def ParallelTransportPreservesInnerProduct (g : MetricTensor) (γ : SpacetimeCurve) : Prop :=
proof body
Definition body.
101 ∀ V W : ℝ → (Fin 4 → ℝ),
102 SmoothField V →
103 SmoothField W →
104 ParallelTransported g γ V →
105 ParallelTransported g γ W →
106 ∀ lam,
107 deriv (fun l =>
108 Finset.univ.sum (fun μ =>
109 Finset.univ.sum (fun ν =>
110 g.g (γ.path l) (fun _ => 0) (fun i => if i.val = 0 then μ else ν) *
111 V l μ * W l ν))) lam = 0
112
113/-- For Minkowski, inner product preservation holds: g(V,W) is constant
114 along any curve when V, W are parallel-transported (both constant in flat space).
115
116 The proof uses the fact that η is position-independent and both V, W
117 have vanishing derivatives (proved by `parallel_transport_flat`).
118 The derivative of Σ (const * const * const) = 0. -/