Foundation Primitive Recognition Calculus Cubical Chain Complex Two Face Cert Bo

The square-zero law

In the Recognition Science framework, a ledger (a discrete record of events) is built from cubical cells. The declaration twoFaceCert_boundary_squared_zero proves a local law: for any certified two-face, applying the boundary operator twice yields the zero function. This is the cubical analogue of the classical statement that the boundary of a boundary is empty, a property that holds for every finite list of such certified faces.

The framework's machine-checked library of formal theorems establishes this result for a specific structure: a two-step chain complex over types C₂, C₁, C₀, where the boundary maps d₂ and d₁ satisfy d₁(d₂ c) = 0 for every c. The declaration packages this for a finite two-face certificate, which consists of a base configuration, two indices i and j, and an integer coefficient. The theorem states that the boundary-of-boundary chain carried by any such certificate is identically zero.

This local square-zero law is stable under finite collections. The stronger result, proved in the same library, states that any finite list of two-face certificates has zero total boundary-of-boundary. This is the additive finite-certificate version of the local law, and it holds without introducing a full homology API.

What the declaration does not claim is more extensive. It does not establish a full all-dimensions homology theory, which remains an open target. It does not assert that the boundary operator is a differential in a global chain complex beyond the two-step case. It does not claim that every configuration is a boundary of some higher-dimensional cell, only that the boundary of a boundary vanishes.

/-- Every finite 2-face certificate has zero boundary-of-boundary. -/
theorem twoFaceCert_boundary_squared_zero {n : ℕ} (F : TwoFaceCert n) :
    F.boundaryBoundary = fun _ => 0 :=
  ambient_two_face_square_zero F.base F.i F.j F.coeff

/-- **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 a full all-dimensions homology theory. It does not assert that every configuration is a boundary of some higher-dimensional cell. It does not claim that the boundary operator is a differential in a global chain complex beyond the two-step case.

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: