target_D3_from_nonencoding_linking
plain-language theorem explainer
Public-spine target that spatial dimension three is forced by nontrivial circle linking, without arithmetic encoding. Cite it for the dual forcing surface of T8 (D = 3) and as the first conjunct of the eight-tick bridge. The binder is the content-typed proposition that an Alexander linking bridge is inhabited; kept as a definition so only real topology can discharge it, with inhabitation proved in the linking-closure module.
Claim. The proposition that an Alexander linking bridge exists: $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ is available, some embedded circle in $S^3$ has nontrivial complement homology, and nontrivial circle linking forces spatial dimension $D=3$.
background
PublicSpine is the dual forcing surface of UnifiedForcingChain: a δ-stratified map for papers and loops that mean "what is forced." Contract rule: T8/T7 must go through a content-typed Alexander linking bridge, never through arithmetic predicates such as SphereAdmitsCircleLinking.
An Alexander linking bridge packages three proved pieces: the isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$; detection of nontrivial linking in dimension three (unknot complement retract); and the forcing statement that DetectsNontrivialLinking at dimension $D$ implies $D=3$, for arbitrary topological embeddings. The spatial dimension constant $D:=3$ is the T8/T9 landmark of the forcing chain.
This declaration is only the binder. Campaign P-d3link closed its inhabitation by real topology (excision spine, arc-complement acyclicity after Hatcher 2B.1, vanishing at low dimension), with no appeal to the older DimensionForcing axiom.
proof idea
One-line definitional wrapper: the target is definitionally Nonempty of the Alexander linking bridge structure. No tactics run here. Inhabitation is supplied downstream by PublicSpineLinkingClosure.target_D3, which applies the arc-acyclic assembly and the reduction bridge_of_forces_D3 (given the forcing half, the already-proved $H_1$ and $d3_detects$ fields complete the structure).
why it matters
This is the public T8 binder on the dual surface. Module doc states the D=3 / eight-tick bridge target is CLOSED (campaign P-d3link): the bridge is fully inhabited with zero sorry and only standard axioms, no encoding. Downstream, target_eight_tick_from_D3 is the conjunction of this target with CubePeriodEight; target_eight_tick_of_bridge reduces the eight-tick claim to this binder alone once the period half is known. DimensionEightTickOpen records the honest equality of the old open certificates with these content-typed binders. bridge_of_forces_D3 and the linking-assembly/closure theorems inhabit it. Framework landmarks: T8 ($D=3$ spatial dimensions) and, via the eight-tick consequent, T7 (period $2^3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.