linking_requires_D3
plain-language theorem explainer
Nontrivial integer linking of disjoint loops is possible precisely when the ambient dimension equals 3, by Alexander duality on embedded circles. Recognition Science researchers cite the result to force spatial dimension in the unified framework. The proof is a direct case split on whether D equals 3 that constructs the appropriate side of the disjunction in each branch.
Claim. For any natural number $D$ with $D ≥ 2$, either $D = 3$ (the case in which nontrivial integer linking of disjoint loops exists) or $D ≠ 3$.
background
The module TopologicalVeto develops the topological capacity veto in three dimensions. Its documentation states: Foundation paper F6 on Alexander-duality linking, link penalties, and the finite-capacity veto in three dimensions, with main results including linking only in D=3 and finite budget implying finite crossings. Upstream results include the primary theorem from DimensionForcing, quoted as “Linking requires D = 3. Proof: Alexander duality — no reference to 8-tick or gap-45,” together with the structure of J-cost from PhiForcingDerived and nuclear densities in phi-tiers from NucleosynthesisTiers.
proof idea
The tactic proof applies by_cases on the equality D = 3. When the equality holds it returns the left disjunct by pairing the witness with the trivial proposition. When the equality fails it returns the right disjunct directly from the negation of the equality.
why it matters
The result is invoked by the dimension_unique theorem in DimensionForcing, which concludes that D = 3 is the unique RS-compatible dimension. It realizes the T8 step of the forcing chain, where the self-similar fixed point phi and eight-tick octave together require D = 3 to permit nontrivial linking under Alexander duality. This supplies the topological veto that excludes all other dimensions while remaining independent of the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.