Foundation Arc Complement Acyclic Exists Nonbounding

A nonbounding cycle

A cycle is a closed loop, and a bounding cycle is one that is the boundary of some higher-dimensional region, like the equator is the boundary of the northern hemisphere. The declaration exists_nonbounding proves that if a space has a nonzero first homology group, then there is a cycle that is closed but does not bound anything. In plainer terms: the space has a hole, and the loop that goes around it cannot be filled in.

This is a standard fact in algebraic topology, where homology groups measure holes. The declaration is a machine-checked proof of this fact within the Recognition Science library, a collection of formal theorems. It states that given a topological space W whose first homology group is not zero, there exists a 1-cycle z such that its boundary is zero, and z is not the boundary of any 2-chain. The proof uses the framework's chain complex and boundary operator definitions.

In Recognition Science, this lemma supports the construction of ledger elements, a discrete record of recognition events, by ensuring that certain closed paths are not trivial. It is a technical building block for the framework's treatment of space. The declaration does not claim that any specific space has a nonzero first homology group; it only says that if one does, then a nonbounding cycle exists.

The result is a theorem about the existence of a cycle, not about its uniqueness or its geometric shape. It also does not assert that the cycle is visible or meaningful in any physical sense. It is a purely topological statement, with no claim about the framework's physical constants or the number of spatial dimensions.

/-- A nonvanishing `H₁` yields a nonbounding cycle. -/
lemma exists_nonbounding {W : TopCat.{0}} (hW : ¬ IsZero (Hgrp W 1)) :
    ∃ z : ↥(Cgrp W 1), bnd W 0 z = 0 ∧ ¬ ∃ w, z = bnd W 1 w := by
  have hnz : ∃ h : ↥(Hgrp W 1), h ≠ 0 := by
    by_contra hall
    push_neg at hall
    apply hW
    haveI : Subsingleton ↥(Hgrp W 1) := ⟨fun x y => by rw [hall x, hall y]⟩
    exact ModuleCat.isZero_of_subsingleton _
  obtain ⟨h, hh⟩ := hnz
  obtain ⟨z, hz, hcl⟩ := exists_classOf (SC W) 0 h
  refine ⟨z, hz, fun hb => hh ?_⟩
  rw [← hcl]
  exact (classOf_eq_zero_iff (SC W) 0 z hz).mpr hb

What this page does not claim

The declaration does not prove that any particular space has a nonzero first homology group. It does not claim that the nonbounding cycle is unique or has any geometric properties. It does not assert any physical interpretation of the cycle beyond the topological statement.

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