SpacetimeCurve
plain-language theorem explainer
A spacetime curve is a map from a real parameter to 4D coordinates together with its tangent vector obtained by componentwise differentiation. Workers on parallel transport, holonomy, and curvature in the Recognition Science framework cite this structure when stating predicates for vector fields along paths. The declaration is a plain structure definition supplying the two fields used by every later transport predicate in the module.
Claim. A spacetime curve consists of a map $γ : ℝ → ℝ^4$ together with its tangent vector field $˙γ^μ(λ) := dγ^μ/dλ$.
background
The module formalizes parallel transport along curves in 4D spacetime using the Levi-Civita connection. In Recognition Science curvature is forced by non-uniform J-cost defect density; parallel-transport failure around closed loops is the geometric manifestation of the ledger imbalance that creates gravity. The structure supplies the basic object (path and tangent) that is extended by ClosedLoop and referenced by ParallelTransported, ParallelTransportPreservesInnerProduct, and parallel_transport_flat.
proof idea
Structure definition that introduces the path field and a default tangent field computed by differentiation. No lemmas or tactics are applied.
why it matters
Foundational type for the entire parallel-transport development. It is extended by ClosedLoop and supplies the curve argument to ParallelTransportCert, ParallelTransportPreservesInnerProduct, minkowski_preserves_inner, and parallel_transport_flat. The module doc states that holonomy encodes the J-cost imbalance; the structure therefore sits at the interface between the geometric side of the Recognition Science forcing chain (T5–T8) and the ledger interpretation of curvature.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.