coord_zero_ne_zero
plain-language theorem explainer
On the unit circle with both poles removed, the first ambient Euclidean coordinate is never zero. Anyone building clopen arcs or sign charts on the doubly punctured S^1 cites this. The proof is a short case split: unit norm plus a vanishing first coordinate forces the second coordinate to be ±1, hence the point is a pole.
Claim. Let $x\in S^1\subset\mathbb{R}^2$ with $x\neq N$ and $x\neq S$ (north and south poles). Writing $x=(x_0,x_1)$ in ambient coordinates, one has $x_0\neq 0$.
background
The ambient space is Esp n = EuclideanSpace ℝ (Fin (n+1)), and Sph n is the unit sphere in that space as a topological space. Ambient coordinates of a sphere point are recovered by the coercion amb. The north pole is the last standard basis vector; the south pole is its negative.
On $S^1$ the ambient space is $\mathbb{R}^2$, so a point has coordinates $(x_0,x_1)$ with $x_0^2+x_1^2=1$. The lemma concerns the doubly punctured circle: $S^1$ minus the two poles. Upstream facts used here are unit norm of ambient points (norm_amb), injectivity of ambient coercion, coordinatewise extensionality in $\mathbb{R}^2$ (esp1_ext), the identity ambient(south) = −north, and the elementary real fact that $t^2=1$ implies $|t|=1$.
proof idea
Argue by contradiction: assume the first ambient coordinate vanishes. Unit norm plus the Euclidean sum-of-squares identity on Fin 2 forces the second coordinate squared to equal 1, hence its absolute value is 1 (abs_eq_one_of_sq_eq_one).
Case on the sign. If the second coordinate is $+1$, ambient coordinates match the north pole vector, so injectivity of amb and esp1_ext identify the point with the north pole, contradicting the hypothesis. If it is $-1$, the same comparison against ambient(south) $= -$north identifies the point with the south pole, again a contradiction.
why it matters
This is a local geometric fact inside SingularSphereGeometry, not a forcing-chain step. It feeds isClopen_arcA, whose closed half uses that on the relevant chart the coordinate never vanishes, so the sign split $\le 0$ / $\ge 0$ is well-defined and closed.
In the broader Recognition setting the singular-sphere apparatus supports discrete/continuous interface geometry (octave and covering constructions). The lemma is pure $S^1$ topology: it guarantees that the first coordinate is a genuine nonvanishing chart function off the poles, which is the algebraic input to clopen arc decompositions used later in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.