IndisputableMonolith.Foundation.AlexanderDuality
The AlexanderDuality module encodes the predicate that reduced cohomology of the circle is nontrivial precisely in degree 1. DimensionForcing cites it for the topological linking argument that forces D=3. It is a closed definitional encoding of Hatcher §2.2 Thm 2.13 with zero axioms.
claim\(\tilde{H}^k(S^1; \mathbb{Z})\) is nontrivial if and only if \(k=1\).
background
This module supplies the topological predicates required by the Recognition Science forcing chain. It defines CircleReducedCohomologyNontrivial as the concrete predicate that the reduced cohomology group of the 1-sphere is nontrivial in a given degree. The encoding follows Hatcher §2.2, Thm 2.13 directly: nontriviality holds iff k=1. The module imports Mathlib and remains open to replacement by a computed cohomology result while preserving the same mathematical content.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
The module feeds the linking argument inside IndisputableMonolith.Foundation.DimensionForcing, which establishes that spatial dimension D=3 is forced. It is re-exported under paper-oriented names in IndisputableMonolith.Papers.DraftV1. This supplies the topological basis for T8 in the T0-T8 forcing chain.
scope and limits
- Does not compute cohomology groups via Mathlib tactics.
- Does not treat spheres of dimension other than 1.
- Does not derive Alexander duality from first principles.
- Does not address linking in non-Euclidean ambient spaces.