AlexanderLinkingBridge
plain-language theorem explainer
Packages the three topological ingredients that force spatial dimension three from genuine circle linking: the circle's first homology is ℤ, some embedded circle in S³ has nontrivial complement homology, and no other dimension admits that obstruction. Anyone citing the public D=3 target or the eight-tick bridge uses this binder. It is a content-typed Prop structure; inhabitation is supplied elsewhere by the unknot retract and the circle-complement dichotomy.
Claim. An Alexander linking bridge is a triple of assertions: (i) $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$; (ii) there exists a topological embedding $f:S^1\hookrightarrow S^3$ whose complement has nonzero first singular homology; (iii) for every dimension $D$, if some embedded circle in $S^D$ has nontrivial complement $H_1$, then necessarily $D=3$.
background
PublicSpine is the dual forcing surface to UnifiedForcingChain: a δ-stratified map of what is forced, kept free of arithmetic encoding predicates. Contract rule 3 requires T8 (spatial dimension) to cite a content-typed linking binder, never the old SphereAdmitsCircleLinking encoding.
The detector DetectsNontrivialLinking D asserts existence of a continuous embedding $f:S^1\to S^D$ such that the first singular homology of the complement is not the zero object. That is the real Alexander/linking obstruction on Mathlib spaces, not a name-firewall Prop.
Upstream pieces: circleH1ZIsoInt certifies $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ as a Mathlib module isomorphism; low- and high-dimension vanishing modules restate the same detector and prove it fails for $D\neq 3$ once arc complements are $H_1$-acyclic (Hatcher 2B.1 arc case, via Mayer–Vietoris/excision).
proof idea
No proof body: this is a structure declaration packaging three Props. Field h1 is the already-proved circle homology isomorphism certificate. Field d3_detects is witnessed by the flat unknot $z\mapsto(z,0,0)$ in $S^3$, whose complement retracts onto a core circle, so nontrivial $H_1$ pulls back. Field forces_D3 is the uniqueness half: vanishing at $D=0,1$ (totally disconnected / low-dim arguments) and at $D=2$ and $D\ge 4$ by the excision spine plus arc-complement acyclicity, assembled unconditionally in PublicSpineLinkingClosure.forces_D3.
why it matters
This binder is the closed public target for T8 (D=3 spatial dimensions) on the dual spine. Downstream, target_D3_from_nonencoding_linking is exactly Nonempty of this structure; D3_of_bridge projects the uniqueness field; DimensionEightTickOpen equates the honest D=3/eight-tick disclosure to inhabitation of this bridge plus cube period eight. Closure theorems forces_D3 and forces_D3_of_arcAcyclic inhabit or discharge it without appealing to the old arithmetic encoding or DimensionForcing.linking_requires_D3.
In the forcing chain this is the topological content behind T8: linking obstruction exists only in three dimensions, feeding the eight-tick octave (T7, period $2^3$) once D is fixed. Campaign P-d3link moved the binder from OPEN to fully inhabited (0 sorry; axioms only propext, Classical.choice, Quot.sound).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.