AlexanderDualityForCircle
plain-language theorem explainer
Packages Alexander duality for an embedded circle K in the D-sphere as the cohomology predicate that reduced H^{D-2} of S^1 is nontrivial (equivalently, reduced H_1 of the complement is Z). Anyone citing the U5 linking selector or the T8 spatial-dimension force uses this alias. The body is a one-line abbreviation of the foundation sphere-circle linking predicate.
Claim. For each natural number $D$, the Alexander-duality circle-linking condition on $S^D$ is the proposition that $S^D$ admits nontrivial linking of disjoint embedded circles: equivalently $\tilde{H}_1(S^D \setminus K)\cong\tilde{H}^{D-2}(S^1)$ is nontrivial (which holds precisely when $D=3$).
background
The module formalizes linking nontriviality witnesses for paper items U5 and U10. U5 is the topological specialization of Alexander duality to loop-loop linking ($p=1$): $H_1(S^D\setminus K)\cong\mathbb{Z}$ if and only if $D=3$, reduced to a cohomology computation on $S^1$. The genuine formalization lives in the foundation Alexander-duality module; at the pinned commit the selector encodes $D=3$ via the reduced-cohomology nontriviality predicate on degree $k$ being $k=1$.
Upstream, the sphere-admits-circle-linking predicate states that $S^D$ admits nonzero linking numbers for disjoint embedded circles. By Alexander duality (Hatcher Thm 3.44), that is equivalent to nontriviality of $\tilde{H}_1(S^D\setminus S^1)$, which is isomorphic to $\tilde{H}^{D-2}(S^1)$. Same-sector arithmetic still permits all odd $D\ge 3$; the loop-loop conclusion $D=3$ uses the specialization $p=1$. Spatial dimension $D=3$ is the T8 landmark in the forcing chain.
proof idea
Pure definitional alias: the body is the single application of the foundation predicate that $S^D$ admits nontrivial circle linking, itself defined as reduced-cohomology nontriviality of $S^1$ in degree $D-2$. No tactics, no lemmas beyond that abbreviation.
why it matters
Gives the verification layer a named U5 selector that is no longer the bare equality $D=3$, but the cohomology computation the paper actually invokes. It sits on the T8 step of the forcing chain (spatial dimension three) and on the loop-loop specialization of Alexander duality. Downstream siblings in the same module (linking forces $D=3$, same-sector oddness, explicit witnesses for odd dimensions, allowed-set characterization) are written against this packaging; the used-by list is empty at this pin, so the declaration is infrastructure for those witnesses rather than a cited theorem itself. It closes the audit gap that the selector previously tautologically asserted $D=3$ instead of stating the duality isomorphism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.