amb_northP_zero
plain-language theorem explainer
On the unit circle S¹, the ambient Euclidean coordinates of the north pole vanish in the first slot. Chart-cover arguments for the singular sphere cite this when ruling out pole collisions. The proof is a one-line reduction to the corresponding fact for the north-pole basis vector.
Claim. Let $S^1$ be the unit circle in $\mathbb{R}^2$. Writing $\mathrm{amb}$ for the ambient $\mathbb{R}^2$-coordinates of a point of $S^1$, if $N$ denotes the north pole then $\mathrm{amb}(N)_0 = 0$.
background
The module builds the singular-sphere geometry used in the Recognition foundation layer. Sph n is the unit sphere in Euclidean space $\mathbb{R}^{n+1}$ packaged as a topological space; for $n=1$ this is the circle $S^1\subset\mathbb{R}^2$.
The north pole is the last standard basis vector, realized first as a vector northV and then as a sphere point northP. The helper amb simply reads off the underlying Euclidean coordinates of a sphere point (coercion across TopCat.of).
The sibling lemma northV_zero already records that the first coordinate of that basis vector is zero: northV 1 0 = 0. The present statement lifts that vector identity to the sphere-point language used by the chart covers.
proof idea
One-line wrapper: the ambient coordinates of northP 1 are definitionally northV 1, so the claim is exactly northV_zero.
why it matters
Feeds the membership lemmas eastP_mem_inter and westP_mem_inter, which place the east and west poles in the intersection of the two standard open covers of $S^1$. Those covers (and the fact that poles sit cleanly outside each other's singular charts) are the geometric substrate for the singular-sphere constructions imported from SingularSphere.
In the broader Recognition stack this geometry supports the eight-tick / octave bookkeeping (T7) and the three-dimensional forcing (T8) by giving a clean model of $S^1$ with controlled chart singularities. The lemma itself is pure coordinate bookkeeping, but without it the cover-intersection arguments do not typecheck.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.