fundamentalLoop
plain-language theorem explainer
The fundamental once-around loop on the unit circle: the continuous path on [0,1] sending t to the point at angle 2πt under the trigonometric covering. Anyone computing winding numbers or path displacements on S¹ cites this as the canonical generator. Continuity is the covering map composed with scalar multiplication by 2π on the unit interval.
Claim. The fundamental loop is the continuous map $f\colon I\to S^1$ given by $f(t)=\gamma(2\pi t)$, where $\gamma\colon\mathbb{R}\to S^1$ is the standard trigonometric covering parametrization and $I=[0,1]$ is the unit interval (as a topological space).
background
This module builds a local winding (displacement) invariant for paths in the exact TopCat.sphere 1 object. One lifts a path through the covering map given by the trigonometric parametrization and measures how far the lift travels in $\mathbb{R}$. The carrier of that sphere object is abbreviated SphereOne.
The trigonometric covering $\gamma$ (written trigCirclePoint) sends a real angle to the corresponding point of $S^1$ and is continuous. Surjectivity of $\gamma$ is available in-module, so every point of the sphere is hit by some real angle. The module's central technical fact is that displacement computed from the canonical lift equals the endpoint difference of any continuous lift: two lifts of one path that start in the same fiber differ by a constant deck transformation in $2\pi\mathbb{Z}$.
No axioms, sorry, or project-local $S^1$ replacements are used.
proof idea
A structure definition of a continuous map $I\to S^1$. The underlying function is $t\mapsto\gamma(2\pi t)$. Continuity is one composition: continuity of the trigonometric covering, composed with continuous multiplication by the constant $2\pi$ and the continuous coercion from the subtype $I\subseteq\mathbb{R}$ to $\mathbb{R}$. No further lemmas are needed.
why it matters
This is the canonical generator against which the winding invariant is calibrated. Downstream, fundamentalLift_lifts records that the explicit linear lift $t\mapsto 2\pi t$ covers this loop; pathDisplacement_fundamentalLoop then shows the displacement equals one full turn $2\pi$; and pathWinding_fundamentalLoop concludes the winding number is $1$. That last fact is the surjectivity witness: the invariant is a left inverse to the fundamental loop class on the nose.
Further downstream, oneSimplexPath_fundamental in CircleWindingChain identifies the fundamental singular $1$-simplex (in the unit-interval parametrization) with this same loop, tying the path-level generator into the singular-simplex chain. Within Recognition Science this sits in the foundation layer that makes topological winding a usable, choice-independent invariant before any physics constants are introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.