LinkingForcesD3
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove any cohomology isomorphism from Alexander duality.
- Does not extend to linkers of dimension greater than one.
- Does not derive the linking_dimension formula from more basic principles.
- Does not address the full forcing chain from T0 to T8.
formal statement (Lean)
78structure LinkingForcesD3 where
79 smallest_linker : ℕ := 1 -- S^1 (circle)
proof body
Definition body.
80 linking_requires : linking_dimension 1 = 3
81 no_linking_in_2D : ∀ D, D ≤ 2 → ¬(∃ p, linking_dimension p = D ∧ p ≥ 1)
82 linking_in_3D : linking_dimension 1 = 3
83