Foundation Primitive Recognition Calculus Cubical Chain Complex

The cubical ledger

A recognition event, a discrete record of a distinction made by a system, can be arranged into a cube whose axes are channels of distinction. The module under discussion packages the square faces of that cube into a chain complex, a standard algebraic structure in which boundary operators compose to zero. The headline result is local and finite: any finite collection of certified square faces, added together, has zero total boundary-of-boundary. In plain terms, the edges of the faces cancel in pairs, so the algebraic boundary of the whole collection vanishes.

The classical idea of a chain complex goes back to the nineteenth century, when mathematicians sought to count holes in geometric shapes by formalizing boundaries. The defining equation is ∂² = 0: the boundary of a boundary is empty. The module proves this equation for the recognition cube's square faces, both for a single face and for any finite list of faces. The proof is carried out in a machine-checked library of formal theorems, so the cancellation is verified by computation rather than by hand-waving.

In Recognition Science, the framework models the cube as a configuration of distinction channels, and the square faces are the elementary two-dimensional distinctions. The module constructs a two-step chain complex with groups C₂, C₁, C₀ and maps d₂, d₁ satisfying d₁ ∘ d₂ = 0. It then proves the same square-zero law for every ambient two-face in an n-channel cube, and packages this into a certificate structure that supports finite sums. The final theorem states that any finite list of two-face certificates has zero total boundary-of-boundary.

The consequence is that the local algebraic structure of recognition is sound: no finite collection of square faces can produce a spurious boundary. This is the foundation for a future homology theory, which would count the holes in the recognition cube and thereby classify its global structure. The module explicitly leaves that full all-dimensions homology API as an open target; what it establishes is the local ∂² = 0 law, stable under finite addition.

/-- The explicit Delta square as a two-step chain complex. -/
def squareBoundaryPair : BoundaryPair ℤ MultiDistinctionGeometry.C1 MultiDistinctionGeometry.C0 where
  d₂ := MultiDistinctionGeometry.d2
  d₁ := MultiDistinctionGeometry.d1
  square_zero := by
    intro c
    exact MultiDistinctionGeometry.boundary_squared_zero 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 module does not provide a full homology API for all dimensions. The module does not prove any global topological classification of recognition cubes. The module does not derive physical constants or empirical predictions.

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: