ordinaryCellularToReducedChainMap
plain-language theorem explainer
The ordinary two-cell cellular model of the circle maps onto the reduced model by killing the degree-0 generator and keeping the degree-1 generator. Algebraic topologists computing H₁(S¹; ℤ) via finite chain models cite this collapse. Construction is a one-line Mathlib wrapper into a single-degree complex, using the degree-1 identification with ℤ and vanishing of all differentials.
Claim. There is a chain map from the ordinary cellular chain complex of the circle ($\mathbb{Z}$ in degrees $0$ and $1$, zero differentials) to the reduced cellular complex ($\mathbb{Z}$ only in degree $1$) that collapses the degree-$0$ generator and retains the degree-$1$ generator via the canonical identification of the degree-$1$ chain group with $\mathbb{Z}$.
background
This module is the local workbench for the algebraic core of $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 geometric equivalence to singular homology is proved. The first proved atom is that a chain complex supported by $\mathbb{Z}$ in degree 1 has degree-1 homology $\mathbb{Z}$.
The ordinary cellular circle model is the two-cell complex with one integer generator in degree 0, one in degree 1, no higher groups, and zero boundary. The reduced model is the single-degree complex with $\mathbb{Z}$ only in degree 1 (an abbreviation of the single-degree-one integer complex). All differentials of the ordinary model are definitionally zero.
The degree-1 chain group of the ordinary model is identified with $\mathbb{Z}$ by a definitional eqToIso. The reduced model is the natural target for collapsing the unused degree-0 cell while keeping the circle generator that computes $H_1$.
proof idea
One-line construction via Mathlib's HomologicalComplex.mkHomToSingle. The degree-1 component is the forward map of the ordinary model's degree-1 isomorphism to $\mathbb{Z}$. The compatibility obligation (that the source differentials vanish so the map lands in a single complex) is discharged by simp on the theorem that every differential of the ordinary cellular circle model is zero.
why it matters
This collapse is the chain-level bridge between the two finite cellular models used in the algebraic half of the circle-$H_1$ computation. Downstream it supplies the degree-1 component identity (modulo the single-complex iso), the quasi-isomorphism at degree 1 (via Mathlib's zero-differential short-complex criterion), and both composite identities that make the reduced model a chain retract of the ordinary one in the degree relevant to $H_1$.
Those facts assemble into the CellularCircleAlgebraicH1Certificate: reduced and ordinary models both have $H_1\cong\mathbb{Z}$, ordinary collapses to reduced in degree 1, and reduced is a retract of ordinary. The remaining Phase 5 gap named by that certificate is only geometric transport from Mathlib singular chains on the topological circle to this cellular model. Within Recognition Science this is scaffolding for the circle homology atom that later supports octave and dimension forcing (T7/T8), not a physics claim by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.