target_of_arcAcyclic
plain-language theorem explainer
Granting H₁-acyclicity of arc complements in every sphere dimension D ≥ 2 except D = 3, the public-spine campaign target is inhabited: a nonempty Alexander linking bridge that forces spatial dimension three from nontrivial linking. Dimension-forcing and public-spine authors cite it to discharge the linking-requires-D=3 gate without the old axiom. The proof is a one-line composition of the arc-conditional uniqueness half with the historical bridge reduction.
Claim. Assume that for every integer $D \ge 2$ with $D \neq 3$, every topological embedding of the unit interval into the $D$-sphere has $H_1$-acyclic complement. Then the public-spine target holds: there exists a fully inhabited Alexander linking bridge (nontrivial linking forces spatial dimension $D = 3$).
background
Recognition Science forces spatial dimension three along the T0–T8 chain; the linking half of that story lives on the public spine. The campaign target is the proposition that an Alexander linking bridge is nonempty: nontrivial (non-encoding) linking detects $D = 3$.
The remaining analytic frontier is arc-complement acyclicity (Hatcher 2B.1, arc case): every continuous embedding of the unit interval into $S^D$ has vanishing first homology on the complement. The high-dimension module packages that statement as a hypothesis parameter and proves that, granted it for all $D \ge 2$, $D \neq 3$, any dimension that detects nontrivial linking must equal three (low dimensions $0$ and $1$ are already banked unconditionally).
A separate reduction lemma on the public spine turns any such uniqueness statement into the inhabited bridge, because the $H_1(\mathrm{circle}) \cong \mathbb{Z}$ isomorphism and the $D = 3$ detection half are already proved.
proof idea
One-line term proof. First apply the sibling assembly lemma that turns the arc-acyclicity hypothesis into the uniqueness half: for every $D$, DetectsNontrivialLinking $D$ implies $D = 3$. Feed that uniqueness map into the public-spine reduction bridge_of_forces_D3, which packages the already-proved circle $H_1$ isomorphism, the $D = 3$ detection fact, and the uniqueness half into a witness of the nonempty Alexander linking bridge.
why it matters
This is the conditional assembly step that the unconditional closure theorem target_D3 instantiates. Downstream, PublicSpineLinkingClosure.target_D3 supplies the classical arc-complement acyclicity fact for every $D$ and obtains a fully inhabited Alexander linking bridge, bypassing the old DimensionForcing.linking_requires_D3 axiom on the public spine.
In the Recognition framework this closes the linking half of spatial-dimension forcing (T8 / T9 landmarks: $D = 3$). The campaign (P-d3link) keeps the target as a content-typed def so no free-Prop shortcut can discharge it; the real topology must inhabit the bridge. Once closed, the public spine no longer depends on an external dimension-forcing axiom for the linking route.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.