coord_sq_add_sq
plain-language theorem explainer
On the unit circle $S^1$, ambient coordinates of any point satisfy the circle equation $x_0^2+x_1^2=1$. Arc-parameter and semicircle-intersection lemmas in the high-dimensional linking-vanishing development cite it as the basic norm identity. The proof is a short rewrite of the Euclidean norm-squared formula using unit norm of sphere points and the two-term Fin sum.
Claim. For every point $z$ on the unit circle $S^1\subset\mathbb{R}^2$, writing $x_i$ for its ambient Euclidean coordinates, one has $x_0^2+x_1^2=1$.
background
The ambient space is Euclidean space $\mathbb{R}^{n+1}$ with the standard $\ell^2$ norm. The object $\mathrm{Sph},n$ is the unit sphere in that space, realized as a topological space (TopCat). For $n=1$ this is the ordinary circle $S^1\subset\mathbb{R}^2$.
The helper $\mathrm{amb}$ extracts the underlying Euclidean vector of a sphere point (a coercion across the TopCat packaging). The lemma $\mathrm{norm_amb}$ records that every such vector has norm $1$. Together these are the only geometric inputs needed for the circle equation in coordinates.
This module develops linking-vanishing statements in high dimension, building on singular sphere geometry and the low-dimensional linking package. The circle equation is the elementary algebraic identity that later arc and semicircle constructions rely on.
proof idea
Start from the identity that the squared Euclidean norm of $\mathrm{amb},z$ equals the sum of squares of its coordinates. Rewrite using unit norm of sphere points ($|\mathrm{amb},z|=1$, so the squared norm is $1$) and expand the Fin-sum over the two indices $0,1$. Symmetrize and clear absolute values via $|t|=|t|$ and $|t|^2=t^2$ to obtain $x_0^2+x_1^2=1$.
why it matters
The lemma is the coordinate form of "$S^1$ is the unit circle," and it is consumed immediately by three siblings in the same module. First, $\mathrm{sq_coord0_le_one}$ deduces $x_0^2\le 1$ by nonnegativity of the second square, which bounds the first coordinate in $[-1,1]$. Second, $\mathrm{arcFun_arcParam}$ uses the identity when reconstructing a circle point from its arc parameter. Third, $\mathrm{range_arcPlus_inter_arcMinus}$ identifies the two semicircle ranges as meeting exactly at the east and west poles; the circle equation keeps those constructions on $S^1$.
In the broader Recognition foundation this sits inside the geometric scaffolding for linking-vanishing arguments on spheres, not in the T0–T8 forcing chain itself. It is pure Euclidean geometry, but without it the arc decompositions used downstream would not typecheck as maps into $\mathrm{Sph},1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.