ParallelTransportPreservesInnerProduct
plain-language theorem explainer
Defines the predicate that the metric inner product of two vector fields stays constant along a curve under parallel transport. Workers on metric compatibility and holonomy in 4D spacetime cite this predicate when building transport certificates. The definition directly encodes the vanishing of the parameter derivative of the contracted product g(V,W).
Claim. For a metric tensor $g$ and spacetime curve $γ$, the inner product preservation property holds precisely when, for all smooth vector fields $V$ and $W$ that are parallel transported along $γ$, the derivative with respect to the curve parameter $λ$ of $∑_{μ,ν} g_{μν}(γ(λ)) V^μ(λ) W^ν(λ)$ equals zero.
background
The module formalizes parallel transport along curves in 4D spacetime via the Levi-Civita connection. SpacetimeCurve is the structure consisting of a smooth path $ℝ → (Fin 4 → ℝ)$ together with its tangent. MetricTensor supplies the local bilinear form interface used to contract vectors. Parallel transport itself is the ODE requiring the covariant derivative of the vector field along the curve to vanish. In the Recognition Science setting, curvature (and therefore holonomy) is the geometric expression of non-uniform J-cost defect density on the recognition manifold.
proof idea
The declaration is a direct definition of the Prop. It expands the preservation statement into the explicit requirement that the λ-derivative of the double sum over the metric components times the vector components is identically zero whenever both fields satisfy the parallel transport ODE.
why it matters
The predicate is required by the ParallelTransportCert structure (inner_product_preserved field) and is instantiated by the minkowski_preserves_inner theorem. It records the standard consequence of metric compatibility ∇g = 0. Within the Recognition framework this supplies the geometric link between ledger imbalance and the failure of parallel transport around closed loops, consistent with the forcing chain that produces D = 3 spatial dimensions and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.