SpacetimeCurve
plain-language theorem explainer
SpacetimeCurve introduces a parameterized path in 4D spacetime together with its tangent vector obtained by componentwise differentiation. Workers on parallel transport, holonomy, and curvature in the Recognition framework cite it when stating the transport ODE or building closed loops. The declaration is a direct structure with one default field computed from the derivative operator.
Claim. A spacetime curve consists of a map $path: ℝ → ℝ^4$ together with its tangent $tangent(λ)^μ = d(path(λ)^μ)/dλ$.
background
The module formalizes parallel transport along curves in 4D spacetime via the Levi-Civita connection from Curvature.christoffel. Parallel transport moves a vector while satisfying the ODE $DV^μ/dλ + Γ^μ_{αβ} (dγ^α/dλ) V^β = 0$. In Recognition Science, curvature is forced by non-uniform J-cost defect density; parallel transport failure around closed loops manifests the resulting ledger imbalance.
proof idea
Structure definition that declares the path field and supplies the tangent field by direct application of the derivative operator imported from Derivatives.
why it matters
SpacetimeCurve is extended by ClosedLoop and supplies the curve argument to ParallelTransported, ParallelTransportCert, parallel_transport_flat, and ParallelTransportPreservesInnerProduct. It supplies the geometric substrate for the holonomy-curvature correspondence that realizes T8 (D = 3 spatial dimensions realized in 4D spacetime) and the geometric consequence of J-cost imbalance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.