Encyclopedia Foundation Foundation Linking Vanishing Low Dim

ARTICLE 3 claims 3 theorems

Foundation Linking Vanishing Low Dim

A machine-checked proof shows that the mathematical object used to detect linking in higher dimensions simply cannot exist in dimensions zero or one.

Verify this page

Why the circle needs room

In topology, a circle is the set of points at a fixed distance from a center in a plane. The question of whether one circle can be linked with another only makes sense when there is space for the second circle to pass around the first. The module LinkingVanishingLowDim in the Recognition Science framework's machine-checked library of formal theorems proves a precise version of this intuition: the standard algebraic tool for detecting nontrivial linking fails in dimensions 0 and 1.

The framework's ledger, a discrete record of events, uses a specific mathematical construction to detect when one sphere is linked with another. This detector, called DetectsNontrivialLinking, examines the space left over after embedding one sphere into another. In dimension 2, an embedded circle inside a 2-sphere leaves behind a region with a hole, and the algebraic signature of that hole is what the detector finds. The module proves this detector cannot work in the two lowest dimensions.

For dimension 0, the 0-sphere is just a two-point space, like the two ends of a line segment. Every subspace of this space is totally disconnected, meaning it falls apart into isolated points. The theorem not_detects_zero proves that the first homology, the algebraic measure of holes, of any such subspace is zero. There is no hole to find because there is no connected loop to enclose one.

For dimension 1, the argument is more subtle. The theorem continuous_injective_circle_self_surjective proves that a continuous, one-to-one map from a circle into itself must cover the entire circle. If it missed a single point, the circle could be stretched out into a line, which is impossible because the circle is connected and a line with a gap is not. Therefore, an embedded circle in a 1-sphere leaves behind nothing at all, and the homology of an empty space is zero. The theorem not_detects_one records this failure.

These results are not a defect in the framework. They are a boundary condition. The detector is a tool that works only when the ambient space has enough room for a loop to enclose a hole. The proofs establish that the framework's linking concept is meaningful starting in dimension 2, which is the dimension where the ordinary physical notion of one loop catching another first becomes possible.

THEOREM not_detects_zero · IndisputableMonolith/Foundation/LinkingVanishingLowDim.lean
not_detects_zero · IndisputableMonolith/Foundation/LinkingVanishingLowDim.lean:75 
/-- 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
THEOREM not_detects_one · IndisputableMonolith/Foundation/LinkingVanishingLowDim.lean
not_detects_one · IndisputableMonolith/Foundation/LinkingVanishingLowDim.lean:211 
/-- 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
THEOREM continuous_injective_circle_self_surjective · IndisputableMonolith/Foundation/LinkingVanishingLowDim.lean
continuous_injective_circle_self_surjective · IndisputableMonolith/Foundation/LinkingVanishingLowDim.lean:178 
/-- A continuous injection of the metric circle into itself is surjective:
if it missed a point, composing with the stereographic projection from that
point would give a continuous injection of the circle into `ℝ¹`. -/
theorem continuous_injective_circle_self_surjective
    (f₀ : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) →
      ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1))
    (hc : Continuous f₀) (hinj : Function.Injective f₀) :
    Function.Surjective f₀ := by
  intro p
  by_contra hp
  push_neg at hp
  haveI fact2 : Fact (Module.finrank ℝ (EuclideanSpace ℝ (Fin 2)) = 1 + 1) :=
    ⟨by norm_num [finrank_euclideanSpace_fin]⟩
  set φ := stereographic' (1 : ℕ) p with hφ
  have hmem : ∀ x, f₀ x ∈ φ.source := by
    intro x
    rw [hφ, stereographic'_source]
    exact Set.mem_compl_singleton_iff.mpr (hp x)
  have hφc : Continuous fun x => φ (f₀ x) :=
    φ.continuousOn.comp_continuous hc hmem
  set g : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) → ℝ :=
    fun x => (φ (f₀ x)) 0 with hg
  have hgc : Continuous g :=
    (EuclideanSpace.proj (0 : Fin 1)).continuous.comp hφc
  have hginj : Function.Injective g := by
    intro x y hxy
    apply hinj
    apply φ.injOn (hmem x) (hmem y)
    ext i
    obtain rfl : i = (0 : Fin 1) := Subsingleton.elim _ _
    exact hxy
  exact (no_continuous_injective_circle_to_real g hgc hginj).elim

What this page does not claim

This module proves that linking is impossible in all low dimensions, only that this specific detector fails. This module establishes the physical claim that space has three dimensions.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND