CellularCircleAlgebraicH1Certificate
plain-language theorem explainer
A Prop certificate packaging the algebraic closure of the finite cellular models for circle H₁: both reduced and ordinary models satisfy H₁ ≅ ℤ, they are mutually isomorphic in degree 1, the reduced model is a chain retract of the ordinary one, and the collapse map is a quasi-isomorphism at degree 1. Anyone citing the algebraic half of the S¹ homology computation uses this bundle. As a structure definition there is no proof body; the companion theorem fills the five fields from prior isomorphisms and chain-map identities.
Claim. A certificate asserting five facts about the finite cellular chain models of the circle: (i) the reduced model has $H_1 \cong \mathbb{Z}$; (ii) the ordinary two-cell model has $H_1 \cong \mathbb{Z}$; (iii) those two degree-1 homology modules are isomorphic; (iv) the reduced model is a chain retract of the ordinary model via the inclusion and collapse maps; (v) the collapse map is a quasi-isomorphism in degree $1$.
background
This module is the local Mathlib-style workbench for the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Per the module doc, it does not replace the topological circle and does not feed the strict T8 bridge until a real equivalence to Mathlib's singular homology object is proved.
The reduced cellular circle model is a chain complex with a single integer generator in degree 1 and zero elsewhere. The ordinary cellular circle model has one integer generator in degree 0, one in degree 1, no higher groups, and zero boundary. The collapse chain map kills the degree-0 generator and retains the degree-1 circle generator; the inclusion map embeds the reduced model into the ordinary one.
The first proved atom in the module is that a chain complex supported by $\mathbb{Z}$ in degree 1 has degree-1 homology $\mathbb{Z}$. The certificate packages that algebraic core for both models together with the retract and quasi-isomorphism relations between them.
proof idea
Structure definition (a Prop bundle), not a proved theorem: no proof body. It declares five fields that must be inhabited: nonempty isomorphisms of both models' $H_1$ with $\mathbb{Z}$ as $\mathbb{Z}$-modules, a nonempty isomorphism between those homology modules, the retract identity (inclusion composed with collapse equals the identity on the reduced model), and the quasi-isomorphism-at-1 property of the collapse map. The companion theorem constructs an instance by supplying prior lemmas for the reduced and ordinary $H_1\cong\mathbb{Z}$ facts, then the remaining retract and quasi-iso fields from the chain-map constructions.
why it matters
Closes the finite cellular algebraic part of the circle-$H_1$ computation. Downstream, the checked-certificate theorem builds an instance of this structure from the reduced and ordinary $H_1$ isomorphisms and the chain-map identities. The doc-comment states the remaining Phase 5 gap is only geometric transport from Mathlib's singular chains on the topological circle to this cellular model. Until that transport lands, the workbench does not feed the strict T8 ($D=3$) bridge. In the Recognition forcing chain a clean $H_1(S^1)\cong\mathbb{Z}$ is the algebraic prerequisite linking circle topology to the eight-tick octave and dimensional forcing; this certificate locks the algebraic half so the geometric half can be attacked in isolation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.