windingChainMap_fundamentalCycleFreeChain
plain-language theorem explainer
The free-coordinate image of an integer multiple of the fundamental 1-cycle on S¹ has winding number equal to that integer. Anyone tracking the winding homomorphism on free singular chains (rather than on the cycle submodule) cites this. The proof unfolds the free image, cancels the free/chain round-trip via the free isomorphism, and applies the already-proved cycle-level winding identity.
Claim. For every integer coefficient $n$, the winding chain map applied to the free-coordinate image of $n$ times the fundamental singular $1$-cycle on $S^1$ equals $n$ as a real number.
background
This module lifts path-level winding on the circle to singular $1$-simplices of $\mathrm{TopCat.sphere},1$ and proves that winding kills boundaries, so it descends to a homology invariant. Together with the fact that the once-around generator has winding $1$, this supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The fundamental cycle is the lift of the once-around singular $1$-chain into the degree-$1$ cycles of the integer singular chain complex of $S^1$. Its free-coordinate image is obtained by including that cycle into free $C_1$ via the free/chain isomorphism. The winding chain map evaluates displacement (equivalently $2\pi$ times winding) on free singular $1$-chains.
Upstream, cycleWinding_fundamentalCycle already states that the cycle-level winding of $n$ times the fundamental cycle equals $n$. The free isomorphism identifies free and ordinary singular $1$-chains, so the free image is the natural place to run prism and oriented-family calculations.
proof idea
Unfold the free-coordinate image of the fundamental cycle. The free/chain round-trip on that image is the identity: apply congruence of the free isomorphism's hom_inv_id and simplify the composite to the identity map. After rewriting, the goal is exactly the cycle-level statement that winding of $n$ times the fundamental cycle equals $n$, which is discharged by that upstream theorem.
why it matters
Oriented cyclic families (finite sign-oriented closed walks in singular $1$-simplices) build free-prism boundaries by subtracting this free fundamental cycle from a sum of oriented edges. Downstream constructions such as the desired free-prism boundary and winding computations for terminal-return sides need a free-chain form of the fundamental winding identity; this theorem is that form.
In the module's larger program it is a bookkeeping step toward the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding is a left inverse to the fundamental class. The generation/surjectivity half still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply. Within Recognition Science this sits in the Foundation layer supporting the circle computation that feeds dimensional and octave forcing (T7/T8), not a direct physics constant claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.