sphere_dim_eq_of_homotopyEquiv
plain-language theorem explainer
Homotopy-equivalent unit spheres have equal dimension: a nonempty homotopy equivalence between Sph m and Sph n forces m = n. Topologists and anyone tracking Stage D of the singular-sphere development would cite it. The proof is a one-step contradiction against the Stage D non-equivalence theorem.
Claim. Let $S^m$ and $S^n$ denote the unit spheres in Euclidean space of dimensions $m+1$ and $n+1$. If there exists a homotopy equivalence $S^m \simeq S^n$, then $m = n$.
background
In this module, Sph n is the unit sphere in Euclidean space $\mathbb{R}^{n+1}$ (written EuclideanSpace ℝ (Fin (n+1))), packaged as a topological space in TopCat. The local setting is Stage D of the singular-sphere geometry development: classical facts about spheres needed before Recognition-specific forcing arguments.
The immediate upstream result is spheres_not_homotopyEquivalent: spheres of different dimension are not homotopy equivalent, stated as emptiness of the type of continuous homotopy equivalences. That theorem is the contrapositive engine for the present claim. Homotopy equivalence here is Mathlib's ContinuousMap.HomotopyEquiv.
Dimension of spheres is a classical topological invariant; the module records it in the form needed by later Recognition geometry (covers, poles, and radial structure on the sphere).
proof idea
Tactic proof by contradiction. Assume $m \neq n$. Apply spheres_not_homotopyEquivalent to obtain that the type of homotopy equivalences between Sph m and Sph n is empty. From the hypothesis, extract a witness via Nonempty.some and feed it to IsEmpty.false, yielding a contradiction. Thus $m = n$. No further case splits or geometric constructions appear at this layer; all work sits in the upstream non-equivalence lemma.
why it matters
Stage D records that sphere dimension is a homotopy invariant, in the Nonempty packaging convenient for later Lean arguments. The companion theorem spheres_not_homotopyEquivalent is the direct engine; this declaration is its positive-equality form.
In the Recognition framework, spatial dimension is forced at T8 ($D = 3$). Sphere topology and its dimension rigidity sit in the geometric substrate that later supports octave structure (T7, period $2^3$) and related covering arguments. No downstream consumers are wired yet in the graph (used_by is empty), so the lemma is presently a closed Stage D fact rather than an active dependency of a higher forcing step.
It does not itself force $D = 3$; it only locks equality of dimensions once a homotopy equivalence is assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.