hn_pt_isZero

The SingularSphere module assembles classical singular-homology facts used later for spheres, prisms, and Mayer–Vietoris arguments in the Foundation layer. The abbreviation for degree-$n$ singular homology with integer coefficients is the homology of the singular chain complex of the space.

A space is totally disconnected when every connected component is a singleton. Mathlib already proves that positive-degree singular homology of such spaces vanishes; the local lemma isZero_homology_of_totallyDisconnected retypes that Mathlib fact onto the module’s homology abbreviation. Its doc-comment: “Positive-degree singular homology of a totally disconnected space vanishes (Mathlib), retyped onto Hgrp.”

The one-point space is totally disconnected, so Stage A is the classical vanishing $H_m(\mathrm{pt})=0$ for $m\neq 0$. The next block in the file is Stage B: $H_0(X)\cong\mathbb{Z}$ for contractible $X$.

One-line term proof. Apply isZero_homology_of_totallyDisconnected to the one-point space TopCat.of Unit with the hypothesis $m\neq 0$. That lemma calls Mathlib’s isZero_singularHomologyFunctor_of_totallyDisconnectedSpace; the unit type carries a TotallyDisconnectedSpace instance, so no extra work is required.

Stage A of the point-space base case inside SingularSphere. It anchors later homology computations for spheres, subdivisions, prism operators, and Mayer–Vietoris sequences imported by the same module. The dependency graph currently lists no downstream users, but the immediate sequel in-file is Stage B ($H_0$ of a contractible space is $\mathbb{Z}$). In the Recognition framework this is topological scaffolding for invariants of the recognition geometry, not a direct step of the T0–T8 forcing chain (J-uniqueness, $\varphi$, eight-tick octave, $D=3$).