cycleWinding_integral_unconditional
plain-language theorem explainer
Every singular 1-cycle on S¹ has integer-valued winding, with no residual finite-flow hypothesis. Anyone assembling the Mathlib comparison H₁(S¹;ℤ) ≅ ℤ cites this as the split-injective half's integrality step. The proof is a one-line discharge: feed the unconditional directed-cycle kernel decomposition into the conditional integrality theorem.
Claim. Every singular $1$-cycle $z$ on $S^1$ has integer winding: there exists $n \in \mathbb{Z}$ such that the real winding number of $z$ equals $n$. No finite-flow or free-boundary-kernel hypothesis remains.
background
The module lifts path-level winding from CircleWinding to singular simplices of $S^1$. Displacement of a singular $1$-simplex is the path displacement of its reparameterization $\Delta^1 \to [0,1]$; the key identity is that alternating face sums of any singular $2$-simplex vanish (winding kills boundaries), by convexity of $\Delta^2$ and homotopy invariance of path displacement.
The proposition cycleWinding_integral asserts that every integer singular $1$-cycle has winding in $\mathbb{Z} \subset \mathbb{R}$. Upstream, a conditional theorem already derives this from free-boundary-kernel decomposition into directed cycles. That decomposition itself is now proved unconditionally by $\ell^1$-induction and oriented closed-walk extraction, under classical decidable equality on singular simplices.
Together with the fundamental loop mapping to winding $1$, integrality supplies the left-inverse half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$. The remaining geometric input for full isomorphism is the zero-winding filling statement.
proof idea
One-line term proof under classical. Apply the conditional theorem that free-boundary-kernel decomposition into directed cycles implies integer winding on all singular $1$-cycles, supplying as hypothesis the already-proved unconditional decomposition (strong induction on $\ell^1$ size, peeling directed cycles). Classical mode supplies the DecidableEq instances the decomposition needs on singular $0$- and $1$-simplices. No further geometric work occurs here.
why it matters
This closes the finite-flow half of the Mathlib $H_1(S^1;\mathbb{Z})$ comparison unconditionally: no axiom, sorry, or project-local circle replacement remains on the integrality side. Downstream, circleH1ZIsoInt_of_zeroWinding_bounds feeds this result plus the zero-winding filling hypothesis into the full integer isomorphism bridge.
In the Recognition Science foundation stack, a clean integer winding on singular cycles is the algebraic backbone for the eight-tick octave and circle-valued phase bookkeeping that later force $D=3$ and the $\varphi$-ladder structure. The only open geometric stub left on this path is zeroWindingCycles_bound (every zero-winding cycle is a singular $2$-boundary), which needs subdivision or prism machinery Mathlib singular homology does not yet expose.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.