high_D_no_linking
plain-language theorem explainer
Dimensions four and higher admit no nontrivial linking of closed curves on the sphere, blocking the stable topological conservation required for ledgers in the Recognition Science framework. A physicist or mathematician studying dimensional emergence or topological invariants in unified models would cite this to exclude D ≥ 4. The proof proceeds by contradiction: the linking-requires-D3 lemma forces equality to 3, which norm_num immediately contradicts with the given bound D ≥ 4.
Claim. Let D be a natural number with D ≥ 4. Then the D-sphere does not admit disjoint embeddings of circles with nonzero linking number (i.e., ¬SupportsNontrivialLinking D), where SupportsNontrivialLinking D holds precisely when the reduced cohomology group H̃₁(S^D ∖ S¹) is isomorphic to ℤ.
background
In the DimensionForcing module, Dimension is the natural number representing spatial dimension. SupportsNontrivialLinking D is the proposition that S^D admits disjoint S¹-embeddings with nonzero linking number, determined by Alexander duality as H̃₁(S^D ∖ S¹) ≅ ℤ if and only if D = 3. The module proves that only D = 3 supports stable topological conservation in the ledger: D = 1 is collinear, D = 2 unlinks by the Jordan curve theorem, and D ≥ 4 unlinks by codimension ≥ 2.
proof idea
The proof is by contradiction. Assume SupportsNontrivialLinking D. Apply the upstream lemma linking_requires_D3 (which states SupportsNontrivialLinking D → D = 3 and is proved via Alexander duality) to obtain D = 3. Then norm_num derives a contradiction with the hypothesis D ≥ 4.
why it matters
This theorem completes the linking argument for forcing D = 3 in the module, which is one of the four arguments establishing that spatial dimension must be three. It directly implements the topological veto described in the module doc-comment: only D = 3 supports nontrivial linking for conservation. The result aligns with framework landmark T8 (D = 3 spatial dimensions) and the primary theorem linking_requires_D3; it rules out higher dimensions without invoking the eight-tick or gap-45 synchronization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.