AlexanderDualityForCircleHypothesis
plain-language theorem explainer
The declaration supplies a hypothesis interface asserting that the D-sphere admits nontrivial linking of embedded circles for use in the DraftV1 paper. Researchers formalizing the linking selection principle would cite it when invoking Alexander duality for loop invariants. It is realized as a direct one-line delegation to the cohomology predicate SphereAdmitsCircleLinking.
Claim. For a natural number $D$, the $D$-sphere admits nontrivial linking of disjoint embedded circles, witnessed by the reduced cohomology group $H^{D-2}(S^1)$ being nontrivial.
background
The DraftV1 module mirrors theorem statements from Draft_v1.tex and supplies explicit hypothesis interfaces for results that rely on external mathematics such as Alexander duality for complements of embeddings. SphereAdmitsCircleLinking is the upstream predicate asserting that the D-sphere admits non-trivial linking of disjoint embedded circles; by Alexander duality this holds precisely when the reduced cohomology of the circle in degree D-2 is nontrivial, replacing an earlier tautological assumption that D equals 3. The CPM2D Hypothesis structure bundles constants and functionals for a Galerkin-state fluid model but is not invoked in the present delegation.
proof idea
One-line wrapper that applies SphereAdmitsCircleLinking directly to the supplied dimension D.
why it matters
This interface feeds the downstream AlexanderDualityApplies definition, which encodes the (T) setup assumptions required for Alexander duality in the paper and supports the linking selection principle. It connects to the Recognition Science forcing chain at the step that forces D = 3 spatial dimensions from the eight-tick octave and the self-similar fixed point phi. An open question is whether the required cohomology nontriviality can be recovered internally from the Recognition Composition Law without external topological input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.