range_arcPlus
plain-language theorem explainer
The image of the upper-semicircle path on the unit circle S^1 equals the closed upper hemisphere {z : amb(z,1) ≥ 0}. Algebraic topologists and RS foundation proofs that split S^1 into two arcs cite this identification. The proof is a two-sided set extensionality: nonnegativity of the second ambient coordinate follows from the square-root formula, and the reverse uses the arc-parameter section.
Claim. The range of the continuous upper-semicircle map $\mathrm{arcPlus}:[0,1]\to S^1$ equals $\{z\in S^1:\mathrm{amb}(z,1)\ge 0\}$, i.e. the closed upper semicircle in ambient coordinates.
background
The module develops linking-vanishing statements for high-dimensional spheres by cutting $S^1$ into two semicircular arcs and showing their complements are acyclic. Points of the unit circle live in the ambient Euclidean plane via the embedding $\mathrm{amb}$; the second coordinate $\mathrm{amb}(z,1)$ is the signed height.
The path $\mathrm{arcFun}(s,h_s)$ sends $t\in[0,1]$ to $(1-2t,,s\sqrt{1-(1-2t)^2})$ on $S^1$, with sign $s=\pm 1$ selecting the upper or lower semicircle. The continuous map $\mathrm{arcPlus}$ is the $s=+1$ case. The section $\mathrm{arcParam}(z)=(1-\mathrm{amb}(z,0))/2$ recovers the parameter from the first coordinate, and $\mathrm{arcFun_arcParam}$ asserts that this section inverts $\mathrm{arcFun}$ whenever the sign condition $s\cdot\mathrm{amb}(z,1)=|\mathrm{amb}(z,1)|$ holds.
proof idea
Set extensionality on $z\in S^1$, then both inclusions.
Forward: if $z=\mathrm{arcPlus}(t)$, rewrite the second ambient coordinate by $\mathrm{arcFun_coord1}$ and $1\cdot x=x$; nonnegativity is $\sqrt{\cdot}\ge 0$.
Reverse: given $\mathrm{amb}(z,1)\ge 0$, take the witness $t=\mathrm{arcParam}(z)$. The sign hypothesis of $\mathrm{arcFun_arcParam}$ reduces (via $1\cdot x=x$ and $\mathrm{abs_of_nonneg}$) to the assumed nonnegativity, so $\mathrm{arcFun}(+1)(\mathrm{arcParam},z)=z$.
why it matters
This range formula is the upper half of the semicircle decomposition of $S^1$. Downstream, $\mathrm{range_arcPlus_union_arcMinus}$ rewrites both ranges and concludes the two arcs cover the whole circle by $\mathrm{le_total}$ on the height coordinate; $\mathrm{range_arcPlus_inter_arcMinus}$ shows they meet exactly at the east and west poles. Those covering and intersection facts feed the acyclicity argument for arc complements ($\mathrm{ArcComplementsAcyclic}$) used in the high-dimensional linking-vanishing chain. In the Recognition foundation this is pure geometric scaffolding: it supports the topological side of the forcing apparatus rather than a numbered T0–T8 step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.