simplexWinding_loop_integral
plain-language theorem explainer
A continuous map from the standard 1-simplex to the circle whose two vertices land on the same point has integer winding. Anyone assembling the singular-chain comparison H₁(S¹;ℤ) ≅ ℤ cites this as the generator-level integrality step. The proof is a short reduction: reparameterize Δ¹ to the unit interval and invoke the path-level loop-integrality theorem.
Claim. Let $f:\Delta^1\to S^1$ be continuous. If the two vertices of the standard $1$-simplex satisfy $f(v_1)=f(v_0)$, then the winding number of $f$ is an integer: there exists $k\in\mathbb{Z}$ with $\mathrm{wind}(f)=k$.
background
This module lifts the path-level winding and displacement invariants on $S^1$ to singular simplices of the topological circle. A singular $1$-simplex is a continuous map $f:\Delta^1\to S^1$, where $\Delta^1=\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},2)$. Displacement is obtained by reparameterizing $\Delta^1$ onto the unit interval $I$ and taking the path displacement (endpoint difference of the canonical real lift); winding is that displacement divided by $2\pi$.
At the path level, a closed path $\gamma:I\to S^1$ has displacement equal to an integer multiple of $2\pi$: the two endpoints of the lift lie in the same fiber of the covering $\mathbb{R}\to S^1$, so they differ by an element of the deck group $2\pi\mathbb{Z}$. The present statement is the same fact stated for singular $1$-simplices whose simplicial endpoints coincide.
The module's larger goal is the chain-level identity that winding kills boundaries (alternating face sum of displacement on any singular $2$-simplex vanishes), which together with evaluation on the fundamental loop yields a left inverse to the fundamental class on $H_1(S^1;\mathbb{Z})$.
proof idea
Unfold winding and displacement on a $1$-simplex down to the path obtained by composing $f$ with the standard reparameterization $\mathrm{intervalToSimplex}:I\to\Delta^1$. Apply the path-level theorem that a closed path has integer winding. The loop hypothesis on the path is exactly the given vertex equality: the reparameterization sends $0$ and $1$ to the two vertices of $\Delta^1$, so the two endpoint evaluations reduce by the endpoint lemmas for that reparameterization. The rest is definitional.
why it matters
This is the simplex-level integrality input used by the singular-simplex form of the same statement, which in turn feeds the proof that cycle winding is integral. That integrality is half of the comparison identifying $H_1(S^1;\mathbb{Z})$ with $\mathbb{Z}$: winding on $1$-cycles is a left inverse to the fundamental class once one also has the kills-boundaries identity and evaluation $1$ on the once-around generator.
In the Recognition Science foundation stack this sits inside the circle-winding chain that supplies a concrete integer-valued homology invariant without project-local replacements for $S^1$. The generation (surjectivity) half of the isomorphism still needs a simplicial prism or subdivision operator, which Mathlib singular homology does not yet provide; this lemma does not close that gap, but it is the clean integrality step on generators.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.