amb_eastP_zero
plain-language theorem explainer
On the unit circle, the east pole has first ambient coordinate equal to 1. Circle-cover and linking arguments cite this to separate east from west and to place the east pole in open charts and arc intersections. The proof reduces to the definition of the standard basis vector via EuclideanSpace.single.
Claim. If $E$ denotes the east point of the unit circle $S^1\subset\mathbb{R}^2$ (the point with ambient coordinates $(1,0)$), then the $0$-th ambient coordinate of $E$ equals $1$.
background
The module equips the unit $n$-sphere as a topological space: $\mathrm{Sph},n$ is the unit sphere in Euclidean space $\mathbb{R}^{n+1}$. Ambient coordinates are the underlying vector of a sphere point (a coercion helper across the $\mathrm{TopCat}$ packaging).
On the circle ($n=1$), the east point is the standard basis vector $e_0=(1,0)$: it is defined as $\mathrm{EuclideanSpace.single},0,1$, which lies on the unit sphere because that single has norm one. The west point is the opposite basis direction. These two poles anchor semicircle arcs and the two-chart cover used later in the singular-sphere geometry.
The ambient-coordinate map simply forgets the sphere subtype, so evaluating it at index $0$ on the east point is exactly reading the first component of $e_0$.
proof idea
Unfold the claim to the concrete vector identity $\mathrm{EuclideanSpace.single},(0:\mathrm{Fin},2),1,,0=1$. Rewrite with $\mathrm{EuclideanSpace.single_apply}$: the coordinate at index $i$ is $1$ when $i=0$ and $0$ otherwise. The branch $i=0$ fires by $\mathrm{rfl}$, so the value is $1$.
why it matters
The lemma is a one-line coordinate fact that unlocks several geometric membership and separation statements on $S^1$. Downstream, $\mathrm{eastP_ne_westP}$ distinguishes east from west by comparing zeroth ambient coordinates ($1$ versus $-1$). $\mathrm{eastP_mem_inter}$ places the east pole in the intersection of the two standard open covers by ruling out coincidence with the south pole. $\mathrm{aW_mem_arcA}$ uses the same identity to show a positive west-coordinate witness on an arc. In the linking module, the two semicircle ranges meet exactly at east and west; this coordinate pin is part of that intersection calculus.
Within Recognition Science foundation work, singular-sphere geometry supports higher-dimensional linking-vanishing arguments that feed the forcing chain's dimensional and topological constraints (notably the $D=3$ and eight-tick landmarks upstream of physical constants). The lemma itself is pure Euclidean bookkeeping, not a physical claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.