isEmbedding_arcPlus
plain-language theorem explainer
The upper semicircle path on the unit circle is a topological embedding of the unit interval. Anyone reducing circle complements by splitting into two arcs cites this. The proof is a one-line specialization of the general arc-map embedding lemma at the positive unit square root.
Claim. The continuous map $\mathrm{arc}^+ : I \to S^1$ that parametrizes the upper semicircle (the image of the standard arc map at parameter $s=1$) is a topological embedding.
background
The module develops vanishing of first homology for complements of embedded circles in $S^D$ when $D \ge 1$ and $D \ne 3$, following the circle case of Hatcher's reduction. The strategy splits an embedded circle into two semicircle arcs and applies Mayer-Vietoris to the complements of those arcs inside the complement of the two endpoints.
The upper semicircle arc $\mathrm{arc}^+$ is the continuous map $I \to S^1$ obtained by specializing the general arc map at $s=1$ (where $s^2=1$). The companion lower arc uses $s=-1$. The general lemma states that for any real $s$ with $s^2=1$, the corresponding arc map is a topological embedding: it is a closed embedding of a compact Hausdorff domain into the $T_2$ sphere $S^1$.
proof idea
One-line wrapper: instantiate the general arc-map embedding lemma at $s=1$, discharging $s^2=1$ by $1^2=1$. No extra topology is proved here; injectivity, continuity, and the closed-embedding upgrade are inherited from that lemma.
why it matters
Parent use is the circle-complement reduction theorem: if arc complements in $S^D$ are $H_1$-acyclic, then every embedded circle in $S^D$ ($D\ge 1$, $D\ne 3$) has $H_1$-acyclic complement. That argument runs Mayer-Vietoris over the two semicircle images; it needs both arcs to be embeddings so their images are homeomorphic copies of $I$ and the endpoint-pair complement is well-defined.
In the Recognition foundation layer this is pure supporting topology for linking-vanishing statements that underwrite dimensional constraints (the $D=3$ exception is explicit in the parent). It does not itself touch the forcing chain T0-T8, but it is part of the geometric scaffolding those dimensional claims rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.