Foundation Linking Vanishing High Dim Is Zero H1 Inter

The vanishing of higher-dimensional linking

A circle drawn in space, and a separate point or loop that you try to link with it, like two rings of a chain. In three dimensions, you can link two circles so that they cannot be separated without cutting one. The mathematical question is whether this kind of linking can happen in other dimensions. The answer, proved in a machine-checked library of formal theorems, is that it cannot: in any dimension other than three, any circle embedded in that space leaves a complement whose first homology group is zero, meaning there is no hole for another loop to catch onto.

The key statement, called isZero_h1_inter, is a theorem that says this vanishing happens for the complement of an embedded circle in a sphere of dimension D, as long as D is at least 1 and not equal to 3, and a technical condition about arcs holds. The proof works by showing that the complement of the circle can be built from two pieces, each of which has no first homology, and that their intersection also has none. This is a topological fact, stated in the language of singular homology with integer coefficients. It does not depend on any physical assumption; it is a property of spheres and continuous embeddings.

In Recognition Science, this theorem is the engine behind a larger claim. The framework models physical space as a sphere of some dimension D, and it defines a notion of a circle detecting a nontrivial linking. The theorem forces_D3_of_arcAcyclic then derives that if every arc complement in high dimensions is acyclic, then any dimension that detects nontrivial linking must be exactly 3. In plain terms, the framework proves that the very possibility of linking, which we experience in our world, rules out all dimensions except three. The proof is a chain of formal implications, all checked by the machine, and it relies on the vanishing result as its central step.

What the declaration does not claim is just as important. It does not claim that the physical universe is three-dimensional; that would require an additional bridge from the topological theorem to the physics of recognition, and that bridge remains open. It does not claim that the technical condition about arcs is proved for all dimensions; that condition is an assumption in the main theorem. And it does not claim anything about dimensions 0, 1, or 2, which are handled by separate low-dimensional results. The theorem is a precise statement about homology groups, and its power comes from being exactly that precise.

The consequence is that a purely mathematical fact, the vanishing of a homology group, becomes the fulcrum for a physical conclusion. A reader can now see that the three-dimensionality of space is not an arbitrary input in this framework but a forced output, once the possibility of linking is taken as a given. The proof is not a metaphor or an analogy; it is a sequence of formal steps that a computer has verified. That is what makes the claim strong, and that is also why its limits must be stated with the same precision.

/-- **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

/-- **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

What this page does not claim

The theorem does not claim that physical space is three-dimensional; that requires an additional bridge that remains open. The theorem does not claim that the arc acyclicity condition is proved for all dimensions; it is an assumption in the main result. The theorem does not cover dimensions 0, 1, or 2, which are handled by separate low-dimensional results.

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: