eastP
plain-language theorem explainer
Names the canonical east pole of the unit circle S^1 as the standard basis vector e_0 in R^2. Downstream geometry (semicircle arcs, linking vanishing, Mayer–Vietoris on circle complements) cites it as a fixed endpoint. The definition is a subtype package: single-coordinate vector plus a one-line norm check.
Claim. Let $E_1=\mathbb{R}^2$ be the ambient Euclidean space of $S^1$. Define the east point $e_+\in S^1\subset E_1$ by $e_+=(1,0)$, i.e. the image of the standard basis vector with first coordinate $1$ and all others $0$, which lies on the unit sphere centered at the origin.
background
The module builds concrete points and open covers on singular spheres $S^n\subset E_n$, where $E_n=\mathrm{EuclideanSpace},\mathbb{R},(\mathrm{Fin}(n+1))$ is the ambient Euclidean space of $S^n$. The unit sphere is the set of vectors of norm one about the origin.
Sibling poles already fix the north–south axis on $S^1$. The east point is the complementary equatorial reference: the pure first-coordinate unit vector. Together with its antipode (the west point), it supplies the two endpoints that split the circle into a pair of semicircle arcs.
Those arcs feed the circle-complement reduction used later for $H_1$-acyclicity statements about complements of embedded circles in $S^D$.
proof idea
Definitional construction, not a tactic proof. The point is packaged as the subtype element whose underlying vector is EuclideanSpace.single 0 1 (value $1$ in coordinate $0$, zero elsewhere). Membership in the unit sphere is discharged by rewriting through the zero-centered sphere–norm equivalence, the norm of a single-coordinate vector, and norm_one.
why it matters
Fixed reference point for all $S^1$ geometry in the singular-sphere stack. Downstream, amb_eastP_zero records that its ambient first coordinate is $1$; eastP_mem_inter and aW place it in the arc-intersection subtype; range_arcPlus_inter_arcMinus identifies the two semicircle ranges as meeting exactly at east and west; eastP_ne_westP separates the poles.
Those facts support isZero_h1_complement_of_embedding (Hatcher 2B.1, circle case): for $D\ge 1$, $D\neq 3$, every embedded circle in $S^D$ has $H_1$-acyclic complement once arc complements are acyclic. The $D\neq 3$ exclusion is the classical dimensional gap; the construction itself is pure topology and does not invoke the RS forcing chain (T5–T8) or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.