reducedCellularCircleChainModelXZeroIsZero
plain-language theorem explainer
The reduced cellular chain model of the circle has vanishing chain group in degree 0. Anyone assembling the finite algebraic model for $H_1(S^1;\mathbb{Z})$ cites this atom. The proof is a one-line application of Mathlib's fact that a single-object complex supported in degree 1 is zero off that degree.
Claim. Let $C_\bullet$ be the reduced cellular chain model of the circle: the chain complex of $\mathbb{Z}$-modules with $C_1 \cong \mathbb{Z}$ and $C_n = 0$ for $n \neq 1$. Then the degree-$0$ object $C_0$ is the zero object in $\mathbf{Mod}_{\mathbb{Z}}$.
background
This module is a Mathlib-style workbench aimed at the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It does not replace TopCat.sphere 1 and does not feed the strict T8 bridge until a real equivalence to Mathlib 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 model is the finite target complex with a single integer generator in degree 1 and zero elsewhere. It is an abbreviation for the single-degree-one integer complex under the downward natural grading. Degree-0 vanishing is the complementary structural fact to the degree-1 identification $C_1\cong\mathbb{Z}$.
proof idea
One-line term proof. Apply Mathlib's HomologicalComplex.isZero_single_obj_X to the single complex of shape ComplexShape.down ℕ supported at degree 1 with value $\mathrm{ModuleCat},\mathbb{Z},\mathbb{Z}$. Instantiate the off-support degree as 0 and discharge $0\neq 1$ by norm_num. No local lemmas are needed beyond the model abbreviation.
why it matters
This is a structural atom of the reduced cellular circle model inside the $H_1(S^1;\mathbb{Z})$ workbench. Together with the companion fact that the degree-1 chain group is $\mathbb{Z}$, it pins the support of the finite algebraic target used for the homology computation. No downstream theorems currently depend on it (used-by is empty); it sits as infrastructure for later quasi-isomorphism and homology-isomorphism bridges in the same module.
Per the module doc, none of this yet replaces singular homology of the topological circle or feeds the strict T8 ($D=3$) bridge. The separate winding-chain injectivity result (infinite order of the once-around loop) remains the hand-proved half of $H_1\cong\mathbb{Z}$; surjectivity/generation is still open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.