reducedCellularCircleChainModelXOneIsoInt
plain-language theorem explainer
The degree-1 chain module of the reduced cellular model of the circle is isomorphic to ℤ as a ℤ-module. Anyone assembling the algebraic core of H₁(S¹;ℤ) ≅ ℤ from a single-support complex cites this identification. The body is the standard Mathlib self-isomorphism for the nonzero degree of a single-object complex.
Claim. The chain group in degree $1$ of the reduced cellular circle chain model (one integer generator in degree $1$, zero elsewhere) is isomorphic, in the category of $\mathbb{Z}$-modules, to $\mathbb{Z}$ itself: $X_1 \cong \mathbb{Z}$.
background
This module is a 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 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 chain model is the single-degree complex with object $\mathbb{Z}$ in degree $1$ and zero elsewhere (shape ComplexShape.down ℕ). That model is an explicit finite chain target, not a singular-homology replacement. The present declaration names the degree-$1$ chain group of that model and records its tautological isomorphism to $\mathbb{Z}$.
Upstream, the model is an abbreviation for the single-degree-one integer complex. Related siblings package the homology-level isomorphisms once a quasi-isomorphism or complex isomorphism into that single complex is available.
proof idea
One-line definitional wrapper. Apply Mathlib's HomologicalComplex.singleObjXSelf at degree $1$ for shape ComplexShape.down ℕ and object ModuleCat.of ℤ ℤ. That lemma states that the chain object of a single-support complex, evaluated at its support degree, is definitionally isomorphic to the supporting object. No further rewriting or homology computation is required.
why it matters
Inside the Recognition Science foundation stack, the circle's first homology is the algebraic skeleton behind winding, the eight-tick octave (T7), and the dimensional forcing that yields $D=3$ (T8). This definition pins the degree-$1$ chain group of the finite cellular model to $\mathbb{Z}$, so later lemmas can transport homology isomorphisms onto that model without re-proving the support identification.
The module doc is explicit: the workbench does not yet supply a real equivalence to Mathlib singular homology, and the full $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ bridge remains open on the geometric side. The injective half (infinite order of the once-around class) is already proved elsewhere via the covering-space winding invariant; generation/surjectivity is separate. This atom only fixes the algebraic $X_1$ slot so those bridges have a clean target.
No downstream consumers are wired yet (used_by empty). It sits ready for the homology-of-single-complex and quasi-iso transport siblings in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.