boundary_squared_zero
plain-language theorem explainer
On the two-channel square, composing the face boundary with the edge boundary yields the zero 0-chain for any integer coefficient. Builders of the cubical chain complex and the multi-distinction geometry headline cite this as the elementary ∂²=0 check. The proof is a four-vertex case split that cancels oriented edge contributions by simplification.
Claim. For every integer coefficient $c$, the edge-boundary of the face-boundary of $c$ is the zero $0$-chain: $\partial_1(\partial_2 c)=0$ at every vertex of the square.
background
The local setting is the explicit two-channel square cell: four vertices ($v_{00},v_{10},v_{01},v_{11}$) and four oriented edges (bottom, right, top, left). Integer $0$-chains and $1$-chains are functions on those vertices and edges.
The face boundary $\partial_2$ sends a coefficient $c$ to the counterclockwise $1$-chain with $+c$ on bottom and right and $-c$ on top and left. The edge boundary $\partial_1$ sends a $1$-chain to a $0$-chain by the usual head-minus-tail rule at each endpoint: bottom contributes $v_{10}-v_{00}$, top $v_{11}-v_{01}$, left $v_{01}-v_{00}$, right $v_{11}-v_{10}$.
Upstream face maps from singular simplices and prisms supply the broader geometric language; here only the combinatorial square operators are needed.
proof idea
Pointwise extensionality on vertices, then a four-way case split on the vertex enum. At each vertex, simp unfolds $\partial_1$ and $\partial_2$ and the signed edge contributions cancel algebraically (two $+c$ and two $-c$ meet at every corner). No external lemmas beyond the definitions of the two boundary maps.
why it matters
This is the load-bearing $\partial^2=0$ fact for the explicit square. Downstream, squareBoundaryPair packages $\partial_2$, $\partial_1$, and this identity into a two-step chain complex over $\mathbb{Z}$. The Phase 6 headline multi_distinction_geometry quotes it as the middle conjunct: independent distinction channels commute, and assembled into an oriented cell complex their boundaries square to zero, first on this square and then for every oriented $2$-face in an ambient $n$-channel cube. In Recognition terms, closure of boundaries is forced by the two-channel cell algebra rather than posited as extra geometry; it sits under the foundation layer that later supports the forcing chain's dimensional and octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.