arcComplementsAcyclic
plain-language theorem explainer
Every topological embedding of the unit interval into the D-sphere has H₁-acyclic complement, for every dimension D. This is Hatcher's arc case of Alexander duality (2B.1), formalized. Linking-vanishing arguments in high dimension cite it to kill nontrivial linking outside D=3. The proof is a nested bisection of bad intervals whose limit point has contractible complement, forcing a bounding chain that eventually escapes the arc image.
Claim. For every $D \in \mathbb{N}$ and every topological embedding $a \colon I \hookrightarrow S^D$ of the unit interval, the first singular homology of the complement vanishes: $H_1(S^D \setminus a(I)) = 0$.
background
The ambient space is the unit sphere $S^D \subset E^D$ (Euclidean $D$-space). An arc here is a continuous injective map $a$ from the unit interval into that sphere. The claim is that the complement of its image is $H_1$-acyclic: every 1-cycle in the complement bounds.
Locally the module packages a bisection invariant Bad: a closed subinterval $[u,v] \subseteq [0,1]$ is bad when the pushforward of a fixed reference 1-cycle into the complement of $a([u,v])$ is not a boundary. A recursive sequence of nested bad intervals (badSeq) halves width at each step while preserving the non-bounding property.
Upstream, contractibility of the complement of a point in $S^D$ supplies vanishing of $H_1$ on that open set, and chain-map naturality moves cycles between nested open complements. The result is the arc case of Hatcher's Alexander duality statement used by the high-dimensional linking-vanishing layer.
proof idea
Assume for contradiction an embedding $a$ whose complement carries a nonbounding 1-cycle $z$. The full interval $[0,1]$ is bad. Bisect repeatedly: at each stage at least one half remains bad, producing nested intervals of width $2^{-k}$ whose left endpoints $s_k$ are bounded above. Their supremum $t^$ lies in $[0,1]$; write $p = a(t^)$.
The complement of the singleton ${p}$ is contractible, so $H_1$ there is zero and the image of $z$ bounds some 2-chain $w$. The compact support $K$ of $w$ misses $p$. Continuity of $a$ yields an $\varepsilon$-neighbourhood of $t^*$ whose arc image avoids $K$. For large $k$ the $k$-th bad interval sits inside that neighbourhood, so its arc image misses $K$ and $z$ would bound in that smaller complement, contradicting badness.
why it matters
This theorem is the geometric engine behind unconditional dimension forcing on the public spine. Downstream, forces_D3 states that nontrivial linking detection implies $D=3$: dimensions $0,1$ vanish by low-dimensional linking, while $D=2$ and $D\ge 4$ reduce via Mayer-Vietoris to this arc-complement acyclicity fact. The companion target_D3 inhabits the full Alexander linking bridge without the older linking_requires_D3 axiom.
In the Recognition forcing chain this closes the geometric half of T8 (spatial dimension three): linking is possible only when arc complements fail to be acyclic in the way high-dimensional spheres force. Together with the eight-tick octave (T7) and $\varphi$-fixed-point structure (T6), it pins the ambient dimension used by the mass ladder and the $\alpha$ band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.