puncturedPolar
plain-language theorem explainer
Polar-coordinate homeomorphism: the orthogonal hyperplane at the north pole, with the origin removed, is topologically the product of its unit sphere with the positive ray. Sphere-cover and homotopy arguments in the singular-sphere geometry cite it when they need radial coordinates on that hyperplane. The body is a one-line specialization of Mathlib's unit-sphere product homeomorphism.
Claim. For each $n\in\mathbb{N}$, writing $\mathrm{Hyp}_n$ for the orthogonal hyperplane to the north-pole direction in the ambient Euclidean space, there is a homeomorphism $\mathrm{Hyp}_n\setminus\{0\}\ \simeq_t\ S(\mathrm{Hyp}_n)\times(0,\infty)$, where $S(\mathrm{Hyp}_n)$ is the unit sphere about the origin in $\mathrm{Hyp}_n$.
background
The module builds singular-sphere geometry used in Recognition foundation arguments: ambient Euclidean space, north and south poles, and two open covers of the sphere that omit one pole each. The abbreviation $\mathrm{Hyp},n$ is the orthogonal complement of the real span of the north-pole vector, so it is the tangent hyperplane at that pole, realized as a Euclidean subspace.
On any real normed space the standard polar decomposition separates direction and radius. Mathlib packages this as a homeomorphism from the punctured space to the product of the unit sphere with the open positive ray. Here that fact is specialized to $\mathrm{Hyp},n$, so points of the punctured hyperplane are written uniquely as a unit vector times a positive scale.
Sibling material in the same file defines the two covers, openness, and their union, and prepares linear isometries between successive hyperplanes. Those pieces feed the same homotopy pipeline that consumes this polar chart.
proof idea
One-line wrapper: instantiate Mathlib's homeomorphUnitSphereProd on the Euclidean space $\mathrm{Hyp},n$. No extra algebraic work; the type ascriptions (punctured set, unit sphere about $0$, and $(0,\infty)$) match the library lemma exactly.
why it matters
Downstream, interHomotopyEquiv (Step 2) composes this polar chart with the homeomorphism of the cover intersection onto the punctured hyperplane and with a linear-isometry homeomorphism of unit spheres. The doc-comment there states the goal: the intersection of the two punctured-sphere covers of $S^{n+1}$ is homotopy equivalent to $S^n$. Radial coordinates on $\mathrm{Hyp},n$ make the deformation retraction to the unit sphere immediate, which is the inductive step in the cover-based homotopy analysis of the singular sphere.
In the broader Recognition foundation this geometry supports the singular-sphere side of the forcing and octave constructions (eight-tick structure, dimensional constraints). The declaration itself is pure topology: it does not encode $\varphi$, $J$-cost, or mass-ladder data, but it is the coordinate tool those sphere arguments rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.