homologyOne_nonzero
plain-language theorem explainer
The degree-1 singular homology of the circle with integer coefficients is nonzero as a ℤ-module. Researchers closing the strict T8 frontier against Mathlib's singular homology cite this nonvanishing. The argument assumes the homology object is zero, pushes the fundamental class through the winding comparison (which evaluates to 1 in ℝ), and obtains the contradiction 1 = 0.
Claim. The degree-$1$ homology of Mathlib's singular chain complex of $S^1$ with coefficients in $\mathbb{Z}$ is not the zero object in the category of $\mathbb{Z}$-modules.
background
This module lifts the path-level winding invariant on $S^1$ to singular simplices. Each singular 1-simplex gets a real displacement (equivalently $2\pi$ times winding) by reparameterizing $\Delta^1$ to the unit interval; the key identity is that this displacement vanishes on boundaries of 2-simplices, by a telescoping homotopy inside the convex standard 2-simplex. That makes winding a homology invariant.
The fundamental homology class is the class of the once-around generator. Composing it with the winding map on homology recovers the map $\mathbb{Z}\to\mathbb{R}$ that sends $1$ to $1$. The module under study is sphereOneSingularIntChainComplex.homology 1, definitionally Mathlib's singular $H_1(S^1;\mathbb{Z})$.
Nonvanishing needs only existence of one nonzero class (the injective/split half already proved). It does not need the generation half that every 1-cycle is homologous to an integer multiple of the fundamental cycle.
proof idea
Assume for contradiction that the degree-1 homology object is zero. Then the fundamental homology class is the zero morphism. Its composite with the winding homology map is therefore zero. Rewrite that composite via the identity that it equals the comparison map $\mathbb{Z}\to\mathbb{R}$ sending $1\mapsto 1$. Evaluate the resulting equality of module morphisms at $1\in\mathbb{Z}$; simplification yields $1=0$ in $\mathbb{R}$, a contradiction. The only substantive inputs are the fundamental class, the winding comparison identity, and zero-object cancellation.
why it matters
This is the concrete circle-$H_1$ nonvanishing the strict T-1-to-T8 frontier was waiting on. Downstream, circleH1ZNonzero_unconditional reduces the imported Mathlib bridge predicate exactly to this theorem, using the definitional equality of the bridge object with the singular chain homology. In the Recognition forcing chain, T8 forces $D=3$ spatial dimensions; the circle computation is the topological witness that the octave/winding structure is not homologically trivial.
The result is unconditional: no axioms, no sorry, and independent of the still-open generation/surjectivity half (simplicial prism subdivision). It closes the nonvanishing side of the split-injective comparison $H_1(S^1;\mathbb{Z})\hookrightarrow\mathbb{R}$ without claiming the full isomorphism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.