linking_dimension_odd
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove the Alexander duality isomorphism itself.
- Does not show that linking is possible only in dimension 3.
- Does not treat higher-dimensional knots or links.
- Does not connect to the phi-ladder or mass formulas.
formal statement (Lean)
69theorem linking_dimension_odd (p : ℕ) : Odd (linking_dimension p) := by
proof body
Term-mode proof.
70 use p; unfold linking_dimension; omega
71
72/-! ## D = 3 Forcing from Linking
73
74The physical argument: recognition events require distinguishable
75topological linking (knots/links). The simplest non-trivial link
76is between circles. Circles link non-trivially only in D = 3. -/
77