Foundation Linking Vanishing Low Dim Linking Complement H1

Linking in low dimensions

Linking is a classical topological idea: two circles in three-dimensional space can be interlocked, like the rings of a chain, so that neither can be pulled apart without breaking one. The framework's machine-checked library of formal theorems formalizes a detector for this idea. The detector takes a dimension D, looks at an embedded circle inside the D-dimensional sphere, removes the circle, and asks whether the leftover space has a nonzero first homology group. Nonzero first homology means the complement has a hole that the embedded circle created, a sign of nontrivial linking.

In dimension 3, this detector can succeed: an embedded circle can leave a complement with a hole. The declaration linkingComplementH1, a formal definition in the framework's library, names the object that computes that complement's first homology. The two theorems proved about it are negative results. In dimension 0, the 0-sphere is just a two-point space, so every subspace is totally disconnected, and its first homology vanishes. In dimension 1, a continuous injection of the circle into itself must be surjective, so the embedded circle fills the whole 1-sphere, its complement is empty, and again the first homology vanishes. The detector therefore fails in both low dimensions.

These are theorems in the framework's machine-checked library, meaning the proofs are verified by a computer and rest on no framework-specific axioms. The result is a boundary condition, not a positive achievement: it says where linking cannot be detected, not where it can. The framework's larger goal of forcing three spatial dimensions from recognition principles uses linking as part of its chain, and this low-dimensional vanishing is a necessary check that the detector behaves correctly in the small cases.

What the declaration does not claim is just as important. It does not claim that linking is impossible in dimensions 0 or 1; circles can still be linked in a sense, but the specific homological detector cannot see it. It does not claim anything about dimension 2 or higher. And it does not claim that the physical universe's three-dimensionality follows from this lemma alone; the full forcing chain, including the physical bridge from recognition to linking, remains open.

/-- No embedded circle in the 0-sphere has homologically nontrivial
complement: every subspace of the two-point space `S⁰` is totally
disconnected, so its first singular homology vanishes. -/
theorem not_detects_zero : ¬ DetectsNontrivialLinking 0 := by
  rintro ⟨f, -, hH⟩
  apply hH
  haveI hTD : TotallyDisconnectedSpace ↥(TopCat.sphere.{0} 0) := by
    show TotallyDisconnectedSpace
      (ULift.{0} ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 1)) 1))
    infer_instance
  haveI : TotallyDisconnectedSpace
      ↥(TopCat.of {x : TopCat.sphere.{0} 0 // x ∉ Set.range f}) :=
    (inferInstance :
      TotallyDisconnectedSpace {x : TopCat.sphere.{0} 0 // x ∉ Set.range f})
  exact AlgebraicTopology.isZero_singularHomologyFunctor_of_totallyDisconnectedSpace
    (ModuleCat ℤ) 1 (ModuleCat.of ℤ ℤ)
    (TopCat.of {x : TopCat.sphere.{0} 0 // x ∉ Set.range f}) one_ne_zero

/-- No embedded circle in the 1-sphere has homologically nontrivial
complement: the embedding is surjective, so the complement is empty, and
singular homology of the empty space vanishes in degree `1`. -/
theorem not_detects_one : ¬ DetectsNontrivialLinking 1 := by
  rintro ⟨f, hemb, hH⟩
  apply hH
  -- the underlying self-map of the metric circle
  set f₀ : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) →
      ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) :=
    fun x =>
      (show ULift.{0} ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) from
        f (show ↥(TopCat.sphere.{0} 1) from ULift.up x)).down with hf₀
  have hc : Continuous f₀ := by
    exact continuous_uliftDown.comp (f.continuous.comp continuous_uliftUp)
  have hinj : Function.Injective f₀ := by
    intro x y h
    have h2 : f (ULift.up x) = f (ULift.up y) := ULift.down_injective h
    have h3 := hemb.injective h2
    exact congrArg ULift.down h3
  have hsurj := continuous_injective_circle_self_surjective f₀ hc hinj
  haveI hE : IsEmpty {x : TopCat.sphere.{0} 1 // x ∉ Set.range f} := by
    constructor
    rintro ⟨x, hx⟩
    obtain ⟨y, hy⟩ := hsurj
      (show ULift.{0} ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) from x).down
    exact hx ⟨ULift.up y, ULift.down_injective hy⟩
  haveI hTD : TotallyDisconnectedSpace {x : TopCat.sphere.{0} 1 // x ∉ Set.range f} := by
    constructor
    intro t _ _ x hx
    exact (hE.false x).elim
  haveI : TotallyDisconnectedSpace
      ↥(TopCat.of {x : TopCat.sphere.{0} 1 // x ∉ Set.range f}) := hTD
  exact AlgebraicTopology.isZero_singularHomologyFunctor_of_totallyDisconnectedSpace
    (ModuleCat ℤ) 1 (ModuleCat.of ℤ ℤ)
    (TopCat.of {x : TopCat.sphere.{0} 1 // x ∉ Set.range f}) one_ne_zero

/-- Verbatim restatement of `PublicSpine.linkingComplementH1`. -/
noncomputable def linkingComplementH1 (D : ℕ)
    (f : C(TopCat.sphere.{0} 1, TopCat.sphere.{0} D)) : ModuleCat ℤ :=
  ((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) 1).obj
    (ModuleCat.of ℤ ℤ)).obj
    (TopCat.of {x : TopCat.sphere.{0} D // x ∉ Set.range f})

What this page does not claim

No claim that linking is impossible in dimensions 0 or 1, only that this particular homological detector cannot see it. No claim about dimensions 2 or higher. No claim that three-dimensionality follows from this lemma alone; the physical recognition-to-linking bridge is open.

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