all_dimensional_cubical_boundary_headline
plain-language theorem explainer
Packages three nilpotency facts: every higher-dimensional cubical face certificate, every finite chain of them, and the Delta-native boundary API all have vanishing second boundary on n-channel cubes. Anyone citing the all-dimensional finite ∂²=0 API for the Delta plan uses this headline. The proof is a three-component term that reuses the face, chain, and API square-zero lemmas.
Claim. For every $n\in\mathbb{N}$, every higher-dimensional cubical face certificate on an $n$-channel cube has vanishing second boundary; every finite chain of such certificates has vanishing second boundary; and the canonical Delta-native all-dimensional cubical boundary API likewise sends every such chain to the zero second-boundary functional.
background
In the Primitive Recognition Calculus, cubical boundaries are tracked by finite certificates rather than abstract chain complexes. A higher-dimensional face certificate on an $n$-channel cube records an intended face dimension together with a finite ledger of codimension-2 square certificates (TwoFaceCert). Its second-boundary display is the pointwise sum of the boundary-of-boundary displays of those squares.
A higher chain is simply a finite list of such face certificates; its second boundary sums the face-level second boundaries. The module builds a canonical Delta-native API whose secondBoundary field is exactly this chain-level map, with a packaged square_zero proof.
Upstream, each square certificate already has vanishing boundary-of-boundary, so finite ledgers and finite chains inherit $\partial^2=0$ by fold and induction. The local setting is the all-dimensional finite boundary layer required by the Delta plan.
proof idea
Term-mode triple constructor. The first conjunct is higherFace_secondBoundary_zero: a face certificate's second boundary is a finite ledger of zero 2-face $\partial^2$ terms, so the fold is identically zero. The second is higherChain_secondBoundary_zero: induct on the list of face certificates and cancel each summand. The third applies the API field deltaCubicalBoundaryAPI.square_zero, which is definitionally the same chain-level lemma. No new cancellation arithmetic appears at this layer.
why it matters
This is the headline all-dimensional finite cubical boundary API demanded by the Delta plan: every finite higher chain whose second boundary decomposes into codimension-2 square certificates satisfies $\partial^2=0$. Downstream it is consumed by strongClosureCertificate in DeltaNativeStrongClosure, which assembles the closed Delta-native theorem surface (real forgetful display, generable carrier, certified analytic protocols, transformers).
In the Recognition foundation stack this supplies the higher-dimensional cubical nilpotency layer beneath recognition calculus and forcing-chain geometry. It does not itself force $D=3$ or the eight-tick octave (T7/T8); it only certifies that the finite cubical boundary calculus used by Delta is square-zero in every dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.