range_arcPlus_inter_arcMinus
plain-language theorem explainer
The upper and lower semicircle arcs on S^1 meet exactly at the east and west poles. Algebraic topologists citing the circle-complement reduction (Hatcher 2B.1 style) use this to pin the two-endpoint set in the Mayer-Vietoris cover. The proof rewrites both ranges as half-plane conditions on the second ambient coordinate, then solves the circle equation.
Claim. The image of the upper semicircle path on $S^1$ and the image of the lower semicircle path intersect in exactly two points: the east pole and the west pole of $S^1$.
background
The module develops linking-vanishing statements for embedded circles in high-dimensional spheres, reducing complement homology via semicircle decompositions. On the unit circle $S^1\subset\mathbb{R}^2$, ambient coordinates satisfy the circle equation $x_0^2+x_1^2=1$.
The continuous path arcPlus traces the upper semicircle (nonnegative second coordinate); arcMinus traces the lower semicircle (nonpositive second coordinate). Prior range lemmas identify those images with the closed half-circles ${z\in S^1:x_1(z)\ge 0}$ and ${z\in S^1:x_1(z)\le 0}$. East and west poles are the standard basis points $(\pm 1,0)$ on $S^1$.
Upstream, coord_sq_add_sq records the circle identity, and abs_eq_one_of_sq_eq_one converts a squared coordinate equal to one into absolute value one.
proof idea
Rewrite both ranges via range_arcPlus and range_arcMinus, so membership in the intersection means $x_1(z)\ge 0$ and $x_1(z)\le 0$. Antisymmetry forces $x_1(z)=0$. The circle identity coord_sq_add_sq then yields $x_0(z)^2=1$, hence $|x_0(z)|=1$ by abs_eq_one_of_sq_eq_one.
Case-split on the sign of $x_0$: $+1$ recovers the east pole and $-1$ the west pole, using ambient injectivity and coordinate-wise extension. The converse direction checks both poles satisfy $x_1=0$, so they lie in both half-circles.
why it matters
This lemma supplies the exact two-point overlap of the semicircle images used by isZero_h1_complement_of_embedding, the circle-complement reduction: if arc complements in $S^D$ are $H_1$-acyclic, then for $D\ge 1$, $D\ne 3$, every embedded circle in $S^D$ has $H_1$-acyclic complement, via Mayer-Vietoris over complements of the two semicircle images inside the complement of the two endpoint images.
In the Recognition foundation stack this is geometric scaffolding for linking vanishing away from dimension three, consistent with the forcing chain's isolation of $D=3$ (T8) as the exceptional spatial dimension. It does not itself force $D=3$; it clears the complementary cases so that nontrivial linking can survive only where the dimensional hypothesis fails.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.