arcMap
plain-language theorem explainer
Packages the semicircle path on S¹ as a ContinuousMap from the unit interval, with sign s = ±1 selecting upper or lower half. Downstream lemmas cite it for injectivity and embedding, and the named arcs arcPlus/arcMinus are thin wrappers. Construction is the ContinuousMap subtype pair of the pointwise arc function and its continuity lemma.
Claim. For real $s$ with $s^2=1$, there is a continuous map $[0,1]\to S^1$ whose underlying function is the semicircle $t\mapsto\bigl(1-2t,\, s\sqrt{1-(1-2t)^2}\bigr)$ (upper half when $s=+1$, lower when $s=-1$).
background
The ambient space is the unit circle $S^1$, written as the topological space of the unit sphere in Euclidean $\mathbb{R}^2$ (the $n=1$ case of the singular-sphere geometry setup). Points on that sphere are built via a two-coordinate helper that lands on the unit sphere once the squared coordinates sum to one.
The underlying path is the semicircle arc: as $t$ runs through the unit interval, the first coordinate runs linearly from $1$ to $-1$, and the second is $s$ times the positive square root that restores the sphere equation. The hypothesis $s^2=1$ forces $s=\pm 1$, so the construction covers exactly the upper and lower open semicircles (endpoints shared).
Continuity of that pointwise map is already proved by composing continuous operations (scalar arithmetic, square root on a nonnegative interval, and the sphere subtype constructor). This definition only lifts that continuous function into Mathlib's ContinuousMap type.
proof idea
One-line ContinuousMap constructor: the pair consisting of the pointwise semicircle function and the already-proved continuity lemma for that function. No extra analytic work happens here.
why it matters
Gives a single ContinuousMap object that the rest of the linking-vanishing development can quote. Immediate consumers are the named upper and lower arcs (sign $+1$ and $-1$), the injectivity lemma for the path, and the embedding lemma that upgrades continuity plus injectivity (with the Hausdorff structure on $S^1$) to a topological embedding.
Those embeddings feed the high-dimensional linking-vanishing story in this module: arcs on $S^1$ are the low-dimensional building blocks against which higher-dimensional linking and homology vanishing are compared. In the broader Recognition foundation this sits under the geometric side of the forcing chain (sphere geometry supporting dimensional and linking constraints), not under the J-cost or mass-ladder arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.