Foundation Primitive Recognition Calculus Cubical Chain Complex Cubical Chain Co

The square-zero law

A chain complex is a standard mathematical staircase: objects on each floor, arrows that descend one floor, and the rule that walking down two steps always lands on zero. The framework's machine-checked library of formal theorems proves this two-step rule for its own primitive geometry of distinctions, the setting it uses to build recognition events. The declaration cubical_chain_complex_headline packages that proof as a single theorem: on the square, and on every ambient two-dimensional face inside an n-channel cube, the boundary of a boundary is zero.

The square case is explicit. The framework defines a boundary pair: a map d₂ from two-dimensional cells to one-dimensional edges, a map d₁ from edges to points, and the proof that d₁ followed by d₂ sends every cell to zero. The headline theorem then extends the same square-zero law to any two-face chosen inside a larger cube. A certificate records such a face: a base configuration, two channel indices, and an integer coefficient. The library proves that every single certificate has zero boundary-of-boundary, and that any finite list of certificates, added together, still has zero total boundary-of-boundary. This is the additive finite-certificate version of the local law.

What the declaration does not claim is the larger target. The docstring names the remaining stronger goal: a full all-dimensions homology API, the machinery that would compute holes and invariants across every dimension at once. The headline theorem is the local ∂²=0 law, proved for the square and for finite collections of certified two-faces. It is not a homology theory. It does not define cycles, boundaries, or quotient groups; it does not compute Betti numbers; it does not connect to the framework's forcing chain or to any physical constant. The theorem is a foundation stone, not a building.

In plain terms, the declaration establishes that the framework's primitive geometry is consistent at the lowest level: boundaries behave, twice is zero, and finite sums of certified faces respect that rule. That consistency is what a later homology API would build on. The reader should take away one fact: the square-zero law holds locally and for finite collections, and everything stronger remains open.

/-- **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 define cycles, boundaries, or homology groups. The declaration does not compute Betti numbers or any global invariant. The declaration does not connect to the framework's forcing chain or physical constants.

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: