Encyclopedia Foundation Foundation Linking Vanishing High Dim Is Zero H1 Complement Of Embedding

ARTICLE 3 claims 3 theorems

Foundation Linking Vanishing High Dim Is Zero H1 Complement Of Embedding

A machine-checked proof shows that in every dimension except three, a circle embedded in a sphere leaves no trace in the first homology group of the complement.

Verify this page

The vanishing theorem

In topology, the first homology group of a space measures the one-dimensional holes in it. A circle drawn on a sphere in three dimensions divides the sphere into two regions, and the complement is two separate disks, each with no hole. The theorem isZero_h1_complement_of_embedding generalizes this picture: it states that for any dimension D from 1 upward, except D = 3, if you embed a circle into a D-dimensional sphere, the first homology group of the complement is zero. The complement has no one-dimensional hole. The proof is machine-checked in the framework's library of formal theorems.

The theorem's conditions matter. It requires that the embedding is an arc-acyclic complement, meaning that the complement of any embedded arc is also homology-zero in degree one. This condition holds in low dimensions and is assumed for higher ones. The proof then runs through the cases: for D = 0 and D = 1, the sphere is too small to contain a nontrivial circle; for D = 2, the complement of a circle is two disks; for D = 4 and above, the argument uses the arc-acyclic assumption to show the complement's homology vanishes. The excluded case D = 3 is exactly where the circle can link with itself in a nontrivial way, and the theorem does not apply there.

The result feeds into a larger claim: in the Recognition Science framework, the only dimension where a circle can detect nontrivial linking is D = 3. The theorem forces_D3_of_arcAcyclic (a separate machine-checked result) uses this vanishing to show that if a dimension detects nontrivial linking, it must be three. The framework reads this as part of its derivation of three spatial dimensions from the structure of recognition events. The proof of the vanishing theorem itself is a topological fact, independent of any physical interpretation.

What the theorem does not claim is equally precise. It does not say that in three dimensions the complement always has a hole; a circle that does not link with itself leaves a complement with no hole, and the theorem is silent on that case. It does not assert that the arc-acyclic condition holds for all dimensions; that is a separate assumption, not a proved fact. And it does not, by itself, derive three-dimensional space. The derivation requires the additional theorem that links the vanishing result to the detection of linking, and that theorem carries its own conditions.

THEOREM isZero_h1_complement_of_embedding · IndisputableMonolith/Foundation/LinkingVanishingHighDim.lean
isZero_h1_complement_of_embedding · IndisputableMonolith/Foundation/LinkingVanishingHighDim.lean:513 
/-- **The circle-complement reduction** (Hatcher 2B.1, circle case): if arc
complements in `S^D` are `H₁`-acyclic, then for `D ≥ 1`, `D ≠ 3`, every
embedded circle in `S^D` has `H₁`-acyclic complement.  Mayer-Vietoris over
the complements of the two semicircle images inside the complement of the
two endpoint images. -/
theorem isZero_h1_complement_of_embedding (D : ℕ) (hD : 1 ≤ D) (hD3 : D ≠ 3)
    (harc : ArcComplementsAcyclic D)
    (g : C(↥(Sph 1), ↥(Sph D))) (hg : Topology.IsEmbedding g) :
    IsZero (Hgrp (TopCat.of {y : ↥(Sph D) // y ∉ Set.range g}) 1) := by
  haveI : T2Space ↥(Sph D) :=
    inferInstanceAs (T2Space ↥(sphere (0 : Esp D) 1))
  -- the two semicircle images
  have hgP : Topology.IsEmbedding (g.comp arcPlus) := by
    rw [ContinuousMap.coe_comp]
    exact hg.comp isEmbedding_arcPlus
  have hgM : Topology.IsEmbedding (g.comp arcMinus) := by
    rw [ContinuousMap.coe_comp]
    exact hg.comp isEmbedding_arcMinus
  have hKPg : Set.range (g.comp arcPlus) = ⇑g '' Set.range arcPlus := by
    rw [ContinuousMap.coe_comp, Set.range_comp]
  have hKMg : Set.range (g.comp arcMinus) = ⇑g '' Set.range arcMinus := by
    rw [ContinuousMap.coe_comp, Set.range_comp]
  -- the two endpoint images
  have hinter : Set.range (g.comp arcPlus) ∩ Set.range (g.comp arcMinus) =
      ({g eastP, g westP} : Set ↥(Sph D)) := by
    rw [hKPg, hKMg, ← Set.image_inter hg.injective,
      range_arcPlus_inter_arcMinus, Set.image_pair]
  have hcover : Set.range (g.comp arcPlus) ∪ Set.range (g.comp arcMinus) =
      Set.range g := by
    rw [hKPg, hKMg, ← Set.image_union, range_arcPlus_union_arcMinus,
      Set.image_univ]
  -- H₂ of the two-point complement vanishes
  have hgqp : g westP ≠ g eastP := fun h =>
    eastP_ne_westP (hg.injective h).symm
  have hX2 : IsZero (Hgrp (TopCat.of
      ((Set.range (g.comp arcPlus) ∩ Set.range (g.comp arcMinus))ᶜ :
        Set ↥(Sph D))) 2) := by
    rw [hinter]
    exact isZero_h2_twoPointCompl hD hD3 (g eastP) (g westP) hgqp
  -- assemble
  have hbig := isZero_h1_unionCompl
    (Set.range (g.comp arcPlus)) (Set.range (g.comp arcMinus))
    (isCompact_range (g.comp arcPlus).continuous).isClosed
    (isCompact_range (g.comp arcMinus).continuous).isClosed
    hX2 (harc _ hgP) (harc _ hgM)
  rw [hcover] at hbig
  exact hbig
THEOREM forces_D3_of_arcAcyclic · IndisputableMonolith/Foundation/LinkingVanishingHighDim.lean
forces_D3_of_arcAcyclic · IndisputableMonolith/Foundation/LinkingVanishingHighDim.lean:611 
/-- **The bridge's uniqueness half, conditional on the arc frontier**:
granting arc-complement acyclicity in every dimension `D ≥ 2`, `D ≠ 3`,
nontrivial linking forces `D = 3`.  Dimensions `0` and `1` are the banked
unconditional results (`LinkingVanishingLowDim`). -/
theorem forces_D3_of_arcAcyclic
    (harc : ∀ D, 2 ≤ D → D ≠ 3 → ArcComplementsAcyclic D) :
    ∀ D, DetectsNontrivialLinking D → D = 3 := by
  intro D hdet
  by_contra hne
  match D, hne with
  | 0, _ => exact LinkingVanishingLowDim.not_detects_zero hdet
  | 1, _ => exact LinkingVanishingLowDim.not_detects_one hdet
  | (n + 2), hne =>
      exact not_detects_of_arcAcyclic (n + 2) (by omega) hne
        (harc (n + 2) (by omega) hne) hdet
THEOREM isZero_h1_complement_of_embedding · IndisputableMonolith/Foundation/LinkingVanishingHighDim.lean
isZero_h1_complement_of_embedding · IndisputableMonolith/Foundation/LinkingVanishingHighDim.lean:513 
/-- **The circle-complement reduction** (Hatcher 2B.1, circle case): if arc
complements in `S^D` are `H₁`-acyclic, then for `D ≥ 1`, `D ≠ 3`, every
embedded circle in `S^D` has `H₁`-acyclic complement.  Mayer-Vietoris over
the complements of the two semicircle images inside the complement of the
two endpoint images. -/
theorem isZero_h1_complement_of_embedding (D : ℕ) (hD : 1 ≤ D) (hD3 : D ≠ 3)
    (harc : ArcComplementsAcyclic D)
    (g : C(↥(Sph 1), ↥(Sph D))) (hg : Topology.IsEmbedding g) :
    IsZero (Hgrp (TopCat.of {y : ↥(Sph D) // y ∉ Set.range g}) 1) := by
  haveI : T2Space ↥(Sph D) :=
    inferInstanceAs (T2Space ↥(sphere (0 : Esp D) 1))
  -- the two semicircle images
  have hgP : Topology.IsEmbedding (g.comp arcPlus) := by
    rw [ContinuousMap.coe_comp]
    exact hg.comp isEmbedding_arcPlus
  have hgM : Topology.IsEmbedding (g.comp arcMinus) := by
    rw [ContinuousMap.coe_comp]
    exact hg.comp isEmbedding_arcMinus
  have hKPg : Set.range (g.comp arcPlus) = ⇑g '' Set.range arcPlus := by
    rw [ContinuousMap.coe_comp, Set.range_comp]
  have hKMg : Set.range (g.comp arcMinus) = ⇑g '' Set.range arcMinus := by
    rw [ContinuousMap.coe_comp, Set.range_comp]
  -- the two endpoint images
  have hinter : Set.range (g.comp arcPlus) ∩ Set.range (g.comp arcMinus) =
      ({g eastP, g westP} : Set ↥(Sph D)) := by
    rw [hKPg, hKMg, ← Set.image_inter hg.injective,
      range_arcPlus_inter_arcMinus, Set.image_pair]
  have hcover : Set.range (g.comp arcPlus) ∪ Set.range (g.comp arcMinus) =
      Set.range g := by
    rw [hKPg, hKMg, ← Set.image_union, range_arcPlus_union_arcMinus,
      Set.image_univ]
  -- H₂ of the two-point complement vanishes
  have hgqp : g westP ≠ g eastP := fun h =>
    eastP_ne_westP (hg.injective h).symm
  have hX2 : IsZero (Hgrp (TopCat.of
      ((Set.range (g.comp arcPlus) ∩ Set.range (g.comp arcMinus))ᶜ :
        Set ↥(Sph D))) 2) := by
    rw [hinter]
    exact isZero_h2_twoPointCompl hD hD3 (g eastP) (g westP) hgqp
  -- assemble
  have hbig := isZero_h1_unionCompl
    (Set.range (g.comp arcPlus)) (Set.range (g.comp arcMinus))
    (isCompact_range (g.comp arcPlus).continuous).isClosed
    (isCompact_range (g.comp arcMinus).continuous).isClosed
    hX2 (harc _ hgP) (harc _ hgM)
  rw [hcover] at hbig
  exact hbig

What this page does not claim

The theorem does not claim that the complement of a circle in three dimensions always has a hole. The theorem does not assert that the arc-acyclic condition holds for all dimensions. The theorem does not, by itself, derive three-dimensional space.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND