Foundation Primitive Recognition Calculus Multi Distinction Geometry Face Bounda

The boundary of a boundary

In ordinary geometry, the boundary of a boundary is empty. A disk's boundary is a circle, and that circle has no boundary of its own. The declaration face_boundary_squared_zero_general proves that the same principle holds inside the Recognition Science framework's model of geometry, where space is built from independent binary distinctions rather than from points and lines.

The framework models a configuration of distinctions as a cube: with n independent channels, each either on or off, there are 2^{n possible states. A 2-face of this cube is a square spanned by two channels, with the other channels held fixed. The declaration states that for any such square, in any ambient cube, the boundary of the square's boundary is the zero chain. Written out, the eight vertex contributions cancel in pairs, leaving nothing.}

This is not an assumption. The proof is a direct computation in the machine-checked library of formal theorems: the definition of the boundary operator, applied twice, simplifies by pure cancellation. The result holds for every choice of base configuration, every pair of channels, and every integer coefficient. It is the discrete analogue of the classical identity ∂² = 0, which in continuous geometry guarantees that boundaries fit together consistently.

In Recognition Science, this identity is load-bearing. It shows that the geometry of independent distinctions is not an extra posit but an algebra: the commutativity of channels (making distinction i then j equals making j then i) and the closure of boundaries together give the two structural properties that geometry needs. The framework's claim is that these properties emerge from the ledger of recognition events, not that they are imposed from outside.

The declaration does not claim that this discrete boundary identity explains any particular physical phenomenon, nor that it derives the dimension of space. It establishes a consistency condition within the framework's model. The step from this algebraic fact to physical geometry, such as the claim that three spatial dimensions are forced, is a separate bridge that the framework leaves open.

/-- **General ambient-n `∂² = 0` for 2-faces.** In any `n`-channel cube, for any
two selected channels and any base configuration, the boundary of the boundary of
the corresponding oriented square is the zero 0-chain. The proof is pure
cancellation of the four vertices. -/
theorem face_boundary_squared_zero_general {n : ℕ} (base : Config n) (i j : Fin n) (c : ℤ) :
    faceBoundaryBoundary base i j c = fun _ => 0 := by
  funext w
  simp [faceBoundaryBoundary]
  ring

What this page does not claim

This declaration does not derive the number of spatial dimensions. This declaration does not explain any specific physical phenomenon. This declaration does not claim that the discrete boundary identity is the only source of geometric structure.

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/MultiDistinctionGeometry.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: