sph0_eq_pole
plain-language theorem explainer
Every point of the unit 0-sphere is exactly one of the two poles. Cite this for the base case of sphere topology or homology: S^0 is a two-point set. The proof reads the unit-norm condition in R^1 as a squared coordinate equal to 1, splits on the absolute value, and matches ambient vectors to the poles by injectivity.
Claim. For every point $x$ of the unit $0$-sphere $S^0 \subset \mathbb{R}^1$, either $x$ equals the north pole or $x$ equals the south pole.
background
In this module the $n$-sphere is the unit sphere in Euclidean space $\mathbb{R}^{n+1}$ (as a TopCat object). Ambient coordinates of a sphere point are the underlying vector in that Euclidean space; the ambient map is injective on the subtype. The north pole is the last standard basis vector on the sphere; the south pole is its negative.
For $n=0$ the ambient space is one-dimensional, so a point is a single real coordinate of absolute value 1. Coordinatewise extensionality on $\mathrm{Esp},0$ says two vectors agree once their sole coordinate agrees. A short local lemma converts $t^2=1$ into $|t|=1$.
The local setting is singular-sphere geometry: poles, open covers, and discrete structure needed before homology of spheres.
proof idea
Start from unit ambient norm. Expand the Euclidean squared-norm identity on $\mathrm{Fin},1$: the single squared coordinate equals 1. Pass to absolute value via the local square-to-abs lemma, then case-split $|t|=1$ into $t=1$ and $t=-1$.
In the positive case, injectivity of ambient plus $\mathrm{Esp},0$ extensionality identifies the point with the north pole (last basis vector evaluates to 1). In the negative case, the same tools plus the ambient formula for the south pole identify it with the south pole (negative of the north vector).
why it matters
This is the combinatorial base of $S^0$: two distinct poles and nothing else. Immediately afterward the file uses it to prove $S^0$ is finite (inject into Bool by testing equality with the north pole, then exhaust the four pole combinations) and therefore carries the discrete topology. That discrete two-point space is the stated base case for vanishing of positive-degree homology of $S^0$.
In the broader Foundation layer this anchors sphere geometry before inductive or covering arguments on higher spheres. It does not itself touch the forcing chain (T5–T8) or the Recognition Composition Law; it is pure topological scaffolding those later geometric claims may sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.