sq_coord0_le_one
plain-language theorem explainer
On the unit circle, the squared first ambient coordinate is at most 1. Anyone building arc parameters or semicircle charts on S^1 cites this bound. The proof is a one-shot nonlinear arithmetic step from the circle identity and nonnegativity of the second squared coordinate.
Claim. For every point $z$ on the unit circle $S^1\subset\mathbb{R}^2$, if $z_0$ denotes its first ambient coordinate, then $z_0^2\le 1$.
background
The ambient space is Euclidean $\mathbb{R}^{n+1}$ with the unit sphere $S^n$ realized as a topological space (Sph n). The helper amb extracts the underlying Euclidean coordinates of a sphere point. Here $n=1$, so points lie on the ordinary unit circle in $\mathbb{R}^2$.
The sibling lemma coord_sq_add_sq records the circle equation: for $z\in S^1$, $z_0^2+z_1^2=1$. Squared coordinates are nonnegative, so each separately is at most 1. The module develops linking-vanishing statements in high dimension and needs a clean parameter on the circle complement; the bound $z_0\in[-1,1]$ is the elementary geometric input for that parameterization.
proof idea
Apply nonlinear arithmetic (nlinarith) to two facts: the circle identity $z_0^2+z_1^2=1$ from coord_sq_add_sq, and $z_1^2\ge 0$ from sq_nonneg. Subtracting a nonnegative quantity from 1 immediately yields $z_0^2\le 1$. No case splits or explicit square roots are required.
why it matters
The sole direct consumer is arcParam, which sends $z\mapsto(1-z_0)/2$ into the unit interval. That map is the preimage parameter for the semicircle arc used to chart circle points when analyzing linking of arcs in the high-dimensional vanishing package. Without the squared bound, the constructor proof that $(1-z_0)/2\in[0,1]$ fails. In the Recognition foundation layer this is pure Euclidean bookkeeping supporting the geometric side of linking-vanishing arguments, not a forcing-chain step (T0–T8), but it keeps the arc calculus closed and sorry-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.