Foundation Primitive Recognition Calculus Cubical Chain Complex Ambient Two Face

The square-zero boundary law

A standard fact in geometry and topology is that the boundary of a boundary is empty. If you take a square, its boundary is four edges; the boundary of those edges is the set of corners, but each corner is counted twice, once from each adjacent edge, so the result cancels to zero. This chain complex condition, written ∂² = 0, is what makes it possible to define holes, cycles, and homology. The Recognition Science framework, which models recognition as a discrete record of events, encodes its geometry in cubes with multiple channels, and its machine-checked library of formal theorems proves that the same square-zero law holds for every two-dimensional face inside any such cube.

The theorem, named ambient_two_face_square_zero, states that for any configuration of an n-channel cube, any choice of two distinct channels i and j, and any integer coefficient, applying the face boundary twice gives the zero function. In plainer terms: take any 2-face of a higher-dimensional distinction cube, compute its boundary, then compute the boundary of that boundary; the result is identically zero. The proof is not a new argument but a direct appeal to a previously established lemma, face_boundary_squared_zero_general, which already held for the underlying multi-distinction geometry. The library also packages this into a headline theorem, cubical_chain_complex_headline, which combines the square case with the general ambient 2-face case, and it extends the result to finite lists of certified 2-faces, showing that the total boundary-of-boundary of any finite collection is also zero.

What this establishes is a local, structural fact: the Recognition Science cubical geometry is consistent at the level of its two-dimensional faces. It means the boundary operator behaves as a chain complex should, which is the foundation needed before asking deeper questions about holes or higher-dimensional structure. The library's own documentation marks this as a packaging headline: the concrete chain-complex interface on the square and the square-zero boundary on every ambient 2-face are now proved. The remaining target, explicitly noted, is the full all-dimensions homology API, which would compute actual holes and cycles, not just the local ∂² = 0 law. That stronger goal remains open.

What the declaration does not claim is equally important. It does not prove that the full homology theory of the distinction cubes exists; that would require a complete API for all dimensions, which the library states is a target, not an achievement. It does not claim that the boundary of a 2-face is zero, only that the boundary of that boundary is zero. And it does not assert anything about the physical interpretation of these cubes, such as whether they correspond to actual space or time; the theorem is purely about the formal algebraic structure of the framework's geometry. The square-zero law is a necessary condition for homology, not a proof that homology exists.

/-- Any ambient 2-face in an `n`-channel cube has square-zero boundary. -/
theorem ambient_two_face_square_zero {n : ℕ}
    (base : MultiDistinctionGeometry.Config n) (i j : Fin n) (c : ℤ) :
    MultiDistinctionGeometry.faceBoundaryBoundary base i j c = fun _ => 0 :=
  MultiDistinctionGeometry.face_boundary_squared_zero_general base i j c

/-- **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 full all-dimensions homology API for the distinction cubes is proved; it remains a stated target. The boundary of a 2-face itself is zero; only the boundary of that boundary is zero. The square-zero law implies the cubes correspond to physical space or time; it is a purely formal algebraic 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/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: