Foundation Singular Sphere Geometry H1 S1 Ne Zero

The circle's first hole

In topology, the circle is the simplest shape with a hole. The hole is not a gap you can see; it is a property of loops. A loop drawn on a circle can wind around it once, twice, or in the other direction, and these winding numbers form the first homology group. For the ordinary circle, that group is the integers. The declaration h1_s1_ne_zero in the framework's machine-checked library of formal theorems states, in formal terms, that this group is not zero: the circle genuinely has a one-dimensional hole.

The proof builds the circle as the set of points at distance one from the origin in a two-dimensional Euclidean space. It then constructs two open sets, each the sphere minus one pole, that cover the circle. Their overlap is a pair of disjoint open arcs. The declaration shows that a particular difference of two points in this overlap, one on each arc, represents a nonzero element in the homology group. This is the standard Mayer-Vietoris argument, formalized in the framework's library.

The theorem is a stepping stone. It is the first nonzero homology group in a sequence that the framework uses to study the topology of spheres. The same library proves that all other homology groups of the circle vanish, and that for higher-dimensional spheres, the only nonzero homology is in the dimension of the sphere itself. These facts are classical, known since the late nineteenth century through the work of Poincaré and others. The framework's contribution is not a new mathematical fact but a formal proof, checked by a computer, that the fact holds within its own axiomatic system.

In Recognition Science, the framework models physical structure as a ledger of recognition events. The homology of spheres is part of the framework's exploration of the geometry that such a ledger might force. The declaration h1_s1_ne_zero is one small, verified piece of that exploration. It does not, by itself, say anything about the physical world. It is a statement about a mathematical object, the circle, and its topological properties.

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

What this page does not claim

The declaration h1_s1_ne_zero does not claim that the physical universe has a one-dimensional hole. It does not claim that the framework's ledger model is physically correct. It does not claim that the circle's homology is a new mathematical discovery.

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: