AlexanderDualityApplies
plain-language theorem explainer
Alexander duality applies in dimension D precisely when the paper's (T) setup assumptions for circle linking are met. Researchers formalizing the Recognition Science draft would cite this definition to confirm the topological precondition for the linking selection principle. The definition is a one-line wrapper that delegates to the circle-linking hypothesis, which the upstream theorem equates to D equaling 3 via reduced cohomology.
Claim. Let $P(D)$ be the proposition that the setup assumptions required for Alexander duality in the paper are satisfied for dimension $D$. This holds if and only if the sphere in dimension $D$ admits nontrivial circle linking.
background
This definition sits in the module that mirrors theorem statements from Draft_v1.tex and supplies explicit hypothesis interfaces for external mathematics such as Alexander duality on embedding complements. The local setting treats such interfaces as honest placeholders whose strength equals the strength of the supplied hypotheses. The key upstream result states: Alexander Duality Applied to Circle Linking (Hatcher, Thm 3.44). Non-trivial closed-curve linking in S^D exists iff D = 3. Its proof reduces SphereAdmitsCircleLinking D to the condition that the reduced cohomology group in degree D-2 is nontrivial, which holds exactly when D-2 equals 1.
proof idea
The declaration is a definition that directly equates the proposition to the circle-linking hypothesis. It is a one-line wrapper around that hypothesis. The mathematical content is supplied entirely by the upstream theorem that rewrites the hypothesis as the cohomology condition and solves it by omega to obtain the equivalence with D=3.
why it matters
This definition fills the paper proposition (T) on the linking selection principle and supplies the bridge from linking topology to the framework landmark that spatial dimensions equal 3. It replaces a previously vacuous hypothesis interface with a connection to the proved cohomology equivalence, thereby closing part of the scaffolding that lets the forcing chain reach T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.