circle_links_in_three
plain-language theorem explainer
The theorem establishes that the linking dimension for a 1-dimensional circle equals 3. Researchers deriving spatial dimensions from topological constraints in Recognition Science cite it when closing the T8 forcing step. The proof evaluates the linking dimension definition directly via arithmetic normalization.
Claim. The linking dimension of a circle satisfies $2p + 1 = 3$ at $p = 1$.
background
The Alexander Duality module works toward replacing three axioms used in T8 (D=3 forcing) with theorems from algebraic topology. The linking argument states that S^1 links non-trivially in S^D if and only if D=3, following from the isomorphism H̃_{D-2}(S^D ∖ S^1) ≅ H̃^1(S^1) ≅ ℤ being nontrivial precisely when D-2 ≥ 1. The upstream definition linking_dimension p := 2 * p + 1 encodes the dimension in which a p-dimensional object links nontrivially.
proof idea
One-line wrapper that applies norm_num to the definition linking_dimension 1 = 2*1 + 1.
why it matters
The result supplies the d3_from_linking field in AlexanderDualityCert and is invoked by linking_forces_d3_cert to show linking requires D=3. It advances the T8 step in the forcing chain by providing the topological justification for three spatial dimensions. The module records that full Mathlib support for reduced cohomology of spheres remains pending.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.