SpacetimeCurve
SpacetimeCurve records a smooth path through 4D spacetime together with its tangent vector obtained by componentwise differentiation. Parallel-transport and holonomy proofs cite it as the basic curve object on which the Levi-Civita connection acts. The definition is a direct structure that supplies the path function and derives the tangent automatically.
claimA spacetime curve is a map $γ:ℝ→ℝ^4$ equipped with its tangent vector field $γ̇(λ)=dγ/dλ$ computed componentwise.
background
The module formalizes parallel transport along curves in 4D spacetime using the Levi-Civita connection from Curvature.christoffel. SpacetimeCurve supplies the underlying geometric object: a parameterized path whose tangent is required for the parallel-transport ODE. In Recognition Science, curvature arises from non-uniform J-cost defect density; parallel-transport failure around closed loops manifests the resulting ledger imbalance that produces gravity.
proof idea
One-line structure definition that records the path function and installs the tangent as the automatic derivative of each component.
why it matters in Recognition Science
SpacetimeCurve is the base type for ClosedLoop, ParallelTransported, ParallelTransportPreservesInnerProduct and ParallelTransportCert. It fills the geometric prerequisite for the holonomy-curvature correspondence that links Riemann curvature to integrated J-cost defects. The module doc states that zero holonomy holds if and only if the Riemann tensor vanishes, directly tying the structure to the Recognition Science claim that curvature is forced by defect density.
scope and limits
- Does not impose a metric or connection on the curve.
- Does not require the path to be closed or timelike.
- Does not enforce higher differentiability beyond existence of the first derivative.
- Does not encode any Recognition Science J-cost or defect data.
Lean usage
def straight_line : SpacetimeCurve := { path := fun λ => ![λ, 0, 0, 0] }formal statement (Lean)
44structure SpacetimeCurve where
45 path : ℝ → (Fin 4 → ℝ)
46 tangent : ℝ → (Fin 4 → ℝ) := fun lam μ => deriv (fun l => path l μ) lam
proof body
Definition body.
47
48/-! ## §2 Parallel Transport Along a Curve -/
49
50/-- A vector field V along a curve γ is parallel-transported if
51 DV^μ/dλ + Γ^μ_{αβ} (dγ^α/dλ) V^β = 0.
52
53 This is the defining ODE for parallel transport. -/