CircleReducedCohomologyNontrivial
plain-language theorem explainer
The predicate that the reduced cohomology group of the circle with integer coefficients is nontrivial in degree k holds exactly when k equals 1. Topologists and Recognition Science researchers formalizing Alexander duality arguments for spatial dimension cite this predicate when characterizing circle linking. The declaration is a direct definitional encoding of the classical Hatcher computation, allowing the related biconditional to reduce to reflexivity.
Claim. The predicate asserting that the reduced cohomology group $H̃^k(S^1; ℤ)$ is nontrivial holds precisely when the degree satisfies $k = 1$.
background
The Alexander Duality module supplies the topological foundation for forcing D = 3 in the Recognition Science framework. It replaces an earlier axiomatic treatment with concrete predicates based on reduced cohomology and Alexander duality (Hatcher, Theorem 3.44). For an embedded circle X = S¹ inside S^D, the duality isomorphism relates the first homology of the complement to the cohomology of the circle: $H̃_1(S^D ∖ S¹; ℤ) ≅ H̃^{D-2}(S¹; ℤ)$. The module documentation states that the reduced cohomology of the circle is nontrivial exactly in degree 1 and vanishes otherwise, which forces the linking group to be nontrivial only for D = 3.
proof idea
The declaration is a one-line definition that directly sets the predicate to the equality k = 1. This encodes the standard algebraic topology result without additional lemmas or tactics at this stage. The sibling theorem then applies Iff.rfl to obtain the biconditional.
why it matters
This definition closes the prior axiomatic gap in the Alexander Duality module and supplies the concrete predicate required by SphereAdmitsCircleLinking. It feeds the theorem circle_reduced_cohomology_iff (proved by Iff.rfl) and thereby supports the full characterization that non-trivial circle linking exists if and only if D = 3. The construction aligns with the eight-tick octave and the forced emergence of three spatial dimensions in the T0–T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.