Foundation Primitive Recognition Calculus Cubical Chain Complex Boundary Pair

The boundary pair

A boundary pair is a small piece of mathematical bookkeeping. It consists of three sets of objects, call them two-dimensional, one-dimensional, and zero-dimensional, together with two maps. The first map takes a two-dimensional object to its one-dimensional boundary. The second takes a one-dimensional object to its zero-dimensional boundary. The rule that makes the pair a boundary pair is that doing both maps in sequence always gives zero: the boundary of a boundary is empty. This is the same rule that makes the edges of a square, taken in the right order, cancel out to nothing.

The idea has a long classical life. In topology, the square-zero boundary rule is what lets mathematicians define homology, a way of counting holes in a shape by looking at which boundaries are not themselves boundaries of something bigger. The rule appears in the work of Henri Poincaré in the 1890s, who introduced it to study the topology of manifolds. It is a local fact: it holds for each individual square or cell, and from it the global counting of holes follows.

In Recognition Science, the framework builds its geometry from a primitive notion of distinction, and the declaration BoundaryPair packages the square-zero rule for that geometry. The framework's library, a machine-checked collection of formal theorems, proves that the specific two-dimensional square it constructs satisfies the rule, and that every two-dimensional face inside an n-dimensional cube of distinctions does too. It also proves the rule survives finite collections: any finite list of certified two-dimensional faces has zero total boundary-of-boundary. These are local statements about the geometry the framework defines.

The declaration does not claim that the full homology theory of the framework's geometry is complete. The library states that the local square-zero law is established, while the stronger target of a full all-dimensions homology API remains open. It also does not claim that the boundary pair itself is a recognition event or a cost; it is a structural fact about the geometry that recognition science uses, not a claim about what recognition costs. The square-zero rule is a foundation stone, not the whole building.

/-- A two-step chain complex over types `C₂`, `C₁`, `C₀`: boundary after boundary
is zero. -/
structure BoundaryPair (C₂ C₁ C₀ : Type*) [Zero C₀] where
  d₂ : C₂ → C₁
  d₁ : C₁ → C₀
  square_zero : ∀ c : C₂, d₁ (d₂ c) = 0

/-- **Cubical chain packaging headline.** Delta's multi-distinction geometry has
a concrete chain-complex interface on the square and square-zero boundary on
every ambient 2-face. The remaining stronger target is the full all-dimensions
homology API, not the local `∂²=0` law. -/
theorem cubical_chain_complex_headline :
    (∀ c : ℤ, squareBoundaryPair.d₁ (squareBoundaryPair.d₂ c) = 0)
      ∧ (∀ (n : ℕ) (base : MultiDistinctionGeometry.Config n) (i j : Fin n) (c : ℤ),
          MultiDistinctionGeometry.faceBoundaryBoundary base i j c = fun _ => 0) :=
  ⟨squareBoundaryPair.square_zero, fun _ base i j c => ambient_two_face_square_zero base i j c⟩

/-- **Finite cubical certificate headline.** The local square-zero law is stable
under finite collections of certified 2-faces: every finite 2-face ledger has
zero total boundary-of-boundary. This is the all-finite-2-face strengthening
available from the current definitions without introducing a full homology API. -/
theorem finite_two_face_ledger_square_zero :
    ∀ (n : ℕ) (faces : List (TwoFaceCert n)),
      (fun w : MultiDistinctionGeometry.Config n =>
        faces.foldl (fun acc F => acc + F.boundaryBoundary w) 0) = fun _ => 0 :=
  fun n faces => twoFaceCert_list_boundary_squared_zero (n := n) faces

What this page does not claim

The declaration does not establish the full homology theory of the framework's geometry, only the local square-zero law. The boundary pair is a structural fact about the geometry, not a claim about the cost of recognition. The square-zero rule for this specific geometry does not by itself imply any global topological property.

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/PrimitiveRecognitionCalculus/CubicalChainComplex.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: