northV_zero
plain-language theorem explainer
The north-pole basis vector in ambient dimension 2 has vanishing zeroth coordinate. Anyone working with stereographic charts or ambient coordinates on the doubly punctured circle cites this. The proof is a one-line rewrite through the definition of the last standard basis vector and the pointwise evaluation of EuclideanSpace.single.
Claim. Let $e_N$ be the north-pole vector in Euclidean space of type $\mathrm{Esp}\,1$ (the last standard basis vector of $\mathbb{R}^2$). Then its zeroth coordinate vanishes: $(e_N)_0 = 0$.
background
The module develops singular sphere geometry for Recognition Science: spheres with poles removed so that stereographic charts cover the rest. Ambient space is Esp n, Euclidean space indexed by Fin (n+1). The unit sphere Sph n sits inside it.
The north-pole vector is defined as the last standard basis vector: northV n := EuclideanSpace.single (Fin.last n) 1. For n = 1 this is the vector with a 1 in the final slot of Fin 2 and zeros elsewhere. The north and south poles northP, southP are the corresponding points on the sphere; ambient projection amb recovers the underlying vector.
Coordinate nonvanishing on the doubly punctured circle is the local goal. Knowing that the north-pole vector itself has a zero in the first slot is the elementary fact that feeds the pole lemmas and the nonvanishing argument.
proof idea
One-line wrapper. Unfold northV to EuclideanSpace.single (Fin.last 1) 1, apply the pointwise formula for single, and discharge the branch with if_neg: the index 0 is not Fin.last 1 (decided by decide), so the entry is zero.
why it matters
Feeds three local lemmas: ambient north-pole coordinate zero (amb_northP_zero is literally this fact), ambient south-pole coordinate zero (via negation of the north vector), and the key nonvanishing statement coord_zero_ne_zero: on the doubly punctured circle the first ambient coordinate never vanishes.
That nonvanishing underwrites chart domains and coordinate functions away from the poles. In the broader foundation stack this is scaffolding for singular-sphere geometry used when Recognition Science needs clean stereographic or radial coordinates on low-dimensional spheres (eight-tick and octave geometry live nearby in the forcing chain, though this lemma itself is pure Euclidean bookkeeping).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.