IndisputableMonolith.Foundation.AlexanderDuality
Packages Alexander duality for circle linking as the topological engine that forces spatial dimension three. Reduced cohomology of the circle is nontrivial exactly in degree one, selecting D = 3 among spheres that admit a nontrivial circle link. Dimension-forcing, linking witnesses, and T6–T8 audits import the module. Encoding is definitional (Hatcher-style), closed with zero axioms.
claimThe module encodes that $\tilde{H}^k(S^1;\mathbb{Z})$ is nontrivial iff $k=1$, and that $S^D$ admits nontrivial circle linking precisely when $D=3$, via the Alexander duality specialization $H_1(S^D\setminus K)\cong\mathbb{Z}$ for $K\simeq S^1$.
background
Recognition Science forces spatial dimension at T8 of the unified chain. One route is topological: nontrivial loop-loop linking inside the ambient sphere. Alexander duality identifies the homology of a sphere minus an embedded submanifold with the cohomology of that submanifold. For an unknotted circle $K\simeq S^1\subset S^D$, the computation collapses to reduced cohomology of $S^1$.
The module introduces the concrete predicate that $\tilde{H}^k(S^1;\mathbb{Z})$ is nontrivial, definitionally encoding Hatcher §2.2, Thm 2.13 (nontriviality holds iff $k=1$). Companion statements record when a sphere admits circle linking, that $D=3$ does, that linking forces $D=3$, and that low and high dimensions admit none. Status: closed from a prior axiom declaration; zero axioms remain.
proof idea
Definition-and-bridge module rather than a deep computational development. The reduced-cohomology predicate is a Prop encoding of Hatcher's iff criterion at degree one, with an accompanying equivalence lemma. Alexander duality is applied as a selector: sphere admits circle linking reduces to that degree-one fact. The positive case $D=3$ is recorded directly; exclusion lemmas rule out $D<3$ and $D>3$; a uniqueness statement assembles that circle linking forces $D=3$. No Mathlib cohomology computation is invoked yet; the mathematical content matches the classical theorem.
why it matters in Recognition Science
Supplies the topological half of dimension forcing. DimensionForcing lists linking as its first argument toward T8 ($D=3$). DimensionLinking treats this module as the genuine U5 Alexander-duality selector: $H_1(S^D\setminus K)\cong\mathbb{Z}$ iff $D=3$ reduces to cohomology on $S^1$. PublicSpine and T6T8SpineAudit import it for the dual forcing surface and the honesty audit of the T6–T8 spine. Without an axiom-free packaging of circle linking, the topological route to three spatial dimensions would remain scaffolding.
scope and limits
- Does not compute singular cohomology from Mathlib; uses a definitional Hatcher encoding.
- Does not treat higher-dimensional linking or nontrivial knots beyond the unknotted circle.
- Does not derive D = 3 from J-cost, dynamics, or the eight-tick octave alone.
- Does not address Hausdorff, measure, or continuum dimension notions.