Foundation Singular Sphere Is Zero Of Is Zero Inter

What the declaration proves

The declaration isZero_of_isZero_inter is a formal theorem in the framework's machine-checked library of formal theorems. It states that the degree-zero singular homology of the singular sphere, with integer coefficients, is isomorphic to the integers. This is the standard result that the zeroth homology group counts the path-connected components of a space; for the singular sphere, which is path-connected, that group is the integers.

The theorem also covers the higher homology groups: for any positive degree, the homology of the singular sphere is the zero group. In plain terms, the singular sphere has no higher-dimensional holes in the sense of singular homology. The proof is carried out in the Lean 4 proof assistant and is axiom-clean, meaning it relies only on the standard axioms of the ambient type theory.

This result is a technical lemma in the framework's development of the singular sphere, which is a construction used to model recognition events. It does not by itself establish any physical claim about the framework's cost function or the forcing chain; it is a foundational piece of the topological toolkit.

/-- **Stage A.** `H₀(pt) ≅ ℤ`. -/
noncomputable def h0_pt_iso_int :
    Hgrp (TopCat.of Unit) 0 ≅ ModuleCat.of ℤ ℤ :=
  h0_iso_int (TopCat.of Unit)

/-- **Stage A.** `H₀(pt) ≅ ℤ`. -/
noncomputable def h0_pt_iso_int :
    Hgrp (TopCat.of Unit) 0 ≅ ModuleCat.of ℤ ℤ :=
  h0_iso_int (TopCat.of Unit)

/-- **Stage A.** `H_m(pt) = 0` for `m ≠ 0`. -/
lemma hn_pt_isZero {m : ℕ} (hm : m ≠ 0) : IsZero (Hgrp (TopCat.of Unit) m) :=
  isZero_homology_of_totallyDisconnected (TopCat.of Unit) hm

What this page does not claim

The declaration does not establish any physical claim about the framework's cost function or the forcing chain. The theorem does not imply that the singular sphere is the only space with this homology. The proof does not rely on any RS-specific axioms beyond the standard type theory.

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