continuous_arcFun
plain-language theorem explainer
For each sign s with s² = 1, the semicircle parametrization t ↦ (1−2t, s√(1−(1−2t)²)) from the unit interval into the unit circle is continuous. Anyone packaging that arc as a C(I, S¹) map or proving it is an embedding cites this. The proof is a short term-mode continuity argument: subtype of ℓ², then coordinatewise fun_prop.
Claim. Let $s \in \mathbb{R}$ satisfy $s^2 = 1$. The map $t \mapsto \bigl(1-2t,\, s\sqrt{1-(1-2t)^2}\bigr)$ from the unit interval $[0,1]$ into the unit sphere $S^1 \subset \mathbb{R}^2$ is continuous.
background
The ambient module builds high-dimensional linking-vanishing statements by reducing nontrivial linking to low-dimensional sphere geometry. The unit sphere Sph 1 is the usual $S^1$ in Euclidean 2-space; points are assembled by a two-coordinate constructor that lands on the sphere once the squared coordinates sum to one.
The arc under study is the semicircle path on that circle: parameter $t$ runs through the unit interval, the first coordinate is the linear ramp $1-2t$ (from $+1$ to $-1$), and the second is $s$ times the positive square root that restores the circle equation. The hypothesis $s^2=1$ forces $s=\pm 1$, selecting the upper or lower semicircle.
Continuity of this path is the analytic prerequisite for treating it as a continuous map $C(I,S^1)$ and later as a topological embedding used in linking arguments.
proof idea
The target is a subtype of an $\ell^2$ product, so the proof applies Continuous.subtype_mk, then composes with PiLp.continuous_toLp. It remains to check continuity of the two real coordinate functions on the unit interval. After continuous_pi and fin_cases on the two indices, each coordinate is discharged by fun_prop: the first is affine in $t$, the second is a composition of continuous operations (multiplication by the fixed sign $s$, square, subtraction from 1, and real square root) on the same affine expression.
why it matters
This lemma is the continuity witness that turns the raw arc function into arcMap, the bundled continuous map $C(I,S^1)$. That map is then fed to isEmbedding_arcMap, which upgrades continuity plus injectivity to a topological embedding of the semicircle into the circle.
In the Recognition foundation stack, such embedded arcs are the geometric probes used when arguing that linking classes vanish (or become detectable) once dimension is high enough relative to the eight-tick / $D=3$ forcing chain. Without a continuous arc, the later closed-embedding and homology-vanishing steps have nothing to push forward. The result is pure topology; it does not itself invoke J-cost or the Recognition Composition Law, but it sits on the geometric side of the continuum bridge that those algebraic structures eventually meet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.