ambient_two_face_square_zero
plain-language theorem explainer
In any n-channel binary cube, the boundary-of-boundary of every oriented ambient 2-face is the zero 0-chain. Homology and cubical-complex packaging cite this as the local ∂²=0 law on squares. The proof is a one-line application of the general face-boundary cancellation theorem.
Claim. For every dimension $n$, every base configuration of $n$ binary channels, every pair of channel indices $i,j$, and every integer coefficient $c$, the boundary-of-boundary 0-chain of the oriented 2-face spanned by $i$ and $j$ is identically zero: $\partial(\partial(\text{face}_{i,j}(c))) = 0$.
background
Multi-distinction geometry models an $n$-channel binary cube: a configuration is a map $\mathrm{Fin},n\to\mathrm{Bool}$, one side per independent distinction. The difference operator on channel $i$ compares the two sides of that distinction while holding the others fixed.
The 2-face spanned by channels $i$ and $j$ has an oriented square boundary. Its boundary-of-boundary is the explicit 0-chain faceBoundaryBoundary: eight signed vertex-indicator terms from the four oriented edges (bottom, right, top, left), intentionally left unsimplified so that $\partial^2=0$ is a pure cancellation statement.
The upstream theorem face_boundary_squared_zero_general already proves that this 0-chain vanishes for every ambient $n$, every base, every pair of channels, and every coefficient $c$, by pointwise simplification and ring cancellation of the four vertices.
proof idea
One-line term wrapper: the claim is exactly the conclusion of face_boundary_squared_zero_general, applied to the same base configuration, channel indices, and coefficient. No extra rewriting is needed; the ambient packaging theorem simply re-exports that cancellation under the cubical-chain-complex name.
why it matters
This is the ambient half of the cubical chain packaging headline: together with the fixed square-boundary pair's own $\partial^2=0$, it shows that Delta's multi-distinction geometry supplies a concrete chain-complex interface on squares and square-zero boundary on every ambient 2-face. Downstream, cubical_chain_complex_headline conjoins the two facts, and twoFaceCert_boundary_squared_zero specializes the result to every finite 2-face certificate (and thence to finite lists of certificates).
In the Recognition foundation this is the local cubical $\partial^2=0$ law, not the full all-dimensions homology API. The headline doc-comment is explicit that the stronger remaining target is that homology interface, not this cancellation. The result sits in Primitive Recognition Calculus as geometric scaffolding for ledger and certificate arguments that need square-zero boundaries before climbing the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.