circle_reduced_cohomology_iff
plain-language theorem explainer
The reduced cohomology of the circle is nontrivial exactly in degree 1. Recognition Science researchers and algebraic topologists cite this to ground the Alexander duality argument that fixes spatial dimension at three. The proof is a one-line reflexivity once the predicate is defined directly as equality to one.
Claim. $H̃^k(S¹; ℤ)$ is nontrivial if and only if $k = 1$.
background
The module replaces a prior definitional tautology for circle linking with a cohomology-based argument drawn from Hatcher. Alexander duality states that for a circle embedded in the D-sphere, nontrivial linking is detected by the reduced homology of the complement, which is isomorphic to the reduced cohomology of the circle in degree D-2. The local setting encodes this via the predicate that the circle's reduced cohomology is nontrivial precisely when the degree equals one.
proof idea
One-line term proof that applies Iff.rfl after the sibling definition CircleReducedCohomologyNontrivial k := k = 1.
why it matters
This declaration closes the former axiom for the circle cohomology computation and supplies the key step in alexander_duality_circle_linking, which proves SphereAdmitsCircleLinking D ↔ D = 3. It thereby grounds the T8 forcing of three spatial dimensions inside the Recognition Science chain via the topological linking condition. The parent theorem now rests on a concrete definition rather than an open hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.