sphere_top_ne_zero
plain-language theorem explainer
For every n ≥ 1 the top singular homology H_n(S^n; ℤ) is nonzero. Dimension-separation arguments cite it to show spheres of unequal dimension are not homotopy equivalent. The proof is induction on n: the circle base uses a Mayer–Vietoris exactness argument, and the step transports nonvanishing across the suspension isomorphism.
Claim. For every natural number $n$ with $n \ge 1$, the degree-$n$ singular homology module $H_n(S^n;\mathbb{Z})$ is not the zero module.
background
In this module the $n$-sphere is realized as the unit sphere in Euclidean space of dimension $n+1$, written as a topological space object. Its degree-$n$ singular homology with integer coefficients is the abelian group (as a $\mathbb{Z}$-module) obtained from the singular chain complex.
Stage D of the local development records elementary sphere facts needed before dimension can be forced. The base nonvanishing $H_1(S^1)\neq 0$ is already proved by Mayer–Vietoris: if that group vanished, the connecting map would kill the point-difference class, contradicting a nonzero pairing. Suspension identifies the top homology of $S^{k+1}$ with that of $S^k$, so nonvanishing propagates upward.
The ambient Recognition chain later forces spatial dimension $D=3$ (T8); distinguishing spheres by homology is the classical topological input that makes unequal dimensions inequivalent.
proof idea
Induct on $n$. The zero case is immediate from the hypothesis $1\le n$. On the successor, match the predecessor: if the predecessor is $0$, invoke the already-proved nonvanishing of $H_1(S^1)$. If the predecessor is $m+1$, assume for contradiction that the top homology of $S^{m+2}$ vanishes; pull the zero object back along the inverse suspension isomorphism to obtain vanishing for $S^{m+1}$, contradicting the inductive hypothesis (after a trivial arithmetic check that $1\le m+1$).
why it matters
This lemma is the homology engine behind spheres_not_homotopyEquivalent: if $m\neq n$, a hypothetical homotopy equivalence would identify top homology groups, but only one of those groups can sit in the matching degree, and nonvanishing of the top group of the larger sphere yields a contradiction.
In the Recognition forcing chain, Stage D supplies the topological distinction among dimensions that T8 later specializes to $D=3$ spatial dimensions. Without top-homology nonvanishing, spheres of different dimension could not be separated inside the Lean development, and the link from the eight-tick/octave structure to three spatial axes would lack its classical topological anchor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.