bW
plain-language theorem explainer
Packages the geometric west point of the unit circle as a point of the doubly punctured circle (intersection of the two standard open covers). Cited wherever the two-arc intersection needs an explicit second basepoint opposite the east point. Construction is the subtype pair of the west point with its membership proof in both covers.
Claim. Let $W_c$ be the doubly punctured unit circle (intersection of the two standard open covers of $S^1$). The west point $b_W \in W_c$ is the point antipodal to the east point, viewed as an element of that intersection.
background
The ambient space is the unit sphere $S^1$ in the Euclidean plane. Two open covers puncture it at the north and south poles respectively; their intersection is the doubly punctured circle $W_c$, a two-arc space used for Mayer–Vietoris computations of $H_0$.
The west point is defined as the negative of the east point on the unit circle. A prior lemma records that this point lies in both open covers, hence in their intersection. The present definition simply reifies that geometric point as a term of the topological space $W_c$.
Local setting is singular-sphere geometry supporting homology of arc covers: east and west points serve as the two connected components of the intersection, so their difference class in $H_0(W_c)$ is the generator detected by the Mayer–Vietoris connecting map.
proof idea
Definitional subtype construction: form the pair consisting of the west point together with the already-proved membership lemma that places it in both open covers (hence in $W_c$). No further algebraic work.
why it matters
Supplies the second basepoint needed to build the point-difference class $\mathrm{pt}_H(a_W)-\mathrm{pt}_H(b_W)$ in $H_0(W_c)$. That class is shown nonzero by pairing against the east-arc augmentation, and is shown to die under the Mayer–Vietoris map into $H_0(U)\oplus H_0(V)$ because both points become path-connected inside each punctured circle. Downstream lemmas bW_notMem_arcA, diffClass, and diffClass_mvPair all consume this point. In the broader Recognition foundation this is pure topological scaffolding for the singular-sphere side of the forcing geometry, not a physical constant claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.