ArcComplementsAcyclic
plain-language theorem explainer
Property that every topological embedding of the unit interval into the D-sphere has vanishing first singular homology on its complement (Hatcher 2B.1, arc case). The high-dimensional linking bridge cites it as the remaining classical frontier: granting it for all D ≠ 3 forces spatial dimension three. Defined as a Prop parameter, not proved in this file; classical topology supplies it via compact-support bisection.
Claim. For $D \in \mathbb{N}$, the predicate holds iff every continuous embedding $a : [0,1] \hookrightarrow S^D$ satisfies $H_1(S^D \setminus a([0,1]); \mathbb{Z}) = 0$ (the first singular homology of the complement is the zero $\mathbb{Z}$-module).
background
The ambient space is the unit $D$-sphere $S^D$ realized as the unit sphere in Euclidean space of dimension $D+1$. Singular homology $H_n(X;\mathbb{Z})$ is the degree-$n$ homology of the singular chain complex of a topological space $X$, packaged here as an object of the category of $\mathbb{Z}$-modules.
An arc means a continuous map from the unit interval that is a topological embedding. Its complement in $S^D$ is the open set of points not in the image. The predicate asserts that this complement is $H_1$-acyclic: the first homology group vanishes.
This module sits in the high-dimensional half of the linking-vanishing argument. Low dimensions $D=0,1$ are handled unconditionally elsewhere; for $D\ge 2$, $D\ne 3$, the circle-complement vanishing is reduced by Mayer–Vietoris to the arc case stated here. The classical reference is Hatcher, Algebraic Topology, Proposition 2B.1.
proof idea
Pure definition of a proposition: no proof obligations. The body quantifies over continuous maps $a$ from the unit interval into the $D$-sphere, assumes the map is a topological embedding, and asserts that the degree-1 singular homology of the complement (viewed as a topological space) is the zero object in the category of $\mathbb{Z}$-modules. Downstream theorems take an instance of this Prop as a hypothesis and discharge the circle case via Mayer–Vietoris on two semicircle arcs.
why it matters
This is the precisely stated remaining frontier for the uniqueness half of the spatial-dimension forcing. Downstream, forces_D3_of_arcAcyclic shows: if the predicate holds for every $D\ge 2$ with $D\ne 3$, then any dimension that detects nontrivial linking must equal 3. The circle-complement reduction (isZero_h1_complement_of_embedding) and the high-dimensional vanishing (not_detects_of_arcAcyclic) both take it as input; the public spine assembly re-exports the same conditional uniqueness.
In the Recognition Science forcing chain this closes the topological side of T8 ($D=3$ spatial dimensions): nontrivial linking of closed curves is possible only in three dimensions once arc complements are $H_1$-acyclic away from $D=3$. Dimensions 0 and 1 are already banked unconditionally. A separate formalization (arcComplementsAcyclic) aims to discharge the hypothesis in every dimension; until then the uniqueness theorem remains conditional on this classical fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.