isZero_sph0
plain-language theorem explainer
Positive-degree singular homology of the 0-sphere vanishes: $H_k(S^0;\mathbb{Z})=0$ for every $k\ge 1$. Anyone proving sphere homology by induction on dimension cites this as the $n=0$ base. The argument is a one-line application of the Mathlib fact that totally disconnected spaces have vanishing positive homology, retyped onto the local $Hgrp$ abbreviation.
Claim. For every natural number $k\neq 0$, the degree-$k$ singular homology group $H_k(S^0;\mathbb{Z})$ is the zero object in $\mathbf{Mod}_{\mathbb{Z}}$. Here $S^0$ is the unit sphere in $\mathbb{R}^1$ (two discrete points).
background
In this module, Sph n is the unit sphere in Euclidean space of dimension $n+1$, packaged as a TopCat object. Degree-$n$ singular homology with integer coefficients is abbreviated Hgrp X n, i.e. the homology of the singular chain complex of $X$.
The 0-sphere $S^0$ is homeomorphic to a two-point discrete space, hence totally disconnected. Mathlib already records that positive-degree singular homology of any totally disconnected space vanishes; the upstream lemma isZero_homology_of_totallyDisconnected simply retypes that fact onto Hgrp.
The local development aims at the classical vanishing pattern for sphere homology, used as geometric scaffolding inside the Recognition foundation layer.
proof idea
One-line term proof: apply isZero_homology_of_totallyDisconnected to Sph 0 at degree $k$, using the hypothesis $k\neq 0$. Instance search supplies total disconnectedness of the two-point sphere; no further calculation is needed.
why it matters
This is the base case of the inductive proof of Stage D vanishing: sphere_homology_vanish asserts $H_k(S^n;\mathbb{Z})=0$ whenever $1\le k$ and $k\neq n$. The induction on $n$ begins with the $n=0$ clause, which is exactly this lemma.
In the broader Recognition geometry stack, controlled vanishing of sphere homology underwrites later Mayer–Vietoris and covering arguments on singular spheres (north/south pole covers, path-connected intersections in dimension $\ge 2$). It is pure algebraic topology infrastructure, not a physics claim, but it sits on the path toward geometric forcing results that feed the foundation chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.