cubical_chain_complex_headline
plain-language theorem explainer
Packages two square-zero facts for Delta multi-distinction geometry: the explicit square chain complex satisfies d1 after d2 equals zero, and every ambient 2-face in an n-channel cube has vanishing double boundary. Cite it for the cubical chain interface on binary distinction cubes. Proof is a one-line pair of the two established square-zero lemmas.
Claim. For every integer coefficient $c$, the two-step boundary maps of the explicit Delta square satisfy $d_1(d_2(c))=0$. Moreover, for every $n$, every $n$-channel binary configuration, every pair of channels $i,j$, and every coefficient $c$, the boundary-of-boundary $0$-chain on the oriented $2$-face spanned by $i$ and $j$ is the zero function on configurations.
background
Multi-distinction geometry models $n$ independent binary channels as configurations $\mathrm{Config},n = \mathrm{Fin},n \to \mathrm{Bool}$. Difference operators on single channels produce $1$-chains; pairs of channels span oriented $2$-faces whose four edges contribute eight signed vertex terms. The double-boundary map faceBoundaryBoundary is that unsimplified eight-term $0$-chain; its vanishing is the local $\partial^2=0$ law on every ambient $2$-face.
The module packages the elementary square as an explicit two-step chain complex squareBoundaryPair with $d_2$ and $d_1$ taken from the multi-distinction differentials, and with a built-in square-zero witness. Upstream, ambient_two_face_square_zero already records that every ambient $2$-face has vanishing double boundary, by reduction to the general face-boundary-squared-zero lemma in MultiDistinctionGeometry.
The local setting is foundation-level chain packaging for Delta's binary cubes, not yet a full cubical homology API in all dimensions.
proof idea
Term-mode pair constructor. The first conjunct is exactly the square_zero field of squareBoundaryPair (itself proved by applying MultiDistinctionGeometry's boundary-squared-zero on the square). The second conjunct is discharged pointwise by ambient_two_face_square_zero, which reduces each ambient $2$-face double boundary to the general face-boundary-squared-zero identity. No new cancellation arithmetic appears here.
why it matters
Doc-comment calls this the cubical chain packaging headline: Delta multi-distinction geometry now exposes a concrete chain-complex interface on the square together with square-zero boundary on every ambient $2$-face. That is the local $\partial^2=0$ law needed before any homology or ledger-counting argument on distinction cubes can be trusted.
No downstream consumers are wired yet (used_by is empty). The same module already carries finite $2$-face certificates and list-level square-zero lemmas that sit beside this headline; the remaining stronger target, stated in the doc-comment, is a full all-dimensions homology API, not another local double-boundary identity. In the Recognition foundation stack this sits under Primitive Recognition Calculus, feeding any later argument that treats multi-channel distinctions as a cubical complex rather than an ad-hoc sign bookkeeping device.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.