has
plain-language theorem explainer
Integer multiples of the fundamental once-around loop on the circle are pairwise non-homologous: n·[γ]=0 in H₁(S¹;ℤ) forces n=0. Anyone citing the injective half of H₁(S¹;ℤ)≅ℤ needs this fact. The intended argument reads winding numbers off the covering-space displacement invariant on singular 1-simplices. The declaration is presently a sorry stub, so the claim is scaffolding rather than a finished proof.
Claim. Distinct integer multiples of the once-around generator loop on $S^1$ are never homologous: if $n\cdot[\gamma_{\mathrm{fund}}]=0$ in $H_1(S^1;\mathbb{Z})$, then $n=0$. Equivalently, the comparison map $\mathbb{Z}\to H_1(S^1;\mathbb{Z})$ sending $1$ to the fundamental class is injective. This is only the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$; surjectivity (that the fundamental loop generates $H_1$) is a separate generation statement and is left open.
background
The ambient module lifts the path-level winding and displacement invariant of the circle to singular simplices of the topological 1-sphere. Every continuous map $f:\Delta^1\to S^1$ is reparameterized to a path on the unit interval; its real displacement (equivalently $2\pi$ times winding) is recorded by simplexDisplacement. The companion identity is that this assignment kills boundaries: for every singular 2-simplex $F:\Delta^2\to S^1$, the alternating face sum of displacements vanishes.
That vanishing is the chain-level reason winding descends to homology. Combined with the normalization that the once-around fundamental loop has winding 1, one obtains a homomorphism on 1-cycles that is a left inverse to the fundamental class, i.e. the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The module works entirely with Mathlib singular simplices and path homotopy; no project-local substitute for $S^1$ is introduced. The converse generation half (every 1-cycle homologous to an integer multiple of the fundamental cycle) needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply.
proof idea
Classified as a sorry stub: there is no completed proof body. The intended route, fixed by the module narrative and the doc-comment, is elementary covering-space arithmetic rather than an appeal to a black-box homology computation.
One evaluates the simplex displacement (path displacement after reparameterizing $\Delta^1$) on integer multiples of the fundamental loop. Normalization sends the once-around generator to winding 1, so the multiple $n$ is sent to the integer $n$. Homologous cycles share displacement because displacement kills boundaries (the 2-simplex telescoping identity: the long boundary walk is homotopic rel endpoints inside the convex standard 2-simplex to the direct edge, and displacement is additive and homotopy-invariant). Distinct integers therefore cannot be homologous.
No axioms are planned; the stub is pure unfinished Lean.
why it matters
This is the injective half of the classical computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, obtained by hand from the winding invariant rather than from a general cellular or simplicial package. Inside Recognition Science it anchors the circle as the carrier of a free infinite cyclic homology class, which is the topological substrate for octave and tick bookkeeping on $S^1$ (the eight-tick period $2^3$ in the forcing chain sits on a circle factor).
The module doc is explicit that the companion generation theorem remains open: without surjectivity one has only a split injection $\mathbb{Z}\hookrightarrow H_1(S^1;\mathbb{Z})$, not the full isomorphism. Closing the stub therefore completes the left-inverse half already outlined by simplexDisplacement, the boundary-killing identity, and the fundamental-loop normalization; it does not by itself finish generation.
Downstream graph edges attached to this short name are noisy and should not be read as genuine consumers. The real dependents are later circle-homology and chain-level arguments in the same foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.