higherFace_secondBoundary_zero
plain-language theorem explainer
Any higher-dimensional cubical face certificate on an n-channel cube has identically zero second boundary. The second boundary is the sum of boundary-of-boundary displays from a finite ledger of codimension-2 two-face certificates, each of which cancels. Cite this when assembling all-dimensional cubical ∂²=0 for the Delta plan. The proof is a one-line application of the finite-list two-face identity.
Claim. For every natural number $n$ and every higher-dimensional cubical face certificate $F$ in an $n$-channel cube (a dimension tag together with a finite list of two-face certificates recording codimension-2 square cancellations), the second-boundary display of $F$ is the zero function on configurations: $F.secondBoundary(w)=0$ for all configurations $w$.
background
In the Primitive Recognition Calculus, cubical boundaries are tracked by finite certificates rather than infinite formal chains. A two-face certificate packages the local square cancellations that make $\partial^2=0$ hold on a single 2-face of an $n$-channel cube. A higher-dimensional face certificate records an intended face dimension and a finite ledger of such two-face certificates: the codimension-2 squares generated by that face.
The second-boundary display of such a certificate is the pointwise sum, over the ledger, of each two-face certificate's boundary-of-boundary integer on configurations. The module builds an all-dimensional finite boundary API on top of the cubical chain complex layer.
The key upstream fact is that any finite list of two-face certificates has total boundary-of-boundary equal to the zero function: the additive finite-certificate form of local cubical $\partial^2=0$.
proof idea
One-line term proof. By definition, the second boundary of a higher face certificate $F$ is exactly the fold-sum of boundaryBoundary over $F$'s two-face ledger. Apply twoFaceCert_list_boundary_squared_zero to that ledger; the resulting function equals fun _ => 0. No induction or case split is needed at this layer.
why it matters
This is the face-level half of the all-dimensional cubical $\partial^2=0$ package. It is the first conjunct of all_dimensional_cubical_boundary_headline, the Delta-plan headline that every finite higher-dimensional cubical chain whose second boundary decomposes into codimension-2 square certificates has zero second boundary. It is also used by higherChain_secondBoundary_zero, which lifts the same identity from a single face certificate to a finite chain of them.
In the Recognition foundation stack this supplies the certified cubical boundary calculus needed before dimensional forcing (T8, $D=3$) and the eight-tick octave (T7) can be read off discrete recognition geometry. It closes the face case of the finite-certificate $\partial^2=0$ API rather than leaving a scaffolding hole.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.