isEmbedding_arcMinus

The module develops H_1-vanishing for complements of embedded circles in high-dimensional spheres, following the circle case of Hatcher's reduction (two semicircle arcs, Mayer–Vietoris on their complements). The ambient space is the unit sphere $S^D \subset E^D$; here one works first on $S^1$.

An arc map is a continuous path $\mathrm{arcMap}(s)$ along a semicircle of $S^1$, parameterized by the unit interval, with sign $s \in {\pm 1}$ selecting upper or lower hemisphere. The lower arc $\mathrm{arc}^-$ is exactly $\mathrm{arcMap}(-1)$ (using $(-1)^2 = 1$). Embedding means the map is a homeomorphism onto its image in the subspace topology.

The sibling lemma isEmbedding_arcMap already shows every such signed arc map is an embedding: the underlying coordinate path is a closed embedding (continuous, injective, closed range into a T2 sphere).

One-line wrapper. Instantiate the general embedding lemma for signed arc maps at $s = -1$, discharging the hypothesis $s^2 = 1$ by the elementary fact $(-1)^2 = 1$. No new topology is proved here.

Feeds the circle-complement reduction theorem in the same module: if arc complements in $S^D$ are $H_1$-acyclic, then for $D \ge 1$ and $D \neq 3$ every embedded circle in $S^D$ has $H_1$-acyclic complement (Mayer–Vietoris over the two semicircle images inside the complement of the two endpoints). Both upper and lower arcs must be embeddings so their images are closed arcs suitable for that MV split.

In the Recognition forcing chain this sits in the geometric side of the $D = 3$ story (T8): the $D \neq 3$ hypothesis is exactly where classical linking can be nontrivial, so the high-dimensional vanishing lemmas fence off the three-dimensional case where recognition geometry lives. The lemma itself is pure point-set topology; its value is as a named building block in that reduction.