twoFaceCert_boundary_squared_zero
plain-language theorem explainer
Every finite 2-face certificate on an n-channel distinction cube has vanishing boundary-of-boundary. Anyone packaging local cubical ∂²=0 for multi-distinction geometry cites this. The proof is a one-line projection onto the ambient square-zero lemma for a single face.
Claim. For any $n\in\mathbb{N}$ and any finite 2-face certificate $F$ (base configuration in the $n$-channel distinction cube, face indices $i,j\in\mathrm{Fin}\,n$, and integer coefficient $c$), the boundary-of-boundary chain carried by $F$ is the zero function on configurations.
background
The module packages Delta's multi-distinction geometry as a cubical chain complex. A configuration is a point of the $n$-channel distinction cube; faces are selected by coordinate indices in $\mathrm{Fin},n$.
A TwoFaceCert is a finite certificate for one ambient 2-face: a base configuration, two face indices, and an integer coefficient. Its boundary-of-boundary is the integer-valued chain obtained by applying the multi-distinction face operator twice to that weighted face.
Upstream, ambient_two_face_square_zero already states that any ambient 2-face (base, $i$, $j$, $c$) has square-zero boundary, via the general multi-distinction identity face_boundary_squared_zero_general. The certificate structure is only a packaging of those four data.
proof idea
One-line term proof: unpack the certificate fields and apply ambient_two_face_square_zero to F.base, F.i, F.j, and F.coeff. That lemma reduces to the general multi-distinction square-zero identity, so no new combinatorial work occurs here.
why it matters
This is the certificate-shaped form of local cubical $\partial^2=0$ inside Primitive Recognition Calculus. Downstream, twoFaceCert_list_boundary_squared_zero sums over a finite list of certificates and concludes the total boundary-of-boundary vanishes; the list theorem inducts by adding one certificate at a time and invoking this result.
In the Recognition foundation stack, square-zero boundary is the algebraic backbone that lets multi-distinction geometry support a chain complex (and later homology) rather than an ad hoc ledger of faces. It sits under the cubical-chain-complex headline and feeds finite ledger statements such as finite_two_face_ledger_square_zero. It does not itself force $\phi$, the eight-tick octave, or $D=3$; those live in the T5–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.