linking_dimension_odd
plain-language theorem explainer
The declaration proves that the linking dimension for any natural number p is odd. Researchers deriving spatial dimensionality from topological linking in Recognition Science would cite it to confirm that circle links occur only in odd dimensions. The proof is a direct one-line term that substitutes the explicit formula for linking dimension and checks the arithmetic property.
Claim. For every natural number $p$, the linking dimension $2p+1$ is odd.
background
The Alexander Duality module develops a proof strategy to replace three axioms used in T8 with results from algebraic topology. The central definition states that linking_dimension p equals 2 times p plus 1, parametrizing the sequence of odd positive integers that can serve as linking dimensions. This sits inside the local argument that circles link non-trivially in S^D if and only if D equals 3, via the reduced-cohomology isomorphism H̃_{D-2}(S^D minus S^1) congruent to H̃^1(S^1) congruent to Z.
proof idea
The proof is a term-mode one-liner. It supplies the witness p to the Odd predicate, unfolds the definition linking_dimension p = 2p + 1, and applies the omega tactic to discharge the resulting arithmetic statement.
why it matters
The result supplies a required arithmetic fact for the D=3 forcing argument that appears in the same module under the heading D = 3 Forcing from Linking. It supports the Recognition Science claim that recognition events require distinguishable topological linking and that the simplest non-trivial case (circles) forces exactly three spatial dimensions (T8). No downstream theorems are recorded, leaving the connection to the full Alexander duality replacement open for later development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.