circle_linking_forces_D3
plain-language theorem explainer
Non-trivial linking of circles embedded in the D-sphere forces the dimension to be exactly three. Researchers deriving spatial dimension from topological invariants in Recognition Science cite this when closing the duality-to-dimension step. The proof is a one-line term that extracts the forward implication from the Alexander duality biconditional.
Claim. For a natural number $D$, if the $D$-sphere admits non-trivial linking of disjoint embedded circles (equivalently, if the reduced cohomology group in degree $D-2$ of the circle is nontrivial), then $D=3$.
background
The module replaces a prior definitional identification of dimension with a proof from Alexander duality. SphereAdmitsCircleLinking D is the predicate that the reduced cohomology group in degree $D-2$ of the circle is nontrivial; by the duality isomorphism this detects nontrivial linking numbers for pairs of circles in the complement inside the $D$-sphere. The reduced cohomology of the circle is nontrivial precisely in degree 1, so the predicate holds only for $D-2=1$.
proof idea
The proof is a one-line term wrapper that applies the left-to-right direction of the biconditional alexander_duality_circle_linking to the hypothesis that SphereAdmitsCircleLinking D holds.
why it matters
This supplies the converse direction required by the sibling results that rule out circle linking for all dimensions other than three. It supports the framework derivation of D=3 (T8) as the unique spatial dimension in which the Recognition Composition Law permits nontrivial linking, closing the historical move from definitional tautology to a cohomology-based argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Systems of Wave Equations on Asymptotically de Sitter Vacuum Spacetimes in All Even Spatial Dimensions
"M = (0,τ0) × Sn ... n even and n≥4"