range_arcMinus
plain-language theorem explainer
The image of the lower-semicircle path on the unit circle equals the closed lower hemisphere {z in S^1 : second ambient coordinate ≤ 0}. Anyone decomposing S^1 into upper and lower arcs for linking or H_1-vanishing arguments will cite it. The proof is set extensionality: forward from nonnegativity of the square-root factor, reverse by the arc-parameter section.
Claim. Let $\gamma_- : [0,1] \to S^1$ be the lower semicircle path $t \mapsto (1-2t,\,-\sqrt{1-(1-2t)^2})$. Then $\mathrm{range}(\gamma_-) = \{ z \in S^1 : z_1 \le 0 \}$, where $z_1$ is the second ambient coordinate of $z$.
background
The ambient setting is the unit circle $S^1 \subset \mathbb{R}^2$, written Sph 1, with ambient coordinate projection amb. Points are built via pt2, which packages a pair $(x_0,x_1)$ already known to lie on the sphere.
The semicircle family arcFun s hs sends $t \in [0,1]$ to $(1-2t,, s\sqrt{1-(1-2t)^2})$ with $s^2=1$. The choice $s=-1$ is the continuous path arcMinus (the lower semicircle). The inverse parameter arcParam z = (1-z_0)/2 recovers $t$ from the first coordinate, and arcFun_arcParam says that under the sign condition $s,z_1 = |z_1|$ one has arcFun s (arcParam z) = z.
This module develops high-dimensional linking-vanishing by reducing to circle geometry; the low-dimensional companion is imported from LinkingVanishingLowDim.
proof idea
Set extensionality on $z \in S^1$, then both inclusions.
Forward: if $z = \mathrm{arcMinus}(t)$, rewrite the second coordinate by arcFun_coord1 to $-\sqrt{1-(1-2t)^2}$. Nonnegativity of the real square root plus nlinarith gives $z_1 \le 0$.
Reverse: given $z_1 \le 0$, take $t = \mathrm{arcParam},z$. The sign hypothesis of arcFun_arcParam for $s=-1$ reduces to $|z_1| = -z_1$, which is abs_of_nonpos plus a ring identity. The lemma then returns $z$ as a point of the range.
why it matters
This is the lower-half half of the standard semicircle cover of $S^1$. Downstream, range_arcPlus_union_arcMinus rewrites both ranges and concludes the two semicircles exhaust the circle via le_total 0 (amb z 1). Likewise range_arcPlus_inter_arcMinus identifies the intersection with the east and west poles.
Those two cover/meet facts feed the acyclicity and linking-detection apparatus in the same module (ArcComplementsAcyclic, DetectsNontrivialLinking, linkingComplementH1). In the broader Recognition foundation this is pure geometric scaffolding for the high-dimensional linking-vanishing step, not a forcing-chain landmark (T5–T8) itself; it clears the circle geometry needed before higher-dimensional vanishing can be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.