Foundation Singular Sphere Is Iso Aug H Of Path Connected

The path-connected bridge

In algebraic topology, the zeroth homology group of a space records how many connected pieces it has. For a space that is path-connected, meaning any two points can be joined by a continuous path, there is exactly one piece. The theorem isIso_augH_of_pathConnected in the framework's machine-checked library of formal theorems proves that the natural map from this homology group to the integers is an isomorphism: the group is exactly the integers, no more and no less.

The map in question, called the augmentation, sends each zero-dimensional simplex to 1 if its point lies in the whole space, and to 0 otherwise. The theorem states that this map, after passing to homology, is an isomorphism whenever the space is path-connected. This is a standard result in algebraic topology, but here it is formalized and verified in a proof assistant, meaning every step of the argument is checked by the machine.

The proof relies on a key lemma: in a path-connected space, any zero-dimensional cycle can be filled by a one-dimensional simplex. This is the heart of the argument, and it is where the path-connected condition is used. The theorem also depends on the fact that the boundary of any one-dimensional simplex has its two endpoints in the same connected component, which is true when the space is path-connected.

In Recognition Science, this theorem is a foundational bridge. It shows that the zeroth homology of a path-connected space is always the integers, which is a building block for later constructions. The framework uses this to define the notion of a point and to set up the machinery for its cost function and forcing chain. The theorem is a small but essential piece of the logical scaffolding.

What the theorem does not claim is equally important. It does not say anything about higher homology groups, which can be complicated and are not necessarily the integers. It does not apply to spaces that are not path-connected, where the zeroth homology can be a direct sum of integers, one for each component. And it does not make any physical claims about recognition or cost; it is a purely topological statement about the relationship between path-connectedness and homology.

/-- The homology augmentation `H₀(X) ⟶ ℤ` of a path-connected space is an
isomorphism. -/
theorem isIso_augH_of_pathConnected (X : TopCat.{0}) [PathConnectedSpace X] :
    IsIso (augH X Set.univ isClopen_univ) := by
  haveI := isIso_homologyMap_augTo X
  unfold augH
  infer_instance

/-- In a path-connected space, every `0`-chain is homologous to its total
augmentation times a base point. -/
lemma exists_bnd_of_pathConnected {X : TopCat.{0}} [PathConnectedSpace X]
    (x₀ : X) (z : ↥(Cgrp X 0)) :
    ∃ v : ↥(Cgrp X 1),
      bnd X 0 v =
        z - gen X 0 (constSimplex X x₀) (augFun X Set.univ z) := by
  induction z using freeInduction with
  | unit s =>
      obtain ⟨w, hw⟩ := exists_bnd_eq_sub
        (PathConnectedSpace.joined x₀ (pointOf s))
      refine ⟨w, ?_⟩
      rw [hw, constSimplex_pointOf]
      rw [show (unitOf s : ↥(Cgrp X 0)) = genUnit X 0 s from rfl,
        augFun_genUnit, if_pos (Set.mem_univ _), ← genUnit_eq]
  | zero =>
      refine ⟨0, ?_⟩
      rw [map_zero, map_zero, map_zero, sub_zero]
  | add a b ha hb =>
      obtain ⟨va, hva⟩ := ha
      obtain ⟨vb, hvb⟩ := hb
      refine ⟨va + vb, ?_⟩
      rw [map_add, hva, hvb, map_add, map_add]
      abel
  | smulz c a ha =>
      obtain ⟨v, hv⟩ := ha
      refine ⟨c • v, ?_⟩
      rw [mapSmul, hv, mapSmul, mapSmul, smul_sub]

What this page does not claim

The theorem does not apply to spaces that are not path-connected. The theorem says nothing about higher homology groups. The theorem makes no physical claims about recognition or cost.

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: