pith. sign in
module module high

IndisputableMonolith.Foundation.AlexanderDuality

show as:
view Lean formalization →

AlexanderDuality encodes the reduced cohomology nontriviality of the circle and Alexander duality facts for circle linking. It supports the topological forcing of spatial dimension three in the Recognition Science framework. The module supplies these as axiom-free definitions and theorems drawn from standard algebraic topology.

claim$\widetilde{H}^k(S^1;\mathbb{Z})\neq 0 \iff k=1$, together with the statements that $S^3$ admits circle linking, that circle linking forces $D=3$, and that circle linking is impossible in dimensions other than three.

background

The module introduces the predicate for nontrivial reduced cohomology of the circle as a definitional encoding of Hatcher §2.2, Thm 2.13, where nontriviality holds precisely when the degree equals one. It further defines statements on sphere admitting circle linking via Alexander duality and the forcing of dimension three by such linking. This provides the topological substrate for the dimension forcing argument without relying on any axioms.

proof idea

This is a definition module, no proofs. The declarations directly encode the required topological predicates and equivalences.

why it matters in Recognition Science

The module supplies the linking argument for the DimensionForcing module, which establishes that D = 3 is forced within the RS framework. It is also referenced in the DraftV1 paper companion. The content fills the topological component of the eight-tick octave derivation of spatial dimensions.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (8)