fundamentalCycleFreeChain
plain-language theorem explainer
Maps an integer coefficient n to the free-module image of n times the once-around fundamental 1-cycle on S¹. Downstream free-coordinate prism and winding-map lemmas cite it as the explicit generator chain. The body is a three-map composition: scale the fundamental cycle, include cycles into C₁, then send to the free module on singular 1-simplices.
Claim. For each integer $n$, write $\gamma_n$ for the free $\mathbb{Z}$-module chain on singular $1$-simplices of $S^1$ obtained by taking $n$ times the fundamental singular $1$-cycle, including it into $C_1(S^1;\mathbb{Z})$, and transporting along the canonical map from the singular chain group to the free module on singular $1$-simplices.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries, so winding descends to a homology invariant. That invariant is a left inverse to the fundamental class and gives the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$; generation (surjectivity) needs free-coordinate prism work.
The singular integer chain complex of $\mathrm{TopCat.sphere},1$ is the Mathlib object whose degree-$1$ homology is the strict T8 target. The fundamental cycle is that complex's once-around generator, lifted into the cycle object via a zero-boundary proof. The free module on actual singular $1$-simplices is the explicit coordinate space used for prism and generation arguments; the map from $C_1$ sends each coproduct summand to the corresponding free generator.
Composing those pieces yields a concrete free chain for every integer multiple of the fundamental class, without leaving the singular-chain setting.
proof idea
Pure definitional composition, no tactics. Start from the fundamental cycle as a morphism $\mathbb{Z}\to Z_1$, apply it to the coefficient $n$, include the resulting cycle into degree-$1$ chains via the cycles inclusion, then push forward along the canonical map from the singular chain group to the free module on singular $1$-simplices. The result is the free-coordinate image of $n$ times the once-around generator.
why it matters
Supplies the free-coordinate avatar of integer multiples of the fundamental class used throughout the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The identification theorem proves this free chain equals $n$ times the geodesic free chain from $0$ to $2\pi$. Oriented cyclic family terms and the free-prism generation theorem (Phase 5 checklist) consume it when correcting path-cone residuals. The winding-chain map applied to this object recovers the integer coefficient, closing the left-inverse half already obtained from simplex displacement killing boundaries. In the forcing chain this is foundation for the circle homology input to T8 ($D=3$), not a physics constant claim itself. Generation remains the open half; this definition is the explicit generator side of that comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.