deltaCubicalBoundaryAPI
plain-language theorem explainer
Packages the all-dimensional finite cubical second-boundary operator and its vanishing law into one Delta-native API record. Anyone citing the all-dimensional cubical boundary headline, or the Delta plan's finite boundary interface, points here. The construction is a two-field structure instance: the fold of face second-boundaries, plus the already-proved chain-level square-zero theorem.
Claim. The canonical all-dimensional cubical boundary API is the pair consisting of (i) the second-boundary map sending each finite higher-dimensional chain $C$ (a list of higher face certificates in dimension $n$) to the integer-valued configuration functional obtained by folding face second-boundaries, and (ii) the identity that this second boundary vanishes identically on every such chain.
background
In the primitive recognition calculus, a higher face certificate packages a codimension-2 square decomposition of a cubical face boundary. A finite higher-dimensional chain is simply a list of such certificates in fixed dimension $n$. Its second boundary is the configuration functional obtained by folding the individual face second-boundaries (integer-valued on configurations).
The structure AllDimensionalBoundaryAPI is the thin interface the Delta plan needs in every dimension: a second-boundary display for every finite higher chain, together with the assertion that the display is identically zero. Upstream, the chain-level vanishing theorem already proves that fold is the zero functional, by induction on the list (nil base case plus face-level square-zero).
This module sits in the Foundation primitive-recognition layer and imports the cubical chain complex scaffolding. The API is deliberately finite and certificate-driven: no infinite chains, no homology computation beyond $d^2=0$ at the second boundary.
proof idea
Definitional instance, not a tactic proof. The second-boundary field is definitionally the existing fold HigherChain.secondBoundary. The square-zero field is a direct application of the upstream theorem that every finite higher-dimensional chain has vanishing second boundary (list induction reducing to face-level square certificates). No new algebra is introduced.
why it matters
This is the packaged all-dimensional finite boundary API required by the Delta plan. The downstream headline theorem quotes it explicitly: every finite higher-dimensional cubical chain whose second boundary decomposes into codimension-2 square certificates has zero second boundary, and the third conjunct is precisely that this API's second-boundary field vanishes.
In the Recognition forcing picture the cubical boundary calculus underwrites discrete recognition steps on the lattice (eight-tick octave structure, $D=3$ spatial forcing). Having a single named API that works uniformly in all dimensions keeps the Delta-native interface stable while face- and chain-level vanishing lemmas evolve underneath. It does not itself force dimension or the J-cost; it only seals $d^2=0$ for finite cubical chains in the certificate language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.