face_boundary_squared_zero_general
plain-language theorem explainer
In any n-channel configuration cube, the double boundary of an oriented 2-face (two selected channels, fixed base configuration, integer weight) is the zero 0-chain. Foundation workers and anyone building the cubical chain complex of multi-distinction geometry cite it for ambient-n ∂²=0. The proof is pointwise unfolding plus ring cancellation of the four signed vertices.
Claim. For every $n\in\mathbb{N}$, every base configuration of $n$ binary channels, every pair of channel indices $i,j\in\{0,\ldots,n-1\}$, and every integer coefficient $c$, the boundary of the boundary of the corresponding oriented square is the zero $0$-chain: $\partial(\partial\sigma_{i,j,c})=0$ as a function on vertices.
background
A configuration of $n$ independent binary distinctions is a map from channel indices to sides (each channel is on or off). Multi-distinction geometry treats the $n$-cube of such configurations as an oriented cell complex: 0-cells are configurations, 1-cells flip one channel holding the rest fixed, and 2-cells are the coordinate squares spanned by two channels.
The double face-boundary operator, given a base configuration, two channel indices, and a weight $c\in\mathbb{Z}$, assembles the cubical boundary twice on that oriented square and returns a $0$-chain (an integer-valued function on vertices). The module already records that single-channel difference operators commute and that the explicit unit square satisfies $\partial^2=0$; the present statement lifts the latter to every ambient $n$ and every embedded 2-face.
Local setting is Phase 6 of the Primitive Recognition Calculus: independence of coordinate directions and closure of boundaries should be pure algebra of several independent distinctions, not an extra geometric posit.
proof idea
Short term-mode argument. Extensionality reduces the claim to a pointwise identity on vertices. Unfolding the double face-boundary definition exposes the four signed vertex contributions of the oriented square (the usual cubical $\partial^2$ pattern). A single ring step cancels those contributions identically, yielding zero at every vertex. No external lemmas are required beyond the definition and integer ring arithmetic; the cancellation is the same four-term telescoping that makes $\partial^2=0$ on any square.
why it matters
Direct input to the Phase 6 headline, which packages three facts: channel difference operators commute for general $n$, the explicit square has $\partial^2=0$, and every oriented 2-face in any ambient $n$-channel cube has $\partial^2=0$. The third conjunct is exactly this theorem. CubicalChainComplex re-exports it as the ambient two-face square-zero statement, so the cubical packaging of multi-distinction geometry depends on it verbatim.
In Recognition terms this is one of the two load-bearing geometric pieces (the other is independence of directions): closure of boundaries is forced by the algebra of independent distinctions rather than assumed. It sits in the foundation layer that later supports higher chain-level structure; it does not itself invoke the forcing chain T0–T8, the J-cost, or the eight-tick octave, but it supplies the chain-complex hygiene those layers need when geometry is assembled from distinctions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.