Foundation Linking Vanishing High Dim

Why linking forces three dimensions

Imagine tying a loop of string around a circle. In three dimensions, you can link the two so they cannot be separated without cutting. That linking is a real, measurable feature of space. But in higher dimensions, the same trick fails: a circle and a loop can always be pulled apart, no matter how you arrange them. This is a classical fact of topology, and it is the seed of a much larger claim.

The classical statement is about the first homology group of the complement of an embedded circle. In plain terms, it asks whether the space left over after removing a circle has a hole that a loop can catch on. In dimension three, it can. In any other dimension, from two upward, the leftover space has no such hole. The framework's machine-checked library of formal theorems proves this in full generality: for any dimension D that is at least 2 and not 3, and for any embedded circle, the first homology of the complement is zero. The proof handles the low dimensions 0 and 1 separately, then treats every dimension from 2 upward by a uniform argument that reduces the problem to a two-point complement, whose homology vanishes by a standard sphere computation.

In Recognition Science, this topological fact becomes a constraint on the ledger, the framework's discrete record of recognition events. The framework models physical space as arising from a structure that must detect nontrivial linking: it must be able to record the difference between a linked pair and an unlinked pair. The theorem forces_D3_of_arcAcyclic states that if every dimension other than 3 has acyclic arc complements, then any dimension that detects nontrivial linking must be exactly 3. The proof is a direct application of the vanishing result: in any dimension other than 3, the homology of the complement is zero, so no linking can be detected. Only in dimension 3 does the complement retain the hole that makes linking visible.

The consequence is that the framework's own logic, starting from the cost of recognition and the forced composition law, arrives at three spatial dimensions as a theorem, not as an assumption. The chain of results that forces the golden ratio, the eight-tick cycle, and the number 8 also forces this topological condition. The physical bridge from recognition to linking, the step that says the ledger's structure is what space is, remains open. What is proved is the topological half: if the ledger detects linking at all, the dimension must be 3. What is not proved is that the ledger does detect linking, or that this topological structure is the whole story of space.

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

/-- **The high-dimensional (and `D = 2`) vanishing, conditional on the arc
frontier**: granting `ArcComplementsAcyclic D`, no embedded circle in `S^D`
(`D ≥ 1`, `D ≠ 3`) has homologically nontrivial complement. -/
theorem not_detects_of_arcAcyclic (D : ℕ) (hD : 1 ≤ D) (hD3 : D ≠ 3)
    (harc : ArcComplementsAcyclic D) : ¬ DetectsNontrivialLinking D := by
  rintro ⟨f, hemb, hH⟩
  apply hH
  have hz := isZero_h1_complement_of_embedding D hD hD3 harc
    (toSphMap D f) (isEmbedding_toSphMap D f hemb)
  exact hz.of_iso (hgrpIso (complDownHomeo D f).toHomotopyEquiv 1)

What this page does not claim

The framework proves that the ledger actually detects nontrivial linking in dimension three. The framework derives the full physical theory of space from this topological theorem alone. The acyclic arc complement condition is proved from the cost function; it is a hypothesis in this module.

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: