linking_dimension
Defines the linking dimension for a p-dimensional sphere as 2p + 1. Researchers deriving spatial dimensionality from circle linking in Recognition Science cite this relation to encode the ambient dimension for non-trivial links. The definition is a direct arithmetic expression.
claimThe linking dimension of a $p$-dimensional linker is $2p + 1$.
background
The AlexanderDualityProof module works toward replacing the three Alexander duality axioms that support T8 forcing of D = 3 with results from algebraic topology. The linking dimension supplies the explicit formula for the ambient space dimension in which a p-sphere exhibits non-trivial linking with its complement. Module documentation states that S^1 links non-trivially in S^D precisely when D = 3, via the reduced-cohomology isomorphism H̃_{D-2}(S^D ∖ S^1) ≅ H̃^1(S^1) ≅ ℤ.
proof idea
The declaration is a direct definition that sets linking_dimension p to the arithmetic expression 2 * p + 1. No lemmas or tactics are applied.
why it matters in Recognition Science
This definition is used in AlexanderDualityCert to record the fact d3_from_linking and in LinkingForcesD3 to establish that linking is impossible for D ≤ 2 while required in D = 3. It thereby supports the T8 step that selects three spatial dimensions from the requirement of distinguishable 1-dimensional links. The module leaves open the complete replacement of duality axioms once Mathlib supplies reduced sphere cohomology.
scope and limits
- Does not prove non-triviality of circle linking in three dimensions.
- Does not derive D = 3 from the Recognition functional equation.
- Does not compute reduced cohomology groups.
- Does not extend the formula to linkers outside the given arithmetic relation.
Lean usage
example : linking_dimension 1 = 3 := rflformal statement (Lean)
65def linking_dimension (p : ℕ) : ℕ := 2 * p + 1
proof body
Definition body.
66