Foundation Primitive Recognition Calculus Cubical Chain Complex Square Boundary

Square-zero boundary

In algebraic topology, a chain complex is a sequence of abelian groups connected by boundary maps with the property that applying the boundary twice gives zero. The declaration squareBoundaryPair establishes this exact property for the framework's primitive recognition calculus on the square: it constructs a two-step chain complex over the integers and the framework's distinction geometries, with a map d₂ from 2-chains to 1-chains and a map d₁ from 1-chains to 0-chains, such that d₁(d₂(c)) = 0 for every 2-chain c. This is the local ∂²=0 law, the foundational consistency condition that makes homology computable.

The theorem ambient_two_face_square_zero extends this from the single square to every ambient 2-face inside an n-channel distinction cube: for any configuration, any two channels i and j, and any integer coefficient, the boundary of the boundary is the zero function. A TwoFaceCert packages such a face with its base configuration, channel indices, and coefficient, and the framework proves that every finite list of these certificates has zero total boundary-of-boundary. This finite-certificate version, finite_two_face_ledger_square_zero, is the strongest statement available without a full homology API.

The framework models a ledger, a discrete record of recognition events, as the substrate from which geometry emerges. The square-zero boundary law is the consistency requirement that makes this ledger cohere into a topological object. The headline theorem cubical_chain_complex_headline packages both the local square law and the ambient 2-face law into a single conjunction, giving the framework a concrete chain-complex interface on the square.

What squareBoundaryPair does not claim is a full homology theory. The framework explicitly states that the remaining stronger target is the all-dimensions homology API, not the local ∂²=0 law. The declarations prove the local square-zero property and its finite additive strengthening, but they do not construct homology groups, Betti numbers, or any global topological invariants. The framework's own docstring marks this boundary: the local law is established, the full homology API remains open.

/-- 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

/-- 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

/-- **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 declarations do not construct homology groups, Betti numbers, or any global topological invariants. The framework does not claim a full homology API for all dimensions; that remains an open target. The square-zero law alone does not determine the framework's cost function or the golden ratio.

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: