pathDisplacement_fundamentalLoop
plain-language theorem explainer
The once-around generator of the circle has path displacement exactly one full turn $2\pi$. Anyone computing the local winding invariant on $S^1$ cites this as the nonzero generator value. The proof rewrites via lift-independence to the explicit linear lift $t\mapsto 2\pi t$ and simplifies the endpoint difference.
Claim. The displacement of the fundamental once-around loop on $S^1$ equals $2\pi$: if $\gamma$ is the path $t\mapsto e^{i 2\pi t}$ (via the standard trigonometric covering), then the endpoint difference of any continuous lift of $\gamma$ to $\mathbb{R}$ is $2\pi$.
background
This module builds a local winding (displacement) invariant for paths in the exact TopCat.sphere 1 object. A path is lifted through the covering map that sends $\theta\in\mathbb{R}$ to the trigonometric point on the circle; displacement is how far that lift travels in $\mathbb{R}$.
Concretely, path displacement of a continuous path $\gamma:I\to S^1$ is the difference of the canonical lift at the endpoints $1$ and $0$. The fundamental loop is the once-around path $t\mapsto$ trig-circle-point of $2\pi t$, and the fundamental lift is the explicit linear map $t\mapsto 2\pi t$ on the unit interval.
The key upstream fact is lift independence: displacement 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}$, so the endpoint gap is well-defined.
proof idea
One short rewrite-and-simplify argument. Apply lift independence to the fundamental loop with the explicit linear lift $t\mapsto 2\pi t$ (which is known to cover the fundamental loop by definitional equality). The goal becomes
$2\pi\cdot 1-2\pi\cdot 0=2\pi$
on the real line, which simp closes. No covering uniqueness or deck-group work is redone here; that is already packaged in the lift-independence lemma.
why it matters
This is the surjectivity witness for the winding invariant: the canonical generator maps to a nonzero real. Immediately downstream, dividing by $2\pi$ yields that the winding number of the fundamental loop is exactly $1$, so winding is a left inverse to the fundamental loop class on the nose.
The same identity is reused in the singular-simplex chain: the displacement of the fundamental singular $1$-simplex is one full turn $2\pi$, feeding the statement that the winding invariant is a left inverse to the fundamental class in the chain complex. In the broader Recognition foundation stack this pins the generator of $\pi_1(S^1)$ under the covering-theoretic displacement measure, with no project-local circle replacements or axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.