range_arcPlus_union_arcMinus
plain-language theorem explainer
The upper and lower semicircle paths on the unit circle jointly cover every point of $S^1$. Algebraic topologists citing the Mayer–Vietoris reduction for $H_1$-acyclicity of circle complements in $S^D$ ($D\neq 3$) need this cover. The proof rewrites each range as a closed half of $S^1$ cut by the second ambient coordinate and invokes order totality.
Claim. Writing $\gamma_+$ and $\gamma_-$ for the continuous upper and lower semicircle paths $I\to S^1$, one has $\operatorname{im}(\gamma_+)\cup\operatorname{im}(\gamma_-)=S^1$.
background
The module builds the high-dimensional half of the linking-vanishing argument: embedded circles in $S^D$ for $D\ge 1$, $D\neq 3$, have $H_1$-acyclic complements once arc complements are acyclic. The circle $S^1$ is split into two continuous semicircle arcs.
arcPlus is the upper semicircle path (sign $+1$ in the arc map); arcMinus is the lower one (sign $-1$). Upstream lemmas identify their images with closed hemispheres of $S^1$: $\operatorname{im}(\gamma_+)={z\in S^1:\operatorname{amb}(z)1\ge 0}$ and $\operatorname{im}(\gamma-)={z\in S^1:\operatorname{amb}(z)_1\le 0}$, where $\operatorname{amb}$ reads ambient Euclidean coordinates on the sphere.
Order totality on the ambient second coordinate (via the integer-order lemma le_total) is the only arithmetic input needed to glue the two halves.
proof idea
Rewrite both ranges by the characterizing lemmas range_arcPlus and range_arcMinus, so the goal becomes
${z:\operatorname{amb}(z)_1\ge 0}\cup{z:\operatorname{amb}(z)_1\le 0}=S^1$.
Extensionality on $z\in S^1$ reduces membership in the union to the disjunction $0\le\operatorname{amb}(z)_1\lor\operatorname{amb}(z)_1\le 0$, which is exactly le_total 0 (amb z 1). Simp clears the set-membership noise; the proof is a short tactic script, not a deep construction.
why it matters
Downstream, isZero_h1_complement_of_embedding quotes this cover to run Mayer–Vietoris on the complements of the two semicircle images inside the complement of the two endpoints (Hatcher 2B.1, circle case). Without a literal set-theoretic cover of $S^1$ by the two arcs, the MV decomposition of the complement of an embedded circle in $S^D$ does not start.
In the Recognition Science foundation stack this is pure topological scaffolding for the high-dimensional linking-vanishing theorem that feeds the Clifford/Bott side of the eight-tick story: once circle complements are $H_1$-acyclic off dimension 3, nontrivial linking cannot obstruct the dimensional forcing that isolates $D=3$. The lemma itself is elementary; its place is as the first geometric input to that reduction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.