D4_no_linking
plain-language theorem explainer
Four-dimensional space does not admit non-trivial linking of closed curves. Researchers modeling topological conservation in ledger structures cite this to exclude D=4 from the allowed dimensions. The proof is a one-line contradiction obtained by feeding the assumption into the general linking-requires-D=3 theorem and discharging the resulting numerical absurdity.
Claim. There do not exist embeddings of two disjoint circles into the four-sphere with non-zero linking number: no pair of disjoint $S^1$ embeddings in $S^4$ has non-trivial linking number.
background
The DimensionForcing module establishes that only three-dimensional space permits stable topological conservation. SupportsNontrivialLinking D holds precisely when the D-sphere admits disjoint circle embeddings whose linking number is non-zero, which Alexander duality shows occurs if and only if D=3. The upstream theorem linking_requires_D3 states that SupportsNontrivialLinking D implies D=3 and is proved via Alexander duality without reference to the eight-tick period or gap-45 synchronization.
proof idea
The proof is a one-line term wrapper. Assume SupportsNontrivialLinking 4. Apply linking_requires_D3 4 to obtain the equality 4=3. This contradicts the numerical fact 4≠3, which is discharged by norm_num.
why it matters
This theorem completes the topological veto on D≥4 inside the DimensionForcing module, reinforcing that only D=3 supports non-trivial linking required for ledger conservation. It aligns with the T8 step that forces three spatial dimensions and closes one of the four independent arguments listed in the module documentation. The result is independent of the phi-ladder and cost functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.