arcParam
plain-language theorem explainer
Maps a point z on the unit circle to the preimage parameter t=(1-z₀)/2 in the unit interval. Cited when inverting the semicircle arc maps t ↦ (1-2t, ±√(1-(1-2t)²)). The membership proof is a short nlinarith/linarith argument from the squared first-coordinate bound on S¹.
Claim. For a point $z$ on the unit circle $S^1 \subset \mathbb{R}^2$, define the arc parameter $t = (1 - z_0)/2 \in [0,1]$, where $z_0$ is the first ambient Euclidean coordinate of $z$.
background
The ambient space is the unit sphere $S^n$ realized as a topological space (Sph n): the unit sphere in Euclidean space of dimension $n+1$. The helper amb extracts ambient coordinates of a sphere point. Here $n=1$, so points are on the circle $S^1 \subset \mathbb{R}^2$.
The first coordinate of any circle point satisfies $z_0^2 \le 1$ (lemma sq_coord0_le_one), hence $z_0 \in [-1,1]$. The semicircle arc maps send $t \in [0,1]$ to $(1-2t,, s\sqrt{1-(1-2t)^2})$ with sign $s=\pm 1$ selecting upper or lower semicircle. The present definition is the coordinate preimage of that first component: solving $1-2t = z_0$ yields $t=(1-z_0)/2$.
The local module develops linking-vanishing statements in high dimension by controlling $H_1$ of arc complements on the circle; parameterizing those arcs is the geometric setup.
proof idea
Definitional construction of a unitInterval subtype. The real value is $(1 - \mathrm{amb}, z, 0)/2$. Membership in $[0,1]$ is proved by two short calculations from sq_coord0_le_one z (which gives $(\mathrm{amb}, z, 0)^2 \le 1$): nlinarith yields $\mathrm{amb}, z, 0 \le 1$ and $-1 \le \mathrm{amb}, z, 0$, then linarith closes $0 \le (1-z_0)/2 \le 1$. No further lemmas.
why it matters
Supplies the left-inverse parameter for the semicircle maps. Downstream, arcFun_arcParam shows that applying the arc map at this parameter recovers $z$ (under the matching sign condition on the second coordinate). The range lemmas range_arcPlus and range_arcMinus identify the images of the upper and lower arc maps with the closed hemispheres ${z_1 \ge 0}$ and ${z_1 \le 0}$ on $S^1$; both rely on this preimage to hit an arbitrary point in the hemisphere.
Those range facts feed the acyclicity of arc complements used in the linking-vanishing argument for high-dimensional spheres. In the Recognition foundation stack this is pure geometric scaffolding (circle parameterization), not a forcing-chain step (T0–T8), but it underwrites the topological side of the singular-sphere geometry imported here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.