Foundation Arc Complement Acyclic Chain Map C Val Unit Of

The unit map lemma

In algebraic topology, a chain map is a way of pushing algebraic data forward along a continuous function between spaces. The lemma chainMap_cVal_unitOf concerns a particular kind of map called the complement-value map, written cVal. Given a space W and a subset S of it, cVal sends the complement of S into W by the inclusion map. The lemma states that applying the chain map induced by cVal to a distinguished element, called a unit, yields the unit of the pushed-forward index. In symbols: chainMap(cVal S) n (unitOf s) = unitOf (cPush s).

The practical content is that the unit element, which marks a chosen generator in the chain complex, behaves predictably under this inclusion. If you have a unit at index s in the complement, its image under the chain map is exactly the unit at the corresponding index cPush s in the larger space. This is a coherence statement: the algebraic structure respects the geometric inclusion in the expected way. It is a lemma, not a theorem about the topology of complements; it does not claim that complements are acyclic or that any unit exists in the first place.

The declaration appears in the machine-checked library of formal theorems, in the file ArcComplementAcyclic.lean, alongside a separate theorem arcComplementsAcyclic that states a stronger property for certain high-dimensional spheres. That theorem, for each natural number D, asserts that the complement of an arc in a sphere is acyclic in the relevant sense. The unit-map lemma is a supporting ingredient for such results, but it is not itself the acyclicity theorem. It only pins down how units transform under the inclusion map.

What the lemma does not claim is equally important. It does not assert that the complement of an arbitrary subset is acyclic, nor that the unit element is unique, nor that the chain map is an isomorphism. It merely records a commuting relation. The lemma is a piece of bookkeeping that makes larger proofs work; it is not a statement about the shape of space or about the recognition framework's physical claims. It is a formal fact about how algebraic invariants behave under inclusion, nothing more.

lemma chainMap_cVal_unitOf {S : Set ↥W} {n : ℕ}
    (s : Idx (TopCat.of {y : ↥W // y ∉ S}) n) :
    chainMap (cVal S) n (unitOf s) = unitOf (cPush s) :=
  chainMap_unitOf _ s

What this page does not claim

The lemma does not assert that complements of arbitrary subsets are acyclic. It does not claim that the chain map is an isomorphism or that units are unique. It makes no statement about the physical or geometric content of the Recognition Science framework.

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: