coordW
plain-language theorem explainer
Extracts the first ambient Euclidean coordinate of a point on the doubly punctured unit circle. Downstream lemmas use the sign of this coordinate to cut the circle into east and west arcs and prove those arcs are clopen. The body is a one-line projection through the ambient embedding of the unit circle.
Claim. Let $W_c$ be the doubly punctured unit circle (intersection of the two standard open covers of $S^1$). For $w \in W_c$, the coordinate $\mathrm{coord}_W(w) \in \mathbb{R}$ is the $0$-th ambient Euclidean coordinate of the underlying point of $w$ on $S^1 \subset \mathbb{R}^2$.
background
In this module the unit $n$-sphere $S^n$ is realized as the topological space of the Euclidean unit sphere in $\mathbb{R}^{n+1}$. The helper amb coerces a point of that space back to its ambient Euclidean vector.
The doubly punctured circle $W_c$ is the intersection of the two standard open covers of $S^1$ (each cover omits one pole). Points of $W_c$ therefore live on $S^1$ away from both poles, so the first ambient coordinate is a well-defined real-valued function on that space.
The local setting is singular-sphere geometry: charts and covers on low-dimensional spheres used to build clopen decompositions and homology generators for the Recognition foundation layer.
proof idea
Pure definition, not a proof. Coerce $w$ from $W_c$ to the underlying point of $S^1$, apply the ambient embedding into $\mathbb{R}^2$, and read index $0$. Continuity is proved separately by composing the continuous Euclidean projection with the two subtype valuations.
why it matters
This coordinate is the cutting function for the east arc of $W_c$: that arc is defined as the set where the coordinate is strictly positive. Membership lemmas for the distinguished east and west points, continuity of the coordinate, and the clopen property of the east arc all depend on it.
Those clopen arcs feed the point-difference class in $H_0$ of the two-arc intersection, part of the singular-sphere toolkit that supports discrete geometric constructions higher in the stack. It is infrastructure rather than a forcing-chain step (T0–T8), but it is the concrete real function that makes the east/west split rigorous.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.