pith. sign in
theorem

alexander_duality_circle_linking

proved
show as:
module
IndisputableMonolith.Foundation.AlexanderDuality
domain
Foundation
line
145 · github
papers citing
6457 papers (below)

plain-language theorem explainer

Nontrivial linking of embedded circles in the D-dimensional sphere holds precisely when D equals three. Recognition Science researchers cite this result to derive the spatial dimension from topological axioms. The proof unfolds the linking predicate to a reduced cohomology condition, rewrites it via the circle cohomology equivalence, and resolves the integer equation with a linear arithmetic tactic.

Claim. For a natural number $D$, the $D$-sphere admits nontrivial linking of disjoint embedded circles if and only if $D = 3$.

background

The module formalizes Alexander duality for circle linking in spheres. The linking predicate is defined via reduced cohomology of the circle in degree $D-2$. The upstream result states that the reduced cohomology of the circle is nontrivial precisely when the degree equals one, citing Hatcher section 2.2 and theorem 2.13. This replaces an earlier tautological definition with a proof from cohomology axioms. The local setting is the topological foundation for forcing $D$ equals 3 in the Recognition Science framework, drawing on Hatcher theorem 3.44 for the duality isomorphism between homology of the complement and cohomology of the subspace.

proof idea

The proof is a short tactic sequence. It unfolds the definition of the linking predicate, rewrites using the circle reduced cohomology equivalence, then applies constructor to split the biconditional and uses intro followed by the omega tactic to solve the resulting arithmetic statements.

why it matters

This theorem is the core of the Alexander duality argument that forces the spatial dimension to be three. It is used by the forward and reverse directions in the same module and feeds into the primary theorems linking_requires_D3 and why_D_equals_3 in the DimensionForcing module. It corresponds to the T8 step in the forcing chain, where $D$ equals 3 is derived from the requirement of nontrivial circle linking via Alexander duality, independent of the eight-tick octave.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 30 of 6457)

The full set is indexed internally; the public theorem page shows a capped sample so high-use declarations do not become many-thousand-row pages.