D3_of_bridge
plain-language theorem explainer
Any dimension that admits a circle embedding with nontrivial complement homology must equal 3, once an Alexander linking bridge is given. Researchers cite this as the topological half of the D=3 forcing step (T8) on the public spine. The proof is a one-line field projection: the bridge already packages the uniqueness statement.
Claim. Given an Alexander linking bridge (a package asserting $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, that dimension 3 detects nontrivial linking, and that only dimension 3 does), for every natural number $D$: if some continuous embedding $S^1\hookrightarrow S^D$ has nonvanishing first singular homology of its complement, then $D=3$.
background
PublicSpine is the dual forcing surface of UnifiedForcingChain: a δ-stratified map that papers should cite for what is forced. Among its closed targets is the D=3 / eight-tick bridge. The detector used here is content-typed, not an arithmetic encoding: DetectsNontrivialLinking D means there exists a topological embedding of the circle into the D-sphere whose complement has non-zero first singular homology (Mathlib objects throughout).
An Alexander linking bridge packages three proved pieces: the isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, the positive detection that D=3 admits such a nontrivial complement (unknot complement retracts onto a core circle), and the uniqueness claim that only D=3 does. Full inhabitation lives in PublicSpineLinkingClosure (campaign P-d3link); vanishing for D=0,1 and for D=2 and D≥4 uses the excision spine and arc-complement acyclicity (Hatcher 2B.1, arc case).
Upstream, the same detector is restated in LinkingVanishingLowDim and LinkingVanishingHighDim; the constant D:=3 appears in GapDerivation and AlphaDerivation as the spatial dimension forced by T8/T9.
proof idea
One-line term proof: project the forces_D3 field of the given bridge. No new topology is argued here; the bridge structure already carries the universal statement ∀ D, DetectsNontrivialLinking D → D = 3, which was closed unconditionally in PublicSpineLinkingClosure via the circle-complement dichotomy.
why it matters
This is the public-spine export of the T8 landmark: spatial dimension D=3 is forced by nontrivial linking, not postulated. MODULE_DOC records the target as CLOSED (campaign P-d3link, 2026-07-18): AlexanderLinkingBridge is fully inhabited with zero sorry and only the standard classical axioms, without appealing to DimensionForcing.linking_requires_D3 and without arithmetic encoding predicates.
Contractually, T8/T7 on this surface must go through AlexanderLinkingBridge rather than SphereAdmitsCircleLinking. The content-typed binder kills the free-Prop encoding cheat (panel K1). Downstream used_by is currently empty on the graph; the declaration exists so papers and the dual spine can cite a theorem-shaped uniqueness fact rather than an open purchase. It sits beside circle_H1_holds, linking_still_encoding, and the forced tower as part of the honest δ-map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.