eastP_mem_inter
plain-language theorem explainer
The east point of the unit circle lies in both open charts of the standard two-chart cover of $S^1$ (equatorially opposite the poles). Anyone building basepoints or transition data on the doubly punctured circle cites this. The proof is a short ambient-coordinate contradiction: the first Euclidean coordinate of the east point is $1$, while both poles have first coordinate $0$.
Claim. Let $S^1\subset\mathbb{R}^2$ be the unit circle, $N$ its north pole, $S$ its south pole, $U=S^1\setminus\{S\}$, and $V=S^1\setminus\{N\}$. If $e\in S^1$ is the east point (ambient coordinates $(1,0)$), then $e\in U\cap V$.
background
In this module the $n$-sphere Sph n is the unit sphere in Euclidean space $\mathbb{R}^{n+1}$, packaged as a topological space. For $n=1$ one works on the circle $S^1\subset\mathbb{R}^2$. The two standard open charts are the complements of the poles: coverU 1 removes the south pole and coverV 1 removes the north pole; their union is all of $S^1$.
Points on the sphere are compared through the ambient-coordinate coercion amb, which reads the underlying vector in $\mathbb{R}^{n+1}$. The east point is the standard basis vector $e_0=(1,0)$; the lemmas amb_eastP_zero, amb_northP_zero, and amb_southP_zero record that its first coordinate is $1$ while both poles have first coordinate $0$. The elementary fact $1\neq 0$ is imported as one_ne_zero.
proof idea
Unfold membership in the intersection and discharge the two sides separately. For the $U$-side, assume the east point equals the south pole; apply congrArg amb and rewrite with amb_eastP_zero and amb_southP_zero to obtain $1=0$, contradicting one_ne_zero. The $V$-side is identical with the north pole and amb_northP_zero. No chart maps or openness arguments are needed: pure coordinate comparison.
why it matters
This lemma is the membership certificate used to package the east point as an element of the intersection chart domain. Downstream, aW is defined by ⟨eastP, eastP_mem_inter⟩, giving a concrete basepoint in the doubly punctured circle on which transition and gluing data for the singular-sphere geometry are built.
Within Recognition Science foundation work, the singular sphere supplies the geometric stage on which the eight-tick octave and the $D=3$ forcing (T7–T8) are later realized; having an explicit, proved point in $U\cap V$ keeps those constructions free of sorry at the chart-intersection layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.