reducedCellularCircleChainModel_d_eq_zero
plain-language theorem explainer
Every differential of the reduced cellular chain model of the circle vanishes. Anyone computing first homology of that finite model (one copy of ℤ in degree 1, zero elsewhere) cites this to kill the boundary maps before reading off H₁ ≅ ℤ. The proof is a one-line appeal to the Mathlib fact that single-object complexes have zero differentials.
Claim. For every pair of degrees $i,j \in \mathbb{N}$, the differential $d_{i,j}$ of the reduced cellular chain model of the circle (the chain complex over $\mathrm{Mod}\,\mathbb{Z}$ that is $\mathbb{Z}$ in degree $1$ and $0$ elsewhere, with shape $\mathrm{down}\,\mathbb{N}$) is the zero map.
background
The 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 yet feed the strict T8 bridge; the first proved atom is purely 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 groups elsewhere. Differentials of any such single-support complex are forced to be zero by the construction of HomologicalComplex.single. That vanishing is the content of the present lemma and is the prerequisite for reading homology off the lone nonzero chain group.
Upstream, the model is just an abbreviation for the single-degree-one integer complex. Spurious name edges (e.g. species labels or winding classes) are not used in the argument.
proof idea
One-line term proof. Unfold the model to the single-object complex in degree 1 with coefficients $\mathrm{ModuleCat},\mathbb{Z},\mathbb{Z}$, then apply Mathlib's HomologicalComplex.single_obj_d for shape ComplexShape.down ℕ. That lemma states that every differential of a single-object complex is the zero morphism, which is exactly the claim for all degree pairs $(i,j)$.
why it matters
Inside the circle $H_1$ workbench this is the differential-vanishing atom for the reduced cellular model. Sibling results then identify the degree-1 chain group with $\mathbb{Z}$ and conclude that the first homology of the model is $\mathbb{Z}$. That algebraic core is the finite-model half of the intended computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
It does not yet close the T8 spatial-dimension bridge: the module doc is explicit that a real equivalence to Mathlib's singular homology of the circle is still missing. The separate winding-chain injectivity result (infinite order of the once-around loop) supplies one half of the topological isomorphism; generation remains open. No downstream consumers are wired yet; the lemma sits ready for the homology-isomorphism wrappers in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.