reducedCellularCircleChainModel
plain-language theorem explainer
Names the reduced cellular chain model of the circle: the integer chain complex with a single generator in degree 1 and zeros elsewhere. Anyone computing algebraic H₁ of finite circle models cites this as the target complex. It is a one-line alias of the single-support degree-1 integer complex.
Claim. The reduced cellular chain model of the circle is the homological complex of $\mathbb{Z}$-modules (shape $\mathrm{down}\,\mathbb{N}$) equal to the complex supported only in degree $1$ by $\mathbb{Z}$.
background
This module is the 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 single-support integer complex is the algebraic core of the finite circle model before topological transport. It is built as the image of $\mathbb{Z}$ under Mathlib's HomologicalComplex.single at degree 1, so all differentials vanish and only the degree-1 chain group is nonzero. The reduced cellular model is exactly that complex, viewed as the finite chain-model target for circle $H_1$.
proof idea
One-line abbreviation: the reduced cellular circle chain model is defined to be the single degree-1 integer complex. No further construction or proof obligations; all differential and homology facts are inherited from that upstream abbrev and Mathlib's single-object complex API.
why it matters
This is the reduced finite cellular target against which ordinary two-cell models are compared. Downstream, the algebraic certificate records that the reduced model has $H_1\cong\mathbb{Z}$, that the ordinary model collapses to it in degree 1, and that the collapse is a quasi-isomorphism at degree 1. Explicit parents include the reduced $H_1\cong\mathbb{Z}$ isomorphisms, the ordinary-to-reduced chain map and its quasi-iso-at-1 theorem, and the structure packing the closed algebraic half of the circle-$H_1$ computation.
In the Recognition foundation chain this sits under the circle winding / $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ work that supports dimensional and octave forcing (T7–T8). The remaining Phase 5 gap is geometric transport from Mathlib singular chains on the topological circle to this cellular model; the present definition only names the algebraic endpoint of that transport.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.