isEmbedding_arcMap
plain-language theorem explainer
The semicircle arc from the unit interval into the unit circle is a topological embedding whenever the fixed transverse coordinate squares to 1. Algebraic topologists working the high-dimensional linking-vanishing argument cite it to treat upper and lower arcs as embedded paths. The proof is a short term argument: continuity plus injectivity give a closed embedding into a Hausdorff sphere, hence an embedding.
Claim. For every real $s$ with $s^2=1$, the continuous map $\mathrm{arcMap}(s):[0,1]\to S^1$ sending the unit interval along the semicircle with transverse sign $s$ is a topological embedding.
background
The ambient space is Euclidean $\mathbb{R}^{n+1}$ (here $n=1$), written $\mathrm{Esp},n$, and $\mathrm{Sph},n$ is the unit sphere in that space as a topological space. The module builds high-dimensional linking-vanishing geometry on top of the singular-sphere toolkit and the low-dimensional linking lemmas.
The map in question is the continuous path $\mathrm{arcFun}(s)$ packaged as $\mathrm{arcMap}(s):C([0,1],S^1)$. Its first coordinate runs monotonically along the diameter (via $\mathrm{arcFun_coord0}$), while the second coordinate is the signed square-root height fixed by $s\in{\pm 1}$. Continuity of $\mathrm{arcFun}$ and injectivity of $\mathrm{arcMap}$ are already established upstream; both are used here without further analysis.
proof idea
Instantiate the Hausdorff ($T_2$) structure on the subtype $S^1\subset\mathrm{Esp},1$. Feed continuity of $\mathrm{arcFun}$ into the closed-embedding criterion for continuous injective maps into Hausdorff spaces, using $\mathrm{arcMap_injective}$ for injectivity. The resulting closed embedding is immediately an embedding. The whole argument is a two-line term proof; no case splits on $s$.
why it matters
Parent lemmas $\mathrm{isEmbedding_arcPlus}$ and $\mathrm{isEmbedding_arcMinus}$ are one-line specializations at $s=\pm 1$. Those embeddings let the high-dimensional linking package treat the two semicircle arcs as embedded 1-cells whose complements can be shown acyclic, feeding $\mathrm{ArcComplementsAcyclic}$ and the detection of nontrivial linking.
In the Recognition foundation layer this is pure topological scaffolding: it supports the geometric side of the forcing chain (sphere geometry used when dimensions and linking constraints are forced) rather than a named T0–T8 identity. No open sorry remains; the lemma is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.