ordinaryCellularCircleChainModelXSuccSuccIsZero
plain-language theorem explainer
In the ordinary two-cell cellular chain model of the circle, every chain group in degree two or higher is the zero object in ModuleCat ℤ. Anyone building H₁ of this finite algebraic model cites this vanishing. The proof unfolds the piecewise definition of the complex and applies the standard fact that the zero module is zero.
Claim. For every natural number $n$, the degree-$(n+2)$ object of the ordinary cellular circle chain complex (one $\mathbb{Z}$ in degree $0$, one $\mathbb{Z}$ in degree $1$, zero elsewhere, zero differentials) is a 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 yet replace TopCat.sphere 1 or feed the strict T8 bridge; the first proved atom is the algebraic core of a finite circle chain model.
The ordinary cellular circle chain model is the two-cell complex with $X_0\cong\mathbb{Z}$, $X_1\cong\mathbb{Z}$, $X_k=0$ for $k\ge 2$, and all differentials zero. It remains a purely algebraic finite-chain model until a later theorem connects it to Mathlib singular homology of the circle.
IsZero is the categorical zero-object predicate in the module category over $\mathbb{Z}$. Vanishing of high-degree chain groups is the elementary support statement needed before computing homology in degree one.
proof idea
Term/tactic hybrid, two steps. Unfold the definition of the ordinary cellular circle chain model: for index $n+2\ge 2$ the piecewise clause returns the zero module. Then apply the standard lemma that the zero object of $\mathbf{Mod}_{\mathbb{Z}}$ is zero. No differential or homology computation is involved.
why it matters
Supports the algebraic core of the circle $H_1$ workbench: a complex supported only in degrees $0$ and $1$ with zero boundary has $H_1\cong\mathbb{Z}$. That atom is the first proved piece toward a Mathlib-linked computation of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
In the Recognition forcing chain, T7 (eight-tick octave, period $2^3$) and T8 ($D=3$) sit downstream of circle/periodicity structure; this lemma is scaffolding for a rigorous singular-homology bridge, not yet that bridge. No parent theorems currently depend on it (used_by is empty). The open gap remains a real equivalence from this finite model to Mathlib's imported singular homology of the 1-sphere.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.