bridge_of_forces_D3
plain-language theorem explainer
Given that only dimension 3 can detect nontrivial circle linking in the sphere, the public-spine D=3 linking target follows. The argument packages the unconditional circle homology isomorphism H₁(S¹;ℤ)≅ℤ with the proved D=3 detection fact and the universal forcing hypothesis. Downstream arc-acyclicity assembly cites it to inhabit the Alexander linking bridge without the old DimensionForcing axiom. Proof is a one-line structure constructor.
Claim. Assume that for every natural number $D$, if some continuous embedding $S^1\hookrightarrow S^D$ has complement with nontrivial first singular homology, then $D=3$. Then the public-spine target asserting spatial dimension $3$ from non-encoding linking holds (i.e., the Alexander linking bridge package is inhabited).
background
PublicSpine is the dual forcing surface to UnifiedForcingChain: a δ-stratified map of what Recognition Science claims is forced, kept separate from the Boolean certificate spine. Among its closed targets is the D=3 / eight-tick bridge (campaign P-d3link): T8 in the forcing chain, that spatial dimension equals 3 because only then can an embedded circle link nontrivially.
The detector DetectsNontrivialLinking D is the non-encoding formulation (panel K1): there exists a continuous embedding $f:S^1\to S^D$ such that the first singular homology of the complement is not the zero object. This is stated on Mathlib topological objects, not on an abstract name-firewall predicate that could be inhabited by the empty detector.
Upstream, circleH1ZIsoInt_holds supplies $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ unconditionally (winding plus zero-winding filling, no remaining hypotheses). The detection half at $D=3$ uses the flat unknot $z\mapsto(z,0,0)$ in $S^3$, whose complement retracts onto a core circle, so nontrivial $H_1$ of the circle is a retract of the complement homology.
proof idea
Term-mode structure inhabitation, not a tactic script. The target type is a nested pair (or triple) whose three fields are filled by:
CircleWindingChain.circleH1ZIsoInt_holds— the unconditional isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$;detectsNontrivialLinking_three— the proved fact that $D=3$ does detect nontrivial linking (unknot-complement retract);- the hypothesis $h$ — $\forall D$, detection implies $D=3$.
No rewriting or case analysis: the constructor of target_D3_from_nonencoding_linking is applied directly to that triple. The historical campaign shape was exactly this reduction; the premise $h$ is discharged later by arc-complement acyclicity arguments.
why it matters
This is the historical reduction shape of campaign P-d3link on the public spine. It converts a universal forcing statement (only $D=3$ detects nontrivial linking) into the content-typed binder target_D3_from_nonencoding_linking, which is the honest replacement for the old T8 certificate that appealed to DimensionForcing.linking_requires_D3.
Downstream, PublicSpineLinkingAssembly.target_of_arcAcyclic applies this lemma after deriving the forcing hypothesis from arc-complement acyclicity (Hatcher 2B.1, arc case) for $D=2$ and $D\ge 4$, together with vanishing at $D=0,1$. Module doc records the bridge as CLOSED: fully inhabited in PublicSpineLinkingClosure with axioms only propext, Classical.choice, Quot.sound, no encoding predicates.
Framework landmark: T8 ($D=3$ spatial dimensions) on the dual surface, paired with T7 (eight-tick octave, period $2^3$) via the cube-period pigeonhole. Papers that mean "what is forced" should cite this module, not UFC names as architecture claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.