pathWinding_fundamentalLoop
plain-language theorem explainer
The once-around generator on the unit circle has winding number exactly 1. Anyone normalizing path displacement by a full turn cites this to pin the scale of the winding invariant. The proof rewrites the definition, inserts the known displacement 2π, and divides.
Claim. Let $\gamma_1$ be the fundamental once-around path $t \mapsto (\cos(2\pi t), \sin(2\pi t))$ on $S^1$. Its winding number (path displacement divided by $2\pi$) equals $1$.
background
This module equips paths in the exact TopCat.sphere 1 with a winding/displacement invariant: lift through the covering map given by the standard trigonometric parametrization $\mathbb{R}\to S^1$, then measure how far the lift travels in $\mathbb{R}$. The key technical fact is that displacement from the canonical lift agrees with the endpoint difference of any continuous lift (deck transformations differ by $2\pi\mathbb{Z}$).
The fundamental loop is the standard generator $t\mapsto$ trigCirclePoint$(2\pi t)$. Its path displacement is already known to be one full turn $2\pi$. Path winding is that displacement normalized by $2\pi$, so it is the integer-valued (for closed paths) count of turns.
proof idea
One short tactic proof. Unfold path winding to displacement over $2\pi$. Substitute the upstream identity that the fundamental loop has displacement $2\pi$. The remaining arithmetic is $(2\pi)/(2\pi)=1$, discharged by positivity of $2\pi$ and field_simp.
why it matters
This pins the scale of the local winding invariant: the canonical generator maps to $1$, so winding is a left inverse to the fundamental-loop class on the nose. That is the surjectivity/normalization witness complementary to the displacement statement (displacement $2\pi$).
In the Recognition foundation stack this sits under circle covering and path lifting, the same geometric layer that feeds singular-cone and circle-winding-chain constructions (the next lemma in-file notes that zero winding forces lift endpoints to agree, consumed by that chain). No T0–T8 forcing step is closed here; the result is pure covering-space bookkeeping that later RS geometry can quote without rescaling conventions.
No downstream dependents are recorded yet in the graph; the declaration is a leaf normalization fact ready for closed-path integrality and cone arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.