arcFun_arcParam
plain-language theorem explainer
On the unit circle, the signed semicircle map sends the arc parameter of a point z back to z whenever the sign matches the second coordinate. Anyone identifying ranges of upper/lower semicircle paths with half-circles cites this left-inverse identity. The proof reduces to ambient-coordinate injectivity and cancels the parameter formula with the sphere relation x^{2}+y^{2}=1.
Claim. Let $s\in\mathbb{R}$ satisfy $s^2=1$, and let $z$ be a point of the unit circle $S^1\subset\mathbb{R}^2$. Write $z_i$ for the ambient $i$-th coordinate of $z$. If $s\cdot z_1=|z_1|$, then the semicircle arc map with sign $s$ applied to the arc parameter $t=(1-z_0)/2\in[0,1]$ recovers $z$.
background
The module develops vanishing of linking data in high dimensions by first controlling paths on the unit circle $S^1=\mathrm{Sph},1$. Points of $S^1$ are accessed through ambient coordinates $\mathrm{amb},z,i$, so two circle points agree once both coordinates agree.
The semicircle arc map sends $t\in[0,1]$ to $(1-2t,,s\sqrt{1-(1-2t)^2})$ on $S^1$, with $s=\pm 1$ selecting the upper or lower semicircle. The arc parameter of a circle point is the preimage $t=(1-z_0)/2\in[0,1]$. The elementary identity $z_0^2+z_1^2=1$ (coord_sq_add_sq) guarantees the square root is well-defined and recovers $|z_1|$.
Upper and lower continuous arcs (arcPlus, arcMinus) are specializations of this map at $s=\pm 1$. The present lemma is the section property needed to identify their images with the closed half-circles.
proof idea
Apply ambient-coordinate injectivity, then extend equality of the two ambient coordinates separately.
Coordinate 0: rewrite by arcFun_coord0 and cancel $1-2\cdot((1-z_0)/2)=z_0$ by ring.
Coordinate 1: rewrite by arcFun_coord1. The identity under the square root collapses, via coord_sq_add_sq and nlinarith, to $z_1^2$. Take Real.sqrt_sq_eq_abs, insert the sign hypothesis $s\cdot z_1=|z_1|$, and cancel $s\cdot(s\cdot z_1)=(s^2)z_1=z_1$ using $s^2=1$ and one_mul.
why it matters
Feeds the two range characterizations range_arcPlus and range_arcMinus, which identify the image of the upper (resp. lower) continuous semicircle with ${z\in S^1:z_1\ge 0}$ (resp. $\le 0$). Those range equalities are the geometric input for showing that arc complements are acyclic and that nontrivial linking is detected only in low dimension.
In the Recognition foundation stack this sits under LinkingVanishingHighDim, imported alongside SingularSphereGeometry and the low-dimensional linking module. It is pure circle geometry: no J-cost, phi-ladder, or forcing-chain step is invoked, but the acyclicity it enables is part of the topological scaffolding that later forces $D=3$ and the eight-tick octave (T7–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.