reducedCellularToOrdinaryChainMap

This module is the local workbench for the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It stays algebraic: it does not replace Mathlib's TopCat.sphere 1 and does not feed the strict T8 bridge until a real equivalence to singular homology is proved.

The reduced cellular circle model is the single-degree complex with $\mathbb{Z}$ in degree 1 and zero elsewhere. The ordinary cellular circle model places $\mathbb{Z}$ in degrees 0 and 1, nothing higher, and sets every differential to zero. The ordinary degree-1 chain group is identified with $\mathbb{Z}$ by a definitional isomorphism; all its differentials vanish by reflexivity.

The map defined here includes the reduced model into the ordinary one, so that later one can prove the reduced complex is a chain-level retract of the ordinary complex in the degree relevant to circle homology.

One-shot construction via HomologicalComplex.mkHomFromSingle. The degree-1 component is the inverse of the ordinary model's degree-1 integer-generator isomorphism. The required commutation-with-differentials side condition is discharged by simp against the theorem that every differential of the ordinary cellular circle model is zero.

This inclusion is half of the chain-level retract between the reduced and ordinary cellular models. Downstream, the composite reduced-then-ordinary is the identity on the reduced complex, and the opposite composite is the identity in degree 1 (the degree that carries $H_1$). Both facts feed the structure CellularCircleAlgebraicH1Certificate, which packages: reduced $H_1\cong\mathbb{Z}$, ordinary $H_1\cong\mathbb{Z}$, ordinary collapses to reduced in degree 1, and the reduced model is a retract of the ordinary one.

That certificate closes the finite cellular algebraic core of the circle-$H_1$ computation. The remaining Phase 5 gap is geometric transport from Mathlib singular chains on the circle to this cellular model; nothing here touches T8 or the forcing chain directly.