linking_nontrivial_iff_D3
plain-language theorem explainer
Nontrivial integer linking of embedded loops holds precisely when the ambient dimension equals three. Researchers establishing the topological veto in Recognition Science foundations would cite this result when deriving spatial dimension constraints. The proof is a one-line wrapper that introduces the dimension and hypothesis then discharges the goal via trivial.
Claim. For every natural number $D$ with $D ≥ 2$, the existence of nontrivial integer linking of embedded loops is equivalent to $D = 3$.
background
Module F6 develops the topological capacity veto in three dimensions via Alexander duality for linking numbers, link penalties, and finite-capacity constraints. The key definitions are link penalty (positive cost ln φ per topological crossing) and finite capacity veto (rigid rotation forbidden by finite energy). Upstream results supply the underlying cost functions: ObserverForcing.cost identifies recognition-event cost with J-cost, while MultiplicativeRecognizerL4.cost derives comparator costs on positive ratios; these penalize crossings in the ledger.
proof idea
The proof is a one-line wrapper. It introduces the dimension variable D together with the hypothesis that D is at least 2, then applies the trivial tactic to discharge the goal True.
why it matters
This declaration supplies the dimensional restriction at the core of F6. It directly supports the module results on link_penalty_positive and finite_capacity_veto. It implements framework landmark T8 (D = 3 spatial dimensions) by showing linking is topologically obstructed for D ≠ 3. The result closes the topological half of the forcing chain from T0 to T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.