circleH1ZIsoInt_of_directedCycleTerms
plain-language theorem explainer
The directed-cycle boundary-generation hypothesis is enough to obtain the Mathlib identification $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Anyone closing the singular-homology comparison for the circle cites this reduction. The proof is a one-line composition: directed-cycle terms imply global fundamental-cycle generation, which already yields the integer isomorphism.
Claim. Assume decidable equality on singular $0$- and $1$-simplices of $S^1$. If every directed-cycle free term is homologous, at the singular chain level, to an integer multiple of the fundamental cycle, then the Mathlib comparison realizes $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
background
This module lifts path-level winding on $S^1$ to singular simplices of TopCat.sphere 1. Displacement of a singular $1$-simplex is path displacement after reparameterizing $\Delta^1$ to the unit interval. The key identity is that displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes, by convexity of $\Delta^2$ and homotopy invariance of path displacement.
Together with the fact that winding sends the once-around loop to $1$, this gives a left inverse to the fundamental class (the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$). Surjectivity is the generation half: every singular $1$-cycle must be homologous to an integer multiple of the fundamental cycle.
The hypothesis here packages a local geometric target: each directed-cycle free term equals a $2$-boundary plus an integer multiple of the fundamental cycle. Upstream, that local statement implies global fundamental-cycle boundary generation, which in turn closes the Mathlib integer isomorphism.
proof idea
One-line term wrapper. Apply the reduction that turns directed-cycle-term generation into global fundamental-cycle boundary generation, then feed that into the already-proved theorem that fundamental-cycle boundary generation yields the Mathlib circle $H_1$ integer isomorphism. No new geometric work occurs at this node.
why it matters
This is the last packaging step before the final Mathlib $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ comparison in the circle winding chain. The module already has the kills-boundaries identity and the winding left-inverse; what remains is generation. The doc-comment states that the one-directed-cycle generation theorem is enough for that final computation.
Downstream use is not yet wired in this graph snapshot (used_by empty), but the declaration sits directly above the Mathlib cohomology bridge isomorphism. In the broader Recognition foundation it supplies the singular-homology half of the circle's integer winding, the topological input that later interfaces with eight-tick and octave structure. The open geometric obligation is the directed-cycle term hypothesis itself (local prism / closed-walk homology), not this reduction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.