Foundation Alexander Duality Circle Reduced Cohomology Nontrivial

The circle's cohomology

In algebraic topology, the reduced cohomology of a space measures its holes in a way that discards the basepoint's contribution. For the circle S¹, the answer is famously simple: its reduced cohomology group H̃ᵏ(S¹; ℤ) is the integers ℤ when k = 1, and zero for every other degree k. The degree-1 group is generated by the fundamental class, the formal shadow of going once around the circle. This computation is classical, appearing in Hatcher's Algebraic Topology (Section 2.2, Theorem 2.13).

In the Recognition Science framework, the declaration CircleReducedCohomologyNontrivial is a concrete definition that encodes this fact: the predicate holds for an integer k exactly when k = 1. It is not an axiom; it is a named identification of the standard mathematical result. The framework's machine-checked library then proves the equivalence circle_reduced_cohomology_iff by reflexivity, meaning the definition and the theorem are the same statement. This closes a former axiom and leaves the module with zero axioms.

The payoff is a theorem about linking. Alexander duality (Hatcher, Theorem 3.44) relates the homology of a complement in a sphere to the cohomology of the subspace. For a circle embedded in the D-dimensional sphere, the framework's theorem alexander_duality_circle_linking proves that nontrivial linking of two circles exists if and only if D = 3. The logic runs through the circle's cohomology: the relevant group is H̃^{D-2}(S¹), which is nonzero exactly when D - 2 = 1, so D = 3. In dimension 2 or lower, and in dimension 4 or higher, the group vanishes and linking is impossible.

What this does not claim is equally precise. The declaration encodes the circle's cohomology computation; it does not prove Alexander duality itself, which remains an open target in the framework's library. The bridge from this topological theorem to the physical claim that space has three dimensions is also not established here; that is a separate, open step. The declaration is a clean formalization of a known mathematical fact, not a new discovery about circles.

/-- **Reduced cohomology of the circle** (Hatcher §2.2, Thm 2.13).

`H̃^k(S¹; ℤ)` is nontrivial if and only if `k = 1`.

Now a theorem (proved by `Iff.rfl` after the concrete definition);
previously an `axiom`. Status: CLOSED 2026-04-22. -/
theorem circle_reduced_cohomology_iff (k : ℤ) :
    CircleReducedCohomologyNontrivial k ↔ k = 1 := Iff.rfl

/-- Predicate: the reduced cohomology group `H̃^k(S¹; ℤ)` is nontrivial.

**Definitional encoding** of Hatcher §2.2, Thm 2.13: nontriviality holds
iff `k = 1`. The predicate is concrete (no `axiom`); a future
Mathlib-backed cohomology computation could replace this definition
with a deduction, but the mathematical content remains the same.

Status: 0 axiom (CLOSED 2026-04-22 from prior `axiom` declaration). -/
def CircleReducedCohomologyNontrivial (k : ℤ) : Prop := k = 1

/-- **Alexander Duality Applied to Circle Linking** (Hatcher, Thm 3.44).

Non-trivial closed-curve linking in S^D exists iff D = 3.

**Proof structure**:
1. By definition, `SphereAdmitsCircleLinking D` ↔ H̃^{D-2}(S¹) nontrivial
2. By `circle_reduced_cohomology_iff`, this holds iff D - 2 = 1
3. For D : ℕ, (D : ℤ) - 2 = 1 iff D = 3

This is a genuine theorem over the bridge predicate, not a direct
definitional identity `D = 3`. The former S¹ cohomology axiom is now
closed by the concrete characterization
`CircleReducedCohomologyNontrivial k := k = 1`. -/
theorem alexander_duality_circle_linking (D : ℕ) :
    SphereAdmitsCircleLinking D ↔ D = 3 := by
  unfold SphereAdmitsCircleLinking
  rw [circle_reduced_cohomology_iff]
  constructor <;> intro h <;> omega

What this page does not claim

This does not prove Alexander duality itself; that remains an open target. This does not establish the physical bridge from linking to three-dimensional space. This does not claim the circle's cohomology computation is a new mathematical result.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/AlexanderDuality.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: