ordinaryCellularCircleChainModel
plain-language theorem explainer
Defines the ordinary two-cell cellular chain complex of the circle over ℤ: free of rank one in degrees 0 and 1, zero elsewhere, with vanishing differential. Anyone computing H₁(S¹;ℤ) algebraically or bridging Mathlib singular chains to a finite model cites this object. The body is a pure case-split construction of the complex, not a proof.
Claim. The ordinary cellular chain model of the circle is the homological complex of $\mathbb{Z}$-modules (shape $\mathrm{down}\,\mathbb{N}$) whose degree-$n$ term is $\mathbb{Z}$ if $n\in\{0,1\}$ and $0$ otherwise, with every boundary map equal to zero.
background
This module is the local workbench for the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It does not replace Mathlib's TopCat.sphere 1 and does not feed the strict T8 bridge until a real equivalence to the imported singular homology object is proved. The first proved atom in the module is algebraic: a chain complex supported by $\mathbb{Z}$ in degree 1 has degree-1 homology $\mathbb{Z}$.
The ordinary model is the unreduced two-cell picture of the circle: one integer 0-cell generator and one integer 1-cell generator, no higher cells, and zero boundary. A sibling reduced model collapses the degree-0 summand; both sit inside the same finite-chain algebra before any geometric transport.
Downstream certificates treat this complex as the algebraic target of a chain homotopy equivalence (or quasi-isomorphism at degree 1) from Mathlib's singular chains on the 1-sphere.
proof idea
Definitional construction only. Chain groups are assigned by a two-branch degree test: $\mathbb{Z}$ at $n=0$ and $n=1$, the zero module otherwise. Every differential component is the zero morphism of $\mathbb{Z}$-modules. No lemmas are applied; the complex axioms hold because all composites of zero maps vanish.
why it matters
This is the ordinary finite cellular target for the circle-$H_1$ workbench. The algebraic certificate structure records that both the reduced and ordinary models have $H_1\cong\mathbb{Z}$, that the ordinary model collapses to the reduced one in degree 1, and that the reduced model is a chain retract of the ordinary one; the remaining Phase 5 gap is geometric transport from Mathlib singular chains on the 1-sphere to this model.
The geometric bridge is exactly a nonempty chain homotopy equivalence from the singular complex of TopCat.sphere 1 into this ordinary model. Conditional theorems then turn such a homotopy equivalence (or a degree-1 quasi-isomorphism) into the Mathlib-facing proposition $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. In the Recognition forcing chain this closes the algebraic half of the circle computation that T8-style dimension and octave arguments rely on once the singular bridge is filled.
Until that bridge is proved, the object remains a pure algebraic finite-chain model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.