linking_dimension
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Hyperspherical flows close gap to diffusion in language reasoning
"The geodesic distance between p,q ∈ S^{d-1} is the angle dS(p,q) = arccos(p⊤q)... exponential map expp(v) = cos(∥v∥)p + sin(∥v∥) v/∥v∥"