circle_h1_nonzero
plain-language theorem explainer
The first singular homology of the circle with integer coefficients is nonvanishing as a Mathlib object. Anyone citing the T8 cohomology bridge, the Mathlib circle-linking backend, or the public T-2–T8 forcing certificate needs this fact. The proof is a one-line field projection from the complete forcing-chain certificate.
Claim. The Mathlib singular-homology object $H_1(S^1;\mathbb{Z})$ is not the zero object: $\neg\mathrm{IsZero}(H_1(S^1;\mathbb{Z}))$. Equivalently, the first singular homology of the circle with integer coefficients is nonvanishing.
background
The Foundation aggregator exposes the T-2 through T8 core and the Mathlib circle-H1 closure for T8, without re-exporting later physics layers. T8 in the forcing chain forces $D=3$ spatial dimensions; the circle's first homology is the algebraic witness that a nontrivial linking/winding class exists in that dimension.
The target proposition circleH1ZNonzero is the concrete Mathlib nonvanishing statement: the singular-homology object of $S^1$ with $\mathbb{Z}$ coefficients is not zero in the category. Upstream, the complete T-2–T8 forcing certificate already packages this as an unconditional field, sourced from the circle-winding chain's unconditional nonvanishing lemma. A stronger sibling target asserts the full isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
proof idea
One-line term-mode projection. The complete forcing-chain theorem builds a structure whose circle_h1_nonzero field is already filled by the unconditional circle-winding nonvanishing result. This declaration simply reads that field off the structure instance, with no extra algebraic work.
why it matters
Closes T8's Mathlib circle-H1 nonvanishing replacement unconditionally, as stated in the doc-comment. Downstream, the Mathlib circle-linking backend structure requires this nonvanishing as a field; a proof of it is enough to inhabit the backend, and the backend is nonempty if and only if this proposition holds. The checked cohomology-bridge contract and the public complete T-2–T8 forcing certificate both depend on it. In the Recognition forcing chain, T8 forces $D=3$; nonvanishing of $H_1(S^1;\mathbb{Z})$ is the homology-side certificate that a nontrivial circle class (linking/winding) survives in that dimension, enabling the singular-homology API path that will replace the concrete $S^1$ encoding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.