Foundation Linking Vanishing High Dim Is Zero H2 Two Point Compl

The vanishing homology

In algebraic topology, the homology group of a space measures its holes. The theorem isZero_h2_twoPointCompl concerns the sphere of dimension n, with two distinct points removed. It states that for any n greater than or equal to 1 and not equal to 3, the second homology group of this punctured sphere is zero. A zero group means the space has no two-dimensional holes; it is, in that algebraic sense, topologically featureless at that level.

The proof is a direct computation. It uses a homeomorphism, a continuous deformation between spaces, to identify the punctured sphere with a punctured Euclidean space. The homology of that space is known to vanish in degree two, and the homeomorphism preserves homology. The conditions on n are essential: the theorem explicitly excludes n = 3, and the case n = 0 is handled separately. For n = 3, the second homology of the two-punctured sphere is not zero, which is the seed of the framework's account of why linking, the entanglement of two loops, is possible in three dimensions but not in others.

In Recognition Science, this theorem is a step in a larger argument. The framework's library of machine-checked theorems uses it to show that, under a hypothesis about arcs, a sphere in dimension D can detect nontrivial linking only when D = 3. The vanishing of this homology group for all other dimensions is what rules them out. The theorem itself, however, is a statement about a specific topological space; it does not, by itself, assert anything about physical space. The step from this algebraic fact to a claim about the dimensionality of the universe requires additional premises about what physical space is and how linking is detected, and those premises are not part of this theorem.

The theorem also does not claim that the two-punctured sphere has no holes at all. It only concerns the second homology group. The first homology group, which measures one-dimensional holes, is not addressed by this statement. A reader should not conclude that the space is contractible, only that a particular algebraic invariant vanishes.

/-- `H₂(Sⁿ \ {p, q}) = 0` for `n ≥ 1`, `n ≠ 3`, and any distinct points. -/
theorem isZero_h2_twoPointCompl {n : ℕ} (hn : 1 ≤ n) (hn3 : n ≠ 3)
    (p q : ↥(Sph n)) (hqp : q ≠ p) :
    IsZero (Hgrp (TopCat.of ↥(({p, q} : Set ↥(Sph n))ᶜ)) 2) := by
  obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (by omega : n ≠ 0)
  exact (sphere_homology_vanish m 2 one_le_two (by omega)).of_iso
    (hgrpIso (twoPointComplHEquiv m p q hqp) 2)

What this page does not claim

The theorem does not assert anything about physical space or the dimensionality of the universe. The theorem does not claim the two-punctured sphere has no holes at all, only that its second homology group is zero. The theorem does not address the case n = 3, where the second homology is non-zero.

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/LinkingVanishingHighDim.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: