Foundation Singular Sphere Geometry Sphere Top Ne Zero

The sphere's first homology

The circle is the set of points at distance 1 from a center in a plane. Its first homology group, a way to count holes by algebra, is the integers: the circle has exactly one hole. The declaration h1_s1_ne_zero proves this group is not zero, meaning the hole is real and cannot be contracted to a point. This is a standard result in algebraic topology, and the framework's library proves it with a machine-checked formal proof.

The proof builds the circle as a topological space, names two special points (north and south poles), and covers the circle with two open sets that exclude each pole. The intersection of these sets is a pair of disconnected arcs. The key step shows that a certain difference of two points in this intersection, called a difference class (a formal way to record a path between two points), is not zero in the homology group. This nonzero class is the hole.

In Recognition Science, this fact is not idle geometry. The framework models recognition (a discrete event of matching one thing to another) as a process on a circle. The nonzero hole provides a topological obstruction: a loop around the circle cannot be shrunk to a point, so the recognition cycle has a genuine, non-trivial structure. This is a necessary step in the framework's chain that derives the number 8 for a recognition cycle and, from that, the three dimensions of space.

The declaration does not claim that the circle is the only space with a nonzero first homology group, nor does it claim that the hole is unique. It also does not claim that this topological fact alone forces the framework's physical constants; it is one link in a longer chain. The proof is internal to the framework's library and does not depend on any physical measurement.

/-- **`H₁(S¹) ≠ 0`.** If it vanished, the Mayer-Vietoris connecting map
out of it would be zero, and exactness would kill the point-difference
class, contradicting its nonzero pairing. -/
theorem h1_s1_ne_zero : ¬ IsZero (Hgrp (Sph 1) 1) := by
  intro hZ
  have hδ : mvδ (isOpen_coverU 1) (isOpen_coverV 1)
      (coverU_union_coverV 1) 0 = 0 :=
    hZ.eq_of_src _ _
  have hex := mv_exact₁ (isOpen_coverU 1) (isOpen_coverV 1)
    (coverU_union_coverV 1) 0
  rw [ShortComplex.moduleCat_exact_iff] at hex
  have hker : mvPair (coverU 1) (coverV 1) 0 (diffClass (1 : ℤ)) = 0 := by
    rw [← ModuleCat.comp_apply, diffClass_mvPair, zeroApp]
  obtain ⟨w, hw⟩ := hex (diffClass (1 : ℤ)) hker
  have hw' : mvδ (isOpen_coverU 1) (isOpen_coverV 1)
      (coverU_union_coverV 1) 0 w = diffClass (1 : ℤ) := hw
  rw [hδ, zeroApp] at hw'
  have h1 : augH Wc arcA isClopen_arcA (diffClass (1 : ℤ)) = (1 : ℤ) := by
    rw [← ModuleCat.comp_apply, diffClass_pairing, ModuleCat.id_apply]
  rw [← hw', map_zero] at h1
  exact one_ne_zero h1.symm

lemma isOpen_coverU (n : ℕ) : IsOpen (coverU n) := isOpen_compl_singleton

lemma isOpen_coverV (n : ℕ) : IsOpen (coverV n) := isOpen_compl_singleton

/-- The point-difference class in `H₀` of the two-arc intersection. -/
noncomputable def diffClass : ModuleCat.of ℤ ℤ ⟶ Hgrp Wc 0 :=
  ptH Wc aW - ptH Wc bW

/-- The point-difference class dies in `H₀(U) ⊞ H₀(V)` (both points join
inside each punctured circle). -/
lemma diffClass_mvPair :
    diffClass ≫ mvPair (coverU 1) (coverV 1) 0 = 0 := by
  have hjU : ptH (TopCat.of (coverU 1))
      ((mvInclU (coverU 1) (coverV 1)).hom aW) =
      ptH (TopCat.of (coverU 1))
        ((mvInclU (coverU 1) (coverV 1)).hom bW) :=
    ptH_eq_of_joined (PathConnectedSpace.joined _ _)
  have hjV : ptH (TopCat.of (coverV 1))
      ((mvInclV (coverU 1) (coverV 1)).hom aW) =
      ptH (TopCat.of (coverV 1))
        ((mvInclV (coverU 1) (coverV 1)).hom bW) :=
    ptH_eq_of_joined (PathConnectedSpace.joined _ _)
  apply biprod.hom_ext
  · rw [assoc, zero_comp, mvPair, biprod.lift_fst, diffClass,
      Preadditive.sub_comp, ptH_natural, ptH_natural, hjU, sub_self]
  · rw [assoc, zero_comp, mvPair, biprod.lift_snd, Preadditive.comp_neg,
      diffClass, Preadditive.sub_comp, ptH_natural, ptH_natural, hjV,
      sub_self, neg_zero]

What this page does not claim

The declaration does not prove the circle's homology group is isomorphic to the integers, only that it is nonzero. The declaration does not claim the circle is the only space with a nonzero first homology group. The declaration does not by itself force the framework's physical constants; it is one step in a longer chain.

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