LinkingForcesD3
plain-language theorem explainer
LinkingForcesD3 assembles the constraints that force three spatial dimensions via circle linking. Researchers closing the T8 step in the Recognition Science forcing chain would cite this structure when replacing Alexander duality axioms. The definition sets the smallest linker to the circle and requires that linking_dimension equals three only in three dimensions while forbidding it in two or fewer.
Claim. Let $d(p) = 2p + 1$. The structure asserts that the smallest linker is the circle ($p=1$), that $d(1)=3$, that no linking dimension equals any $D$ with $D$ at most 2 for any $p$ at least 1, and that linking occurs in dimension three.
background
The module develops a structural framework to replace the Alexander duality axioms used for forcing three spatial dimensions. Upstream, linking_dimension is defined by $d(p) := 2p + 1$. The mathematical content is that the circle links non-trivially in $S^D$ precisely when $D=3$, following from the isomorphism of reduced cohomology groups that is nontrivial for $D$ at least 3.
proof idea
The structure is defined by directly stating its four fields. The linking_requires and linking_in_3D fields both invoke the upstream linking_dimension definition at argument 1. The no_linking_in_2D field is a universal quantification over dimensions at most two.
why it matters
This definition supplies the type for the certificate theorem linking_forces_d3_cert, which witnesses the structure using circle_links_in_three. It fills the mathematical content for the Alexander duality argument in the module, supporting the replacement of axioms toward T8 where spatial dimension equals three. The structure encodes the key fact that linking is impossible below three dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.