arcFun_coord0
plain-language theorem explainer
On the unit circle, the semicircle arc map sends parameter t to a point whose first ambient coordinate is exactly 1−2t. Anyone proving injectivity of the arc map or inverting the arc parameterization cites this identity. The proof is definitional reflexivity: the coordinate is written that way in the arc constructor.
Claim. For every sign $s\in\mathbb{R}$ with $s^2=1$ and every $t\in[0,1]$, the ambient $0$-coordinate of the semicircle arc point at parameter $t$ equals $1-2t$.
background
The module builds high-dimensional linking-vanishing statements from singular sphere geometry and low-dimensional linking facts. Points of the unit sphere $S^1$ are handled via ambient Euclidean coordinates: amb simply reads the underlying vector in $\mathbb{R}^2$.
The semicircle arc arcFun is the standard parameterization $t\mapsto\bigl(1-2t,, s\sqrt{1-(1-2t)^2}\bigr)$ on the unit interval, with $s=\pm 1$ choosing the upper or lower semicircle. The first coordinate is therefore designed to run linearly from $1$ down to $-1$ as $t$ runs from $0$ to $1$. This lemma records that design choice as an equality of real numbers.
proof idea
One-line definitional proof (rfl). Unfolding arcFun builds a sphere point via pt2 whose first component is literally $1-2t$; amb projects to that ambient vector, so the $0$-th coordinate matches by construction.
why it matters
The identity is the computational engine behind two local lemmas. Injectivity of the arc map reduces equality of arc images to equality of first coordinates, then applies this formula twice and cancels. The left-inverse statement arcFun_arcParam likewise rewrites the first coordinate via this lemma when showing that reparameterizing a point on the chosen semicircle recovers the point.
In the broader Recognition foundation stack, these arc facts support acyclicity and linking-vanishing arguments on sphere complements (the module's ArcComplementsAcyclic / linking-detection interface). They are geometric scaffolding rather than a forcing-chain step (T5–T8), but they underwrite the topological side of the high-dimensional vanishing claims the module is assembling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.