westP
plain-language theorem explainer
The west point on the unit circle S¹ is the antipode of the east point under the ambient Euclidean embedding. Geometers working the circle-complement and linking-vanishing arguments cite it as a fixed endpoint of the two semicircle arcs. The definition is a one-line negation of the already-constructed east point.
Claim. Let $E_1 = \mathbb{R}^2$ with the Euclidean norm, and let $S^1$ be the unit sphere about the origin in $E_1$. The west point of $S^1$ is the antipodal image of the east point: if the east point is the standard basis vector $e_0$, the west point is $-e_0$.
background
The ambient space Esp n is Euclidean space $\mathbb{R}^{n+1}$ indexed by Fin (n+1). The unit sphere about the origin in that space is the model of $S^n$ used throughout the module. For $n=1$ one works in the plane, so the unit circle is a subset of $\mathbb{R}^2$.
The east point is the standard positive basis vector along the first coordinate, already shown to lie on the unit sphere. Negation in the ambient Euclidean space restricts to the antipodal map on the sphere, so the west point is well-defined as a point of $S^1$ once the east point is.
Local setting is singular-sphere geometry supporting the circle-complement reduction: two open semicircle arcs whose closures meet exactly at the east and west endpoints, used later for Mayer–Vietoris on complements in $S^D$.
proof idea
One-line definition: apply ambient negation to the already-constructed east point. Sphere membership is automatic because the unit sphere is centrally symmetric (equivalently, the coe-neg-sphere identity used downstream). No separate norm check is needed at this declaration.
why it matters
Supplies one of the two fixed endpoints that pin the semicircle decomposition of $S^1$. Downstream, range_arcPlus_inter_arcMinus records that the two arc images meet exactly at the east and west points; eastP_ne_westP separates them by reading the first ambient coordinate; amb_westP_zero evaluates that coordinate as $-1$; and bW packages the west point as a point of the two-arc intersection used for $H_0$ difference classes.
Those facts feed isZero_h1_complement_of_embedding, the circle-complement reduction (Hatcher 2B.1, circle case): for $D\ge 1$, $D\ne 3$, every embedded circle in $S^D$ has $H_1$-acyclic complement once arc complements are acyclic. In the Recognition forcing chain this is geometric scaffolding for the $D=3$ exceptional case (T8), not a direct physics identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.