fundamentalCycleClass_generates
plain-language theorem explainer
Names the concrete generation property for degree-1 singular homology of the circle: every integer 1-cycle is homologous to an integer multiple of the fundamental once-around cycle. Anyone closing H₁(S¹;ℤ) ≅ ℤ via the winding retraction cites this Prop as the missing geometric half. It is a pure Prop definition, not a proved theorem.
Claim. Every degree-$1$ singular cycle $z$ on $S^1$ with integer coefficients has the same homology class as $n$ times the fundamental once-around class, for some $n \in \mathbb{Z}$. Equivalently: the image of $z$ under the canonical projection from cycles to $H_1(S^1;\mathbb{Z})$ equals the image of $n$ under the integer comparison map $n \mapsto n\cdot[\gamma_{\mathrm{fund}}]$.
background
The module lifts path-level winding on $S^1$ to singular $1$-simplices and proves that displacement kills boundaries of $2$-simplices. Combined with the fact that the once-around loop has winding $1$, this yields a winding homomorphism on $1$-cycles that is a left inverse to the fundamental class map, i.e. the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The integer comparison map sends $n\in\mathbb{Z}$ to $n$ times the homology class of the fundamental singular $1$-cycle (the once-around generator). The chain complex in play is Mathlib's singular chain complex of $\mathrm{TopCat.sphere},1$ with coefficients in $\mathbb{Z}$.
Surjectivity of that comparison map is the generation half. This definition packages generation at the cycle-representative level rather than as bare surjectivity on homology: every cycle's class matches some integer multiple of the fundamental class.
proof idea
No proof: this is a Prop definition. It quantifies over degree-$1$ cycles of the singular integer chain complex of $S^1$ and asserts existence of an integer $n$ such that the homology projection of the cycle equals the image of $n$ under the fundamental homology class map. Downstream lemmas treat the Prop as a hypothesis and discharge geometric consequences from it.
why it matters
This is the concrete missing geometric statement for the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ in the CircleWindingChain development. The module already has the winding retraction (split-injective half); generation closes the isomorphism.
Downstream, assuming this Prop yields surjectivity of the fundamental homology class map, the final Mathlib $H_1$ isomorphism bridge, and the zero-winding filling target. A companion lemma shows that a stronger boundary-decomposition form of generation implies this cycle-class form (the $2$-chain term dies under homology projection).
In the Recognition forcing chain the circle computation is the strict algebraic-topology input toward T8 ($D=3$ spatial dimensions) and the eight-tick octave structure; closing generation removes the last scaffolding gap between winding geometry and Mathlib singular homology of $S^1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.