ParallelTransportCert
plain-language theorem explainer
The parallel transport certificate structure asserts that a metric g makes parallel-transported vectors constant along curves when g is Minkowski and ensures inner-product preservation for any curve. Researchers deriving curvature from J-cost defects in Recognition Science cite it to anchor the flat-space baseline before introducing holonomy. The definition is a direct packaging of the flat-triviality and preservation conditions with no lemmas required.
Claim. A metric tensor $g$ satisfies the parallel transport certificate when, for the Minkowski metric, any vector field $V$ that is parallel-transported along a spacetime curve $γ$ has constant components, and the inner product $g(V,W)$ remains constant along $γ$ whenever both $V$ and $W$ are parallel-transported.
background
SpacetimeCurve is a smooth path in 4D spacetime with a tangent vector obtained by differentiation. ParallelTransported requires that a vector field $V$ along $γ$ obeys the first-order ODE $dV^μ/dλ + Γ^μ_{αβ} (dγ^α/dλ) V^β = 0$, where $Γ$ are the Christoffel symbols of the Levi-Civita connection induced by $g$. ParallelTransportPreservesInnerProduct states that if both vector fields are parallel-transported then their $g$-inner product is invariant along the curve, a direct consequence of metric compatibility. The module formalizes parallel transport via the Levi-Civita connection and interprets curvature as the geometric signature of non-uniform J-cost defect density that produces gravity.
proof idea
This is a structure definition that directly encodes the two required properties: flat_trivial (constant components under Minkowski) and inner_product_preserved (metric compatibility along curves). No tactics or lemmas are applied inside the definition itself; the downstream theorem parallel_transport_cert_minkowski supplies the concrete witnesses by reduction to the flat-transport lemma and the preservation property.
why it matters
The certificate supplies the flat-space reference case required by the module's holonomy results, including HolonomyDefect and holonomy_vanishes_iff_flat. It anchors the Recognition Science claim that curvature arises from J-cost ledger imbalance, with parallel-transport failure around closed loops as the observable manifestation. The immediate parent is the theorem parallel_transport_cert_minkowski that instantiates the certificate for Minkowski; this step precedes any curvature-induced holonomy calculations in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.