westP_mem_inter
plain-language theorem explainer
The west point of the unit circle lies in both charts of the standard two-set open cover (circle minus south pole and circle minus north pole). Anyone building the doubly punctured circle or its chart atlas cites this membership. The proof is a short coordinate contradiction: the west point has first ambient coordinate −1, while both poles have first coordinate 0.
Claim. Let $S^1\subset\mathbb{R}^2$ be the unit circle, $N$ its north pole, and $S$ its south pole. Write $U=S^1\setminus\{S\}$ and $V=S^1\setminus\{N\}$. The west point $W=(-1,0)\in S^1$ satisfies $W\in U\cap V$.
background
In this module the $n$-sphere is realized as the unit sphere in Euclidean space $\mathbb{R}^{n+1}$ (as a TopCat object). Ambient coordinates of a sphere point are recovered by the coercion helper amb. On $S^1$, the north and south poles are the standard antipodal points along the last axis; the west point is the negative first basis vector on the circle.
The two open sets coverU 1 and coverV 1 form the usual stereographic atlas: each is $S^1$ with one pole removed. Their intersection is the doubly punctured circle, the space on which subsequent coordinate functions and transition data live. Upstream coordinate lemmas record the first ambient coordinate of the poles (both $0$) and of the west point (equal to $-1$).
proof idea
Term-mode proof via mem_inter_iff, splitting into two membership goals.
For membership in coverU 1 (circle minus south pole): assume the west point equals the south pole, push the equality through amb, and rewrite with amb_westP_zero and amb_southP_zero to obtain $-1=0$, discharged by norm_num.
For membership in coverV 1 (circle minus north pole): the same pattern with amb_northP_zero again yields $-1=0$. No topology beyond the set-theoretic definition of the covers is used.
why it matters
This lemma is the sole membership witness used by bW, which packages the west point as a concrete point of the doubly punctured circle Wc. That point anchors chart coordinates and transition maps on the intersection of the two stereographic charts.
In the broader Singular Sphere Geometry development, the doubly punctured circle is the model space for one-dimensional recognition geometry before lifting to higher spheres. The result is pure foundation infrastructure: it does not itself invoke the forcing chain (T0–T8), the Recognition Composition Law, or the $\varphi$-ladder, but it supplies a named basepoint those later constructions can reference once the continuum bridge is in place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.