reducedCellularCircleChainModelXSuccSuccIsZero
plain-language theorem explainer
For every natural number n, the chain group of the reduced cellular circle model in degree n+2 is the zero object among ℤ-modules. Anyone building the algebraic model of H₁(S¹; ℤ) cites this to kill all degrees above 1. The proof is a one-line application of Mathlib's vanishing lemma for single-object complexes off their support degree, with n+2 ≠ 1 discharged by omega.
Claim. For every $n \in \mathbb{N}$, the degree-$(n+2)$ chain group of the reduced cellular circle model (the chain complex with a single copy of $\mathbb{Z}$ in degree $1$ and zeros elsewhere, shaped by $\mathrm{ComplexShape.down}\,\mathbb{N}$) is the zero object in $\mathbf{Mod}_{\mathbb{Z}}$.
background
This module is the local Mathlib-style workbench for 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 one integer generator in degree 1 and zero elsewhere. It is an abbreviation for the single-degree-1 integer complex in the category of $\mathbb{Z}$-modules, with differentials oriented by the down complex shape on $\mathbb{N}$. Sibling facts already record that the degree-1 group is $\mathbb{Z}$ and the degree-0 group is zero; this declaration extends vanishing to every degree at least 2.
proof idea
One-line term proof. Apply Mathlib's HomologicalComplex.isZero_single_obj_X to the single-object complex at degree 1 with coefficients ModuleCat.of ℤ ℤ, evaluated at index $n+2$. The side condition $n+2\neq 1$ is discharged by omega. No custom lemmas are needed beyond the model being that single complex.
why it matters
Closes the higher-degree half of the reduced cellular circle model: once degrees $\ge 2$ and degree 0 are zero and degree 1 is $\mathbb{Z}$, the complex is algebraically ready for the homology-isomorphism lemmas already in the module (quasi-iso and single-complex homology transfers). That package is the algebraic core toward $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
In the Recognition framework this sits in Foundation scaffolding for circle topology, not yet on the forcing chain. The module header is explicit that the workbench does not feed the strict T8 ($D=3$) bridge until equivalence to Mathlib's singular homology of the 1-sphere is proved. No downstream consumers are wired yet; the declaration is inventory for that future bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.