cellularCircleAlgebraicH1Certificate

This module is the local workbench for the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It does not yet replace Mathlib's TopCat.sphere 1 singular chains, and it does not feed the strict T8 bridge until a geometric equivalence to that imported object is proved. The first proved atom is purely algebraic: a chain complex supported by $\mathbb{Z}$ in degree 1 has degree-1 homology $\mathbb{Z}$.

Two finite cellular models sit side by side. The reduced model is essentially a single $\mathbb{Z}$ in degree 1 (zero elsewhere). The ordinary model has one integer generator in degree 0 and one in degree 1, with vanishing differentials. Comparison maps include the degree-1 generator into the ordinary complex and collapse degree 0 back down.

The certificate structure records that both models have $H_1\cong\mathbb{Z}$, that those $H_1$ groups are isomorphic to each other, that the reduced complex is a retract of the ordinary one at chain level, and that the collapse is a quasi-isomorphism in degree 1. The remaining Phase 5 gap is only geometric transport from Mathlib singular chains on the circle to this cellular model.

Term-mode structure constructor. Each field is filled by a previously proved proposition-facing lemma:

• reduced_h1_iso_int from the nonempty packaging of the reduced model's $H_1\cong\mathbb{Z}$ isomorphism.
• ordinary_h1_iso_int from the analogous ordinary-model packaging.
• ordinary_h1_iso_reduced_h1 from the algebraic comparison of the two finite models in degree 1.
• reduced_is_retract from the chain-map identity that include-then-collapse is the identity on the reduced complex (proved by from_single_hom_ext and componentwise simplification).
• collapse_quasiIsoAt_one from the quasi-isomorphism-at-1 theorem, which uses Mathlib's zero-differential short-complex criterion: both relevant short complexes have zero differentials in degree 1, and the middle component of the collapse is an isomorphism on the chosen integer generator.

No new algebra is done here; the certificate is the bundle.

Closes the finite cellular algebraic half of the circle-$H_1$ computation inside the Foundation layer. The module doc states the target explicitly: $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ is the missing computation whose singular-chain form is the final strict T8 target (T8 forces $D=3$ spatial dimensions in the forcing chain). This certificate does not yet discharge that target; it only seals the algebraic core so that the remaining work is geometric transport from Mathlib's imported singular chain complex of TopCat.sphere 1 to the cellular model.

No downstream consumers are wired yet (used_by is empty). The natural parent is whatever Phase-5 bridge equates Mathlib singular homology of the circle with these cellular models. Until that bridge exists, the certificate is a checked inventory rather than a link in the forcing chain. It still matters: without the algebraic side closed, the geometric comparison would have nothing rigid to land on.