isClopen_arcA
plain-language theorem explainer
The east arc of the doubly punctured circle is clopen in the subspace topology. Algebraic topologists running the Mayer-Vietoris argument for nonzero first homology of the circle cite it to justify the arc-augmentation pairing. The proof rewrites the arc as a continuous preimage of either $(0,\infty)$ or $[0,\infty)$, using that the first ambient coordinate never vanishes off the poles.
Claim. Let $W_c$ be the unit circle with north and south poles removed, and let $\mathrm{coord}_W:W_c\to\mathbb{R}$ be the first ambient Euclidean coordinate. The east arc $A=\{w\in W_c:\mathrm{coord}_W(w)>0\}$ is clopen in $W_c$.
background
The ambient space is the unit sphere $S^1\subset\mathbb{R}^2$ with distinguished poles $N$ and $S$. The standard open covers $U=S^1\setminus{S}$ and $V=S^1\setminus{N}$ meet in the doubly punctured circle $W_c=U\cap V$, whose points are exactly those unequal to both poles (via mem_inter_iff).
On $W_c$ one has a continuous real coordinate $\mathrm{coord}_W$, the restriction of the first Euclidean projection. A companion lemma records that this coordinate never hits zero on $W_c$: vanishing would force the point onto a pole by the unit-norm identity. The east arc is the strict positive locus of that coordinate.
The local setting is singular-sphere geometry supporting a Mayer-Vietoris computation of $H_*(S^1)$ in the Recognition foundation layer.
proof idea
Split IsClopen into closed and open.
Closed half: prove set-equality of the east arc with $\mathrm{coord}_W^{-1}([0,\infty))$. Membership in $W_c$ supplies the two pole inequalities; the non-vanishing lemma upgrades a non-strict inequality $\mathrm{coord}_W\ge 0$ to a strict one, so the two sets coincide. Continuity of $\mathrm{coord}_W$ then pulls back the closed ray.
Open half: the arc is definitionally $\mathrm{coord}_W^{-1}((0,\infty))$, so continuity pulls back the open ray.
why it matters
Downstream, the clopen certificate is the second argument of the arc-augmentation map used in diffClass_pairing: the point-difference class pairs to $1$ against that augmentation, hence is nonzero. That nonzero pairing is the engine of h1_s1_ne_zero, which shows $H_1(S^1)\ne 0$ by exactness of Mayer-Vietoris: if the homology vanished the connecting map would kill the difference class, a contradiction.
In the Recognition foundation this is the topological seed that the singular sphere carries nontrivial first homology, the geometric backdrop for the eight-tick octave and the $D=3$ forcing steps that sit higher in the chain. No open scaffold remains; the lemma is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.