punctTranslateHomeo
plain-language theorem explainer
Homeomorphism translating a single puncture to the origin: for a normed additive group F and point y₀, F \ {y₀} is topologically equivalent to F \ {0} via x ↦ x − y₀. Downstream homotopy arguments for two-point sphere complements cite it to normalize the second puncture after stereographic projection. The body is a subtype restriction of right translation.
Claim. Let $F$ be a normed additive commutative group and $y_0 \in F$. Translation by $-y_0$ induces a homeomorphism $F \setminus \{y_0\} \simeq_t F \setminus \{0\}$.
background
The ambient module develops high-dimensional linking vanishing: complements of arcs and finite point sets in spheres become acyclic or homotopy-equivalent to lower-dimensional spheres once dimension is large enough. A recurring normalization step is to move a distinguished puncture to the origin so polar or ray decompositions apply cleanly.
Here $F$ carries only a NormedAddCommGroup structure (no inner product is required for this map). Complements are ordinary set complements of singletons, and $\simeq_t$ means a homeomorphism of the subtype topologies. The companion low-dimensional linking module and singular-sphere geometry supply the sphere and stereographic infrastructure that will compose with this translation.
Right translation $x \mapsto x - y_0$ is already a homeomorphism of $F$; the content is that it restricts to the punctured sets.
proof idea
Start from Mathlib's Homeomorph.subRight y₀, the homeomorphism of the ambient group given by right translation by $y_0$. Restrict it to subtypes via Homeomorph.subtype, supplying the membership equivalence: $x \notin {y_0}$ if and only if $x - y_0 \notin {0}$. That biconditional is not_congr sub_eq_zero after unfolding complement and singleton membership. No continuity or inverse work is redone; both come from the ambient homeomorphism.
why it matters
Parent consumer is twoPointComplHEquiv: after stereographic projection at one puncture $p$ of $S^{n+1}$, the image of the second puncture $q$ is some $y_0 \neq 0$ in the chart; this homeomorphism slides that image to the origin so the subsequent polar decomposition and ray collapse can identify the two-point complement with the equator sphere $S^n$. That identification is the geometric engine for high-dimensional linking vanishing in the Recognition foundation stack (complements detect no nontrivial linking once dimension exceeds the link dimension).
In the broader forcing picture the result is infrastructure rather than a T0–T8 landmark: it supports the topological side of why higher-dimensional recognition geometry cannot carry residual linking defects that would obstruct dimensional forcing toward $D = 3$ and the eight-tick octave. It closes no open sorry; it is a pure definitional homeomorphism used as a normalization step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.