Foundation Primitive Recognition Calculus Cubical Chain Complex Two Face Cert Li

The finite certificate ledger

A boundary is the edge of a shape. In geometry, a standard fact is that the boundary of a boundary is empty: the edges of a square's perimeter have no endpoints left over. The Recognition Science declaration twoFaceCert_list_boundary_squared_zero establishes this same fact for a finite collection of square faces inside an n-dimensional distinction cube. Each face is certified by a base configuration, two channel indices, and an integer coefficient. The theorem states that when you take the boundary of each face, then take the boundary of that result, and add up all contributions across the list, the total is exactly zero at every point.

The declaration is a theorem in the framework's machine-checked library of formal theorems. It builds on two earlier results: the square boundary pair, which defines the boundary maps, and the ambient two-face square-zero theorem, which proves the local law for a single face. The list version extends this by induction. The proof works by taking each face in the list, applying the single-face theorem, and summing the results. The final statement, finite_two_face_ledger_square_zero, packages this for all dimensions n and all finite lists at once.

What the declaration does not claim is a full homology theory. It proves the local square-zero law for finite collections, but it does not define cycles, boundaries, or homology groups in all dimensions. The docstring explicitly names the stronger target as the full all-dimensions homology API. The theorem is a consistency check on the existing definitions, not a complete topological structure. It also does not claim anything about infinite collections, since the proof uses induction over finite lists.

The practical consequence is that any finite ledger of certified 2-faces in the framework's recognition calculus is internally consistent: no boundary-of-boundary residue accumulates. This matters because it means the local geometry of the distinction cube is coherent under finite aggregation, a necessary precondition for any future homology construction. The theorem is a stepping stone, not the destination.

/-- A finite list of two-face certificates has zero total boundary-of-boundary.
This is the additive finite-certificate version of local cubical `∂²=0`. -/
theorem twoFaceCert_list_boundary_squared_zero {n : ℕ} (faces : List (TwoFaceCert n)) :
    (fun w : MultiDistinctionGeometry.Config n =>
      faces.foldl (fun acc F => acc + F.boundaryBoundary w) 0) = fun _ => 0 := by
  induction faces with
  | nil =>
      funext w
      simp
  | cons F rest ih =>
      funext w
      have hF := congrFun (twoFaceCert_boundary_squared_zero F) w
      have hrest := congrFun ih w
      simp [List.foldl_cons, hF, hrest]

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

What this page does not claim

It does not prove the existence of nontrivial cycles or homology groups. It does not apply to infinite collections of faces. It does not establish any physical claim about three-dimensional space.

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: