Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.AllDimensionalCubicalBoundary

show as:
view Lean formalization →

Packages the all-dimensional cubical boundary calculus: face certificates, higher chains, and the identity ∂²=0 on n-channel cubes. Recognition analysts cite it when lifting the 1D ledger identity to arbitrary face dimension. The argument is a finite codimension-2 square-cancellation ledger, not an infinite complex.

claimFor an $n$-channel cube, a higher face certificate of dimension $d$ carries a finite ledger of codimension-2 square cancellations. On that ledger one has $\partial^2=0$. The same identity holds for higher chains assembled from such faces, yielding a uniform all-dimensional cubical boundary API.

background

Primitive Recognition Calculus treats recognition events on discrete cubes whose edges are signed ledger moves. The imported cubical chain complex supplies the low-dimensional boundary operators and the elementary face relations.

This module lifts that structure to arbitrary face dimension. A higher face certificate records an intended dimension $d$ together with the finite list of codimension-2 squares generated by that face; the second-boundary identity is reduced to pairwise cancellation on that list. Higher chains are formal sums of such certified faces.

The setting is purely combinatorial: no continuum topology is assumed. The only algebraic content needed is the cubical face incidence that makes opposite edges of each square cancel.

proof idea

The module is mostly definitional scaffolding plus short cancellation lemmas. HigherFaceCert packages dimension and the codimension-2 ledger. The second-boundary theorems (for a single higher face and for a higher chain) walk that finite ledger and invoke the square-cancellation identity already present in the cubical chain complex. AllDimensionalBoundaryAPI and the delta-cubical wrapper expose a uniform interface; the headline lemma states ∂²=0 in that interface.

why it matters in Recognition Science

Delta-native analysis and the strong-closure development import this module to treat multi-channel recognition boundaries without dimension-by-dimension casework. In the Recognition forcing chain, clean cubical boundaries underwrite the discrete octave and spatial-dimension steps (T7 eight-tick period, T8 $D=3$): once ∂²=0 holds in every dimension, higher face defects cannot accumulate into spurious topological charge. The API is the bridge from the 1-skeleton ledger to the full cubical complex used downstream.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)