abs_eq_one_of_sq_eq_one

The module develops elementary geometry of the unit spheres Sph n inside Euclidean space: ambient coordinates, north and south poles, and open covers used for singular-sphere constructions in the Recognition foundation.

Norm identities are the usual source of squared-coordinate constraints. If $|x|=1$ in ambient Euclidean space, the sum of squares of coordinates equals 1; in dimension 0 or after other coordinates vanish, a single real $t$ satisfies $t^{2}=1$. Passing from that identity to $|t|=1$ is the elementary real-analysis step recorded here.

The only named upstream dependency in the graph is a zero-product fact (a*b=0 implies a factor vanishes). In the proof body that role is played by the standard real factorization of $|t|^{2}-1$.

From $t^{2}=1$ rewrite $|t|^{2}=1$ via sq_abs. Nonlinear arithmetic rearranges to $(|t|-1)(|t|+1)=0$. Case-split on the zero-product property. The first factor zero is $|t|=1$ by linear arithmetic. The second factor zero is $|t|=-1$, which contradicts abs_nonneg. Eight-line tactic proof; no external sphere lemmas.

Local utility lemma inside singular-sphere geometry. Downstream it discharges the squared-coordinate step in sph0_eq_pole (every point of $S^{0}$ is a pole) and in coord_zero_ne_zero (on the doubly punctured circle the first ambient coordinate never vanishes). It is also used when identifying the intersection of the two semicircle ranges with the east and west points in high-dimensional linking-vanishing arguments.

Those facts support the geometric scaffolding around the singular sphere that the foundation uses when organizing covers, poles, and linking data. The lemma itself is pure real arithmetic; its place in the chain is only as a reusable bridge from norm-square identities to absolute-value conclusions.