Encyclopedia Foundation Foundation Linking Vanishing Low Dim Sphere Fin One Finite

ARTICLE 3 claims 3 theorems

Foundation Linking Vanishing Low Dim Sphere Fin One Finite

A machine-checked proof that the 0-sphere has only two points, which helps show why the framework's linking detector stays silent in the lowest dimensions.

Verify this page

Two points, no loops

The 0-sphere is the set of points at distance exactly 1 from the origin in a one-dimensional space. That set contains just two points: the number 1 and the number -1. The declaration sphere_fin_one_finite is a machine-checked proof of this fact, recorded in the framework's library of formal theorems. It states that this two-point set is finite, which is a basic but load-bearing step for what follows.

Why does finiteness matter here? The Recognition Science framework uses a ledger, a discrete record of events, to detect structure. In this part of the framework, a detector asks whether an embedded circle leaves a hole behind in a sphere of a given dimension. The detector works by looking at the first homology group of the complement: the part of the sphere left over after the circle is removed. A nonzero homology group means a hole exists. The two-point 0-sphere has no room for such a hole, because every subspace of a two-point space is totally disconnected, and the first homology of a totally disconnected space vanishes.

The proof of finiteness is the first link in a short chain. The chain continues with a theorem that the detector fails in dimension 0, and another that it fails in dimension 1. In dimension 1, the circle is the whole sphere, so an embedded circle leaves nothing behind, and the homology of the empty space is zero. These results are proved in the machine-checked library, with no gaps.

What the declaration does not claim is just as important. It does not say anything about dimensions 2 or higher, where linking can occur. It does not claim that the framework's linking detector is useless; it only establishes that the detector is silent in the two lowest dimensions. It also does not claim that the two-point set has any special structure beyond being finite. The declaration is a narrow, precise fact, and the framework uses it as one small brick in a larger wall.

THEOREM sphere_fin_one_finite · IndisputableMonolith/Foundation/LinkingVanishingLowDim.lean
sphere_fin_one_finite · IndisputableMonolith/Foundation/LinkingVanishingLowDim.lean:49 
/-- The unit sphere in `ℝ¹` is contained in the two-point set `{e, -e}`. -/
lemma sphere_fin_one_finite :
    (Metric.sphere (0 : EuclideanSpace ℝ (Fin 1)) 1).Finite := by
  have hsub : Metric.sphere (0 : EuclideanSpace ℝ (Fin 1)) 1 ⊆
      {EuclideanSpace.single (0 : Fin 1) (1 : ℝ),
        EuclideanSpace.single (0 : Fin 1) (-1 : ℝ)} := by
    intro x hx
    rw [EuclideanSpace.sphere_zero_eq _ zero_le_one, Set.mem_setOf_eq,
      Fin.sum_univ_one] at hx
    have h0 : (x 0 - 1) * (x 0 + 1) = 0 := by nlinarith
    rcases mul_eq_zero.mp h0 with h | h
    · left
      ext i
      obtain rfl : i = (0 : Fin 1) := Subsingleton.elim _ _
      rw [EuclideanSpace.single_apply, if_pos rfl]
      linarith
    · right
      ext i
      obtain rfl : i = (0 : Fin 1) := Subsingleton.elim _ _
      rw [EuclideanSpace.single_apply, if_pos rfl]
      linarith
  exact ((Set.finite_singleton _).insert _).subset hsub
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

What this page does not claim

The declaration says nothing about dimensions 2 or higher, where linking can occur. The declaration does not claim that the linking detector is useless; it only shows it is silent in dimensions 0 and 1. The declaration does not attribute any special structure to the two-point set beyond finiteness.

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