arcFun
plain-language theorem explainer
Parametrizes the upper or lower unit semicircle by t in [0,1]: the point (1-2t, s√(1-(1-2t)²)) on S¹, with s=±1 choosing the half. Anyone building continuous arcs or linking-vanishing arguments on the circle cites it. The body is a subtype package: build the Euclidean point and discharge circle membership by algebra.
Claim. For $s\in\mathbb{R}$ with $s^2=1$ and $t\in[0,1]$, let $\mathrm{arcFun}(s,t)$ be the point of the unit circle $S^1\subset\mathbb{R}^2$ with coordinates $(1-2t,\, s\sqrt{1-(1-2t)^2})$.
background
The ambient space is the unit circle as a topological space: $\mathrm{Sph},1$ is the unit sphere in Euclidean $\mathbb{R}^2$ (SingularSphereGeometry). Points of the plane are packaged by $\mathrm{pt2}(a,b)$, the $\ell^2$ vector $(a,b)$; membership in the unit circle is exactly $a^2+b^2=1$ via $\mathrm{pt2_mem_sphere}$.
The module develops linking-vanishing in high dimensions, building on the low-dimensional case. Semicircle arcs are the elementary paths used to cut the circle and control homology of complements. The sign $s$ with $s^2=1$ selects the upper ($s=+1$) or lower ($s=-1$) semicircle; the parameter $t$ runs the closed unit interval from the rightmost point through the left and back in projection.
proof idea
Definitional subtype construction. Form $\mathrm{pt2}(1-2t,, s\sqrt{1-(1-2t)^2})$ and prove it lies on the unit sphere by $\mathrm{pt2_mem_sphere}$. The needed identity $a^2+b^2=1$ is pure real algebra: bound $(1-2t)^2\le 1$ from $t\in[0,1]$ by nlinarith, rewrite $s^2\cdot(\sqrt{\cdots})^2$ with $s^2=1$ and $\mathrm{sq_sqrt}$, then ring. No continuity or injectivity is proved here.
why it matters
This is the raw path used throughout LinkingVanishingHighDim. Downstream it becomes the continuous map $\mathrm{arcMap}$, with continuity, coordinate projections, injectivity, and left/right inverse against the arc parameter all stated separately. Range lemmas for the plus and minus arcs feed the acyclicity and linking-detection statements that justify vanishing of linking in high dimensions. In the Recognition foundation stack this is geometric scaffolding for the sphere and octave geometry that later force $D=3$ and the eight-tick structure, not a physics claim by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.