amb_westP_zero
plain-language theorem explainer
On the unit circle, the west pole has ambient first coordinate equal to $-1$. Anyone working the singular-sphere cover or the two-arc linking setup cites this as the coordinate pin for the antipode of the east point. The proof is a short term rewrite: west is minus east, and the standard basis single at index $0$ evaluates to $1$, so the sign flips.
Claim. Let $S^1$ be the unit circle in $\mathbb{R}^2$. Write $\mathrm{amb}$ for the ambient Euclidean coordinates of a point of $S^1$, and let $W$ be the west point (the antipode of the east point $E = e_0$). Then $\mathrm{amb}(W)_0 = -1$.
background
The module equips the unit spheres $S^n \subset \mathbb{R}^{n+1}$ as topological spaces Sph n, with ambient coordinate coercion amb extracting the underlying Euclidean vector. On the circle $n=1$, the east point is the first standard basis vector $e_0 = (1,0)$, and the west point is defined as its antipode $-E$.
These poles anchor the open covers and the two semicircular arcs used later for linking and intersection arguments. The ambient first coordinate is the natural test functional that separates east from west and decides membership in the arc and cover sets.
Upstream, the geometry sits in the Foundation layer that packages sphere charts and poles before higher-dimensional linking-vanishing statements.
proof idea
Term-mode rewrite. First apply the sphere-coe identity for negation of a sphere point to replace amb(westP) by $-(e_0)$ in $\mathbb{R}^2$. Then evaluate at index $0$: negation passes through the coordinate, EuclideanSpace.single at matching index returns $1$, and the if_pos branch fires, yielding $-1$.
why it matters
This is the coordinate fact that makes east and west distinguishable and places west correctly relative to the arc/cover predicates. Downstream, eastP_ne_westP obtains $E \neq W$ by comparing ambient zeroth coordinates ($1$ vs $-1$). The two-arc intersection lemma uses the same poles as the exact meeting set of the semicircles. Locally, westP_mem_inter and bW_notMem_arcA rewrite through this identity to settle cover membership and arc non-membership by a norm_num on $-1$.
In the broader Recognition foundation, the singular-sphere geometry supports linking-vanishing arguments in high dimension that feed the structural side of the forcing chain; this lemma is a low-level pin, not a chain step itself, but without it the pole-separation and arc-intersection layer does not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.