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. Analysts of the native recognition differential cite it when lifting 1D ledger cancellations to full cubical homology. The argument is finite square-cancellation bookkeeping per face, packaged as a reusable boundary API.

claimFor an $n$-channel cube, a higher face certificate of dimension $d$ carries a finite ledger of codimension-2 square cancellations. On the associated higher chain, the cubical boundary satisfies $\partial^2=0$. The module exposes a single all-dimensional boundary API specializing this identity for the native recognition differential.

background

Primitive recognition calculus treats discrete recognition events on cubical complexes built from $n$ binary channels (the eight-tick octave is the $n=3$ case). The imported cubical chain complex supplies faces, edges, and the formal boundary operator $\partial$ on chains.

A higher-dimensional face certificate records an intended face dimension together with the finite list of codimension-2 squares generated by that face. Each such square contributes a signed pair of 1-chains that cancel in $\partial^2$. Higher chains assemble these certificates so the same cancellation ledger proves $\partial^2=0$ uniformly in dimension, not only on edges.

The module sits in the Foundation layer: it does not yet specialize constants ($\varphi$, $J$-cost, mass rungs) but supplies the combinatorial skeleton those specializations will use.

proof idea

Definition-heavy module with short algebraic lemmas. Higher face certificates package the codimension-2 square ledger; higherFace_secondBoundary_zero checks pairwise cancellation on that ledger. Higher chains lift the same check to assembled faces via higherChain_secondBoundary_zero. The public API (AllDimensionalBoundaryAPI, deltaCubicalBoundaryAPI) and the headline theorem simply re-export $\partial^2=0$ in the form downstream native-$\Delta$ analysis expects. No analytic estimates; pure finite signed cancellation.

why it matters in Recognition Science

Downstream modules DeltaNativeAnalysis and DeltaNativeStrongClosure import this boundary API to treat the native recognition differential as a genuine cubical coboundary (so closed loops and exactness statements are well-typed). Without all-dimensional $\partial^2=0$, strong closure of discrete recognition dynamics would be stuck at the 1-skeleton.

In the broader forcing chain this is scaffolding under T7 (eight-tick octave, period $2^3$): the cube dimension $n$ is free here, and $n=3$ is the physically forced case. It does not itself force $D=3$ or the $J$-cost; it only guarantees that whatever differential is later placed on the cube is a complex.

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)