spheres_not_homotopyEquivalent
plain-language theorem explainer
Spheres of unequal dimension are never homotopy equivalent: if m ≠ n then there is no continuous homotopy equivalence between the unit m-sphere and the unit n-sphere. Algebraic topologists and anyone tracking Stage D of the RS forcing chain cite this as the empty-homotopy form of dimensional rigidity. The proof is a two-case homology contradiction: a putative equivalence would identify a nonvanishing top homology group with a vanishing one.
Claim. For natural numbers $m \neq n$, the set of continuous homotopy equivalences between the unit $m$-sphere $S^m \subset \mathbb{R}^{m+1}$ and the unit $n$-sphere $S^n \subset \mathbb{R}^{n+1}$ is empty.
background
In this module, Sph n is the unit sphere in Euclidean space of dimension $n+1$, packaged as a topological space in TopCat. Homology is taken in the module's Hgrp groups; Stage D of the pre-temporal forcing order is the geometric layer that pins spatial dimension.
Upstream, sphere_homology_vanish states Stage D vanishing: $H_k(S^n)=0$ whenever $1 \le k$ and $k \neq n$. The companion nonvanishing fact sphere_top_ne_zero asserts that the top group $H_n(S^n)$ is nontrivial. Homotopy equivalences induce isomorphisms on all Hgrp degrees via hgrpIso.
The ambient RS landmarks are T8 (forcing $D=3$ spatial dimensions) and the singular-sphere geometry that makes that forcing topological rather than merely combinatorial. Several modules export a constant $D:=3$; this lemma is the pure homotopy obstruction used before specializing to that value.
proof idea
Assume a homotopy equivalence $e:S^m\simeq S^n$ and split on $m<n$ versus $n<m$ (the equal case is excluded by hypothesis).
If $m<n$, apply sphere_homology_vanish at degree $n$ on $S^m$ to get $H_n(S^m)=0$, transport across hgrpIso e n (then reverse the iso) to conclude $H_n(S^n)=0$, and contradict sphere_top_ne_zero n.
If $n<m$, run the same argument with $e^{-1}$ at degree $m$: vanishing of $H_m(S^n)$ pulls back to vanishing of $H_m(S^m)$, again contradicting top nonvanishing. Both branches close by omega on the dimension inequalities.
why it matters
This is the empty-form half of Stage D dimensional rigidity for spheres. Its sole recorded consumer is sphere_dim_eq_of_homotopyEquiv, which rephrases the claim as: any nonempty homotopy equivalence forces $m=n$. Together they certify that sphere dimension is a homotopy invariant inside the RS singular-sphere stack.
In the forcing chain this sits under T8 ($D=3$ spatial dimensions): once spheres of different dimension cannot be homotopy equivalent, the geometric models used to force three spatial dimensions cannot collapse across dimension by continuous deformation. It does not itself compute $D$; it supplies the topological separation that later specializations to $D=3$ rely on.
No scaffolding remains: the claim is fully proved from the module's homology vanishing and nonvanishing package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.