circleH1ZNonzero_unconditional
plain-language theorem explainer
Singular first homology of the circle with integer coefficients is nonzero, as a Mathlib-facing Prop, with no remaining hypotheses. Forcing-chain and cohomology-bridge authors cite it to close the strict T-1-to-T8 frontier. The proof transfers the local nonvanishing theorem across the identity isomorphism between the Mathlib singular-homology functor object and the project's chain-complex homology.
Claim. The Mathlib singular homology object $H_1(S^1;\mathbb{Z})$ is not the zero module: $\neg\mathrm{IsZero}\bigl(H_1^{\mathrm{sing}}(S^1;\mathbb{Z})\bigr)$. Equivalently, the first homology of the integer singular chain complex of the topological $1$-sphere is nonzero.
background
The module builds a winding invariant on singular $1$-simplices of $\mathrm{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 alternating face sums of displacements vanish on every singular $2$-simplex (winding kills boundaries). Together with the fact that the once-around generator has winding $1$, this yields a left inverse to the fundamental class, hence the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Upstream, homologyOne_nonzero already proves the local chain-complex homology is nonzero: the fundamental homology class maps under the winding comparison to $1\in\mathbb{R}$, so the module cannot be zero. The Mathlib bridge packages nonvanishing as the Prop $\neg\mathrm{IsZero}(\mathrm{circleH1Z})$. An identity isomorphism identifies the Mathlib singular-homology functor value on the $1$-sphere with that local homology object.
proof idea
Term-mode one-liner. Assume the Mathlib object is zero. Transport that zero hypothesis across the symmetric identity isomorphism singularHomologyFunctorSphereOneIntIsoHomologyOne (which is Iso.refl) to obtain that the local sphereOneSingularIntChainComplex.homology 1 is zero. Discharge the contradiction by applying homologyOne_nonzero, whose argument uses only the mono half of the fundamental class (winding sends it to $1$, not the generation/surjectivity half).
why it matters
This is the concrete circle-$H_1$ computation the strict T-1-to-T8 frontier was waiting on. Downstream, mathlibCircleLinkingBackend_unconditional builds the Mathlib circle-linking backend object straight from this theorem, and complete_forcing_chain_tminus2_to_t8 records it as the circle_h1_nonzero field of the public T-2-through-T8 forcing certificate. In the Recognition forcing chain, T7 (eight-tick octave) and T8 ($D=3$) sit on topological structure that needs a genuine nonzero $H_1(S^1;\mathbb{Z})$; discharging the Mathlib nonvanishing Prop unconditionally removes the last external hypothesis on that link. Generation/surjectivity of the integer comparison map remains open on the Mathlib side (needs prism/subdivision), but nonvanishing does not depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.