arcA
plain-language theorem explainer
Defines the open east arc on the doubly punctured circle as the locus where the ambient first coordinate is positive. Algebraic topologists cite it when building the two-arc cover used for Mayer–Vietoris on S¹. It is a one-line set comprehension from the coordinate function on the intersection of the standard open covers.
Claim. Let $W_c$ be the doubly punctured unit circle (intersection of the two standard open hemispheric covers of $S^1$). The east arc is the subset $A = \{ w \in W_c : x_0(w) > 0 \}$, where $x_0$ is the first ambient Euclidean coordinate restricted to $W_c$.
background
The ambient space is the unit circle $S^1 \subset \mathbb{R}^2$, covered by two open sets $U$ and $V$ (complements of the south and north poles respectively). Their intersection $W_c = U \cap V$ is the circle with both poles removed: two open arcs, east and west.
The coordinate function on $W_c$ is the restriction of the first ambient coordinate $x_0$. On the doubly punctured circle this coordinate never vanishes, so the sign of $x_0$ cleanly splits $W_c$ into two nonempty open arcs.
Local setting is singular homology of spheres via Mayer–Vietoris: the two-arc decomposition of $W_c$ supplies a clopen set whose augmentation pairs nontrivially against the point-difference class of the east and west basepoints.
proof idea
Pure definition: the set of points of $W_c$ at which the coordinate function is strictly positive. No proof obligations; noncomputable only because $W_c$ and the ambient coordinate inherit noncomputability from the topological constructions.
why it matters
Supplies the distinguished clopen subset of $W_c$ used throughout the $H_1(S^1)\neq 0$ argument. Downstream, isClopen_arcA shows it is clopen; aW_mem_arcA and bW_notMem_arcA place the east and west basepoints on opposite sides; diffClass_pairing then shows the point-difference class pairs to $1$ against the east-arc augmentation, hence is nonzero. That nonzero class, together with exactness of Mayer–Vietoris, forces $H_1(S^1)\neq 0$ in h1_s1_ne_zero.
In the Recognition foundation this is geometric scaffolding for the circle’s first homology, which underwrites the eight-tick octave (T7) and the topological side of the forcing chain rather than a direct physical constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.