amb_southP_zero
plain-language theorem explainer
On the unit circle S¹, the south pole has vanishing first ambient coordinate. Geometric lemmas about the open cover of the doubly punctured circle cite this when ruling out pole collisions. The proof rewrites via the south-pole ambient formula, then applies the known vanishing of the north-pole vector at index 0 and neg_zero.
Claim. Let $S^1$ be the unit circle in $\mathbb{R}^2$. If $s$ denotes the south pole of $S^1$ and $\mathrm{amb}(s)\in\mathbb{R}^2$ its ambient coordinates, then the first coordinate satisfies $\mathrm{amb}(s)_0=0$.
background
The module develops the singular-sphere geometry used in the foundation layer: the $n$-sphere Sph n is the unit sphere in Euclidean space $\mathbb{R}^{n+1}$, with north-pole vector the last standard basis vector and south pole its negative. Ambient coordinates amb are the coercion from a point of the topological sphere back into that Euclidean space.
For $n=1$ one works on the circle in $\mathbb{R}^2$. The north-pole vector is $(0,1)$, so its zeroth coordinate vanishes (northV_zero). The companion identity amb_southP records that the ambient image of the south pole is exactly the negation of the north-pole vector, hence $(0,-1)$.
These facts feed the open-cover calculus on the doubly punctured circle (covers omitting the two poles), which is the local setting for later intersection and chart arguments.
proof idea
Term-mode rewrite chain. First replace amb(southP 1) by -(northV 1) via amb_southP. Pointwise evaluation of the negation is definitional, so the goal becomes -(northV 1 0)=0. Apply northV_zero to obtain -0=0, then close with neg_zero.
why it matters
Feeds the membership proofs eastP_mem_inter and westP_mem_inter, which place the east and west poles in the intersection of the two standard open covers of the doubly punctured circle. Those lemmas proceed by contradiction: if an equatorial point coincided with the south pole, its ambient first coordinate would vanish, contradicting the equatorial vanishing lemmas once rewritten through this identity.
In the Recognition foundation stack this is pure geometric scaffolding for the singular-sphere model that sits under the T-minus-1 to T8 bridge and the primitive-distinction forcing chain. It does not itself force a physical constant; it keeps the circle-cover calculus honest so later uniqueness and dimension arguments can quote clean open-set facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.