ClosedLoop
plain-language theorem explainer
ClosedLoop defines a spacetime curve that returns to its starting point after traversing the parameter interval [0,1]. Researchers studying holonomy and the geometric origin of curvature in Recognition Science cite this structure when formalizing the failure of parallel transport around loops. The definition is a direct structure extension of SpacetimeCurve that adds only the endpoint identification condition.
Claim. A closed loop is a smooth curve $γ : [0,1] → ℝ^4$ in 4D spacetime satisfying $γ(0) = γ(1)$.
background
The module formalizes parallel transport along curves in 4D spacetime using the Levi-Civita connection from Curvature.christoffel. SpacetimeCurve supplies a smooth path : ℝ → (Fin 4 → ℝ) together with its tangent vector field. ClosedLoop extends this by the single condition that the path returns to its initial point after one unit of parameter time. In the Recognition Science setting, curvature arises from non-uniform J-cost defect density, so that parallel transport around a closed loop registers the ledger imbalance that produces gravity.
proof idea
This is a structure definition extending SpacetimeCurve by the field closed : path 0 = path 1. No lemmas or tactics are invoked; the declaration directly encodes the mathematical endpoint condition.
why it matters
ClosedLoop supplies the loop object required by HolonomyDefect, which states that the difference between an initial vector and its parallel-transported value around the loop equals the Riemann contraction R^ρ_σμν V^σ δA^μν. It likewise supports the theorem no_holonomy_if_flat asserting that vanishing Riemann curvature implies zero holonomy. The structure therefore realizes the geometric meaning of curvature as the integrated effect of J-cost defects, consistent with the T0-T8 forcing chain in which D = 3 spatial dimensions and the eight-tick octave appear.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.