IndisputableMonolith.Foundation.AlexanderDuality
This module encodes the topological input for the linking argument in dimension forcing: the reduced cohomology of the circle is nontrivial precisely in degree 1, together with Alexander duality statements that permit nontrivial circle linking only in three-dimensional spheres. It is cited by the DimensionForcing module to establish D=3 and by the DraftV1 paper mirror. The module consists of concrete definitions and theorems with zero axioms, directly transcribing Hatcher §2.2 Thm 2.13.
claimThe reduced cohomology group satisfies that $H̃^k(S^1;ℤ)$ is nontrivial if and only if $k=1$. Alexander duality implies that a circle links nontrivially inside $S^3$ but admits no such linking inside $S^n$ for $n≠3$.
background
The module supplies predicates and theorems in the Foundation layer that encode standard algebraic topology facts needed for the Recognition Science forcing chain. Its central object is the predicate that the reduced cohomology group of the circle is nontrivial, defined directly as the statement that $H̃^k(S^1;ℤ)≠0$. This is a closed, axiom-free encoding of Hatcher §2.2 Theorem 2.13, which asserts the nontriviality holds exactly when the degree equals one. The module imports Mathlib for the underlying cohomology definitions and introduces sibling declarations covering circle linking on spheres and the dimension-specific consequences of Alexander duality.
proof idea
This is a definition module. The core predicate CircleReducedCohomologyNontrivial is introduced by direct reference to the cohomology group being nonzero. The iff statement circle_reduced_cohomology_iff follows from the standard computation in algebraic topology. The remaining declarations (SphereAdmitsCircleLinking, alexander_duality_circle_linking, D3_admits_circle_linking, circle_linking_forces_D3) are stated as consequences of Alexander duality applied to the circle case, with no further tactic expansion required inside the module.
why it matters in Recognition Science
The module supplies the topological half of the linking argument that feeds IndisputableMonolith.Foundation.DimensionForcing, which proves D=3 is forced by the RS framework. It also mirrors the corresponding statements in Papers.DraftV1 for the paper audit surface. The declarations close the topological input to the T8 step of the unified forcing chain, where spatial dimension is derived from the eight-tick octave and self-similar fixed point.
scope and limits
- Does not compute cohomology groups from first principles inside Mathlib.
- Does not prove Alexander duality in full generality beyond the circle case.
- Does not address linking in non-spherical manifolds or with coefficients other than ℤ.
- Does not connect the cohomology statements to the J-cost function or phi-ladder.