circleH1ZNonzero
plain-language theorem explainer
Names the proposition that the first singular homology of the topological circle with integer coefficients is a nonzero ℤ-module. Dimension-forcing and T8 bridge authors cite it as the Mathlib nonvanishing obligation before the concrete S¹ encoding can be retired. The body is a one-line Prop abbreviation: negation of IsZero on the Mathlib singular-homology object.
Claim. The proposition that $H_1(S^1;\mathbb{Z})$, realized as the value of Mathlib's singular homology functor at degree $1$ on the topological $1$-sphere, is not the zero object in the category of $\mathbb{Z}$-modules.
background
The module MathlibCohomologyBridge records the exact backend Mathlib must supply before Recognition Science can replace its concrete $S^1$ cohomology encoding. Mathlib already exposes the singular homology functor API; T8 needs a genuine computation of the (reduced) cohomology of the circle and the Alexander-duality link from circle-complement homology to that group.
The companion abbreviation circleH1Z is the concrete Mathlib object: first singular homology of the topological circle with integer coefficients, written as the degree-$1$ value of singularHomologyFunctor on TopCat.sphere 1 in ModuleCat ℤ. Nonvanishing of that object is the minimal computational fact required before the current bridge can be swapped out. The module deliberately refuses to fake the backend by reusing the existing Alexander-duality nonvanishing certificate.
proof idea
Definitional, not a proof. The Prop is the literal negation of Mathlib's CategoryTheory.Limits.IsZero applied to circleH1Z. No tactics, no lemmas: a one-line abbreviation that packages the nonvanishing claim as a named target for downstream discharge.
why it matters
This is the named nonvanishing target that closes T8's Mathlib circle-$H_1$ obligation. Downstream, circle_h1_nonzero asserts the target is closed unconditionally via the complete forcing chain. The CircleWindingChain suite discharges it under cyclic-edge-list, extraction-step, large-support, and zero-winding hypotheses, and finally unconditionally by identifying circleH1Z with Mathlib sphere homology and invoking homologyOne_nonzero.
In the forcing chain, T8 forces $D=3$ spatial dimensions; the circle homology computation is the topological input that makes the Mathlib-backed replacement of the concrete $S^1$ bridge legitimate. Sibling certificates (CircleH1TargetCertificate, iso-to-$\mathbb{Z}$ routes) strengthen nonvanishing to a full $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ computation once Mathlib supplies it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.