arcPlus
plain-language theorem explainer
Names the continuous upper semicircle path on S^1 as a map from the unit interval. Used throughout the high-dimensional linking-vanishing argument to split an embedded circle into two arcs for Mayer-Vietoris. Defined by specializing the signed semicircle map at sign +1.
Claim. Let $\mathrm{arc}^+ : I \to S^1$ be the continuous path along the upper semicircle (the set of points of $S^1$ with nonnegative second ambient coordinate), obtained by specializing the signed semicircle map at sign $+1$.
background
The module develops the high-dimensional half of the linking-vanishing story: for $D \ge 1$ with $D \ne 3$, every embedded circle in $S^D$ has $H_1$-acyclic complement, once arc complements are assumed acyclic. The argument follows Hatcher's circle case (2B.1): cut the circle into two semicircle images and run Mayer-Vietoris on their complements inside the complement of the two endpoints.
Sph n is the unit sphere in Euclidean space of dimension $n+1$. The signed map arcMap s (with $s^2=1$) packages the continuous semicircle path of sign $s$ as an element of $C(I,S^1)$. The ambient second coordinate distinguishes upper from lower: nonnegative for the upper arc, nonpositive for the lower.
proof idea
One-line specialization: apply the signed semicircle continuous map at $s=1$, using $1^2=1$. No further proof content; continuity and the path formula are inherited from the signed map and its underlying arc function.
why it matters
This is the upper half of the standard two-arc cover of $S^1$. Downstream lemmas record that it is an embedding, that its range is exactly ${z\in S^1: z_1\ge 0}$, that the two semicircle ranges meet only at the east and west poles, and that their union is the whole circle. Those set identities feed the Mayer-Vietoris setup in 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. In the Recognition foundation this clears nontrivial linking obstructions outside the exceptional dimension $D=3$ forced by the T8 spatial-dimension step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.