h0_pt_iso_int

In this module, singular homology with integer coefficients is packaged as an abbreviation: for a topological space $X$ and degree $n$, one takes the degree-$n$ homology of the singular chain complex of $X$. The local Stage A goal is the classical computation of the homology of a point, which anchors later sphere and Mayer–Vietoris arguments.

Upstream, the path-connected case is already available: for any path-connected $X$, the augmentation map induces an isomorphism $H_0(X;\mathbb{Z})\cong\mathbb{Z}$. Its doc-comment states exactly that: "$H_0(X)\cong\mathbb{Z}$ for a path-connected space, via the augmentation." A one-point space is path-connected, so the general result applies verbatim.

The target is the category of $\mathbb{Z}$-modules, so the isomorphism is an isomorphism of modules (equivalently of abelian groups), not merely a bijection of underlying sets.

One-line wrapper: instantiate the path-connected isomorphism at the one-point space TopCat.of Unit. Path-connectedness of a singleton is automatic in the typeclass instance search, so the augmentation isomorphism specializes immediately to $H_0(\mathrm{pt})\cong\mathbb{Z}$. No extra diagram chase or chain-level work is done here.

Stage A of the singular-sphere development records the classical base case $H_0(\mathrm{pt})\cong\mathbb{Z}$ (and, nearby, vanishing in positive degrees). That base case is the starting rung for inductive or Mayer–Vietoris computations of sphere homology inside Foundation.SingularSphere, which in turn supports the topological side of the pre-temporal forcing and recognition interface stages.

In the broader Recognition Science chain, singular homology of spheres and points is scaffolding for discrete topological invariants tied to the eight-tick octave and dimension-forcing arguments (T7–T8), not a physical mass or coupling claim. No downstream consumers are wired yet in the graph; the declaration exists as the named Stage A fact that later sphere and pair arguments are expected to quote.