reducedCellularCircleChainModelH1NonemptyIsoInt
plain-language theorem explainer
The reduced cellular chain model of the circle has first homology isomorphic to the integers, packaged as a nonempty-isomorphism certificate. Algebraic H₁ workers cite this when assembling the finite-model half of the circle computation. The proof is a one-line wrapper that inhabits Nonempty with the existing explicit degree-1 isomorphism.
Claim. There is a nonempty isomorphism of $\mathbb{Z}$-modules $H_1(C_\bullet^{\mathrm{red}}(S^1);\mathbb{Z})\cong\mathbb{Z}$, where $C_\bullet^{\mathrm{red}}(S^1)$ is the reduced cellular chain model of the circle (one integer generator in degree $1$, zero elsewhere).
background
This module is the local workbench for the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It does not replace Mathlib's TopCat.sphere 1 and does not feed the strict T8 bridge until a real equivalence to imported singular homology is proved. The first proved atom is algebraic: a chain complex supported by $\mathbb{Z}$ in degree 1 has degree-1 homology $\mathbb{Z}$.
The reduced cellular circle chain model is the finite complex with a single integer generator in degree 1 and zero chain groups elsewhere (implemented as the single-degree-one integer complex). Its ordinary two-cell sibling has generators in degrees 0 and 1 with zero boundary; both remain algebraic finite-chain models until later theorems connect them to topology.
Upstream, an explicit isomorphism already identifies the model's first homology with $\mathbb{Z}$. The present declaration is only the proposition-facing Nonempty packaging of that isomorphism.
proof idea
One-line term proof. The witness is the existing explicit isomorphism from the reduced cellular circle model homology in degree 1 to $\mathrm{ModuleCat}$ of $\mathbb{Z}$ over $\mathbb{Z}$. That isomorphism itself is a thin rename of the single-degree-one integer complex homology isomorphism. No new homology computation occurs here; Nonempty is inhabited by angle-bracketing the prior iso.
why it matters
Feeds the checked certificate for the finite cellular algebraic part of the circle-H1 computation: that certificate records both the reduced and ordinary model H1-nonempty-iso-to-$\mathbb{Z}$ facts. Without this Nonempty form, the certificate structure cannot be filled.
In the Recognition framework this sits in Foundation scaffolding toward identifying algebraic circle homology with the topological object used by the forcing chain. The module doc is explicit that the workbench does not yet replace TopCat.sphere 1 or feed the strict T8 ($D=3$) bridge. The open step remains a quasi-isomorphism or equivalence linking these finite cellular models to Mathlib singular homology of the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.