faceBoundaryBoundary
plain-language theorem explainer
Explicit boundary-of-boundary 0-chain on an oriented 2-face inside an n-channel binary cube. Given a base configuration, two channels i and j, and an integer coefficient c, it assembles the eight signed vertex indicators contributed by the four oriented edges of the square. Downstream square-zero theorems cite this unsimplified expression; their proofs are pure cancellation of the four corners. Anyone packaging multi-distinction geometry as a cubical chain complex needs this map as the concrete ∂² on 2-faces.
Claim. For ambient dimension $n$, base configuration $b$ of $n$ binary channels, channel indices $i,j \in \{0,\ldots,n-1\}$, and coefficient $c \in \mathbb{Z}$, define the 0-chain that sends each configuration $w$ to the signed sum of eight vertex indicators on the four corners of the oriented square spanned by $i$ and $j$ (two contributions per edge: bottom, right, top, left), each scaled by $\pm c$. The expression is left unsimplified so that $\partial^2=0$ is a cancellation identity.
background
Multi-distinction geometry treats an $n$-channel configuration as a map from channel indices to Boolean sides: each channel is an independent binary distinction. The ambient space is the $n$-cube of all such configurations. A 2-face is selected by fixing a base configuration and two channels $i,j$; its four vertices are obtained by updating those two coordinates to the four Boolean pairs.
The integer vertex indicator of a fixed configuration $a$ is the Kronecker map sending $w$ to $1$ if $w=a$ and $0$ otherwise. Oriented edges of the face contribute $\pm c$ times the indicators of their endpoints. The present definition packages the full boundary-of-boundary 0-chain by writing out all eight endpoint contributions from the four edges (bottom, right, top, left) without algebraic simplification.
Local setting: this sits in the Primitive Recognition Calculus layer that builds geometry from commuting distinction operators, prior to the cubical chain-complex packaging that asserts $\partial^2=0$ on every ambient 2-face.
proof idea
Definitional construction, not a proof. The body is a lambda on configurations $w$ that adds eight terms: for each of the four oriented edges of the $(i,j)$-face, the two endpoint vertex indicators appear with opposite signs, all scaled by the coefficient $c$. Vertices are produced by faceVertex (double Function.update of the base on channels $i$ and $j$); indicators are the integer Kronecker maps. No lemmas are applied; the expression is deliberately left expanded so the later square-zero theorem reduces to simp plus ring cancellation of matching $\pm c$ pairs.
why it matters
This is the concrete $\partial^2$ expression that the general ambient-$n$ square-zero theorem cancels termwise, and that the cubical packaging re-exports as ambient_two_face_square_zero. The Phase-6 headline multi_distinction_geometry conjoins channel-commutation with both the explicit-square and ambient-face $\partial^2=0$ laws; the third conjunct is exactly pointwise vanishing of this map. The cubical chain-complex headline packages the same vanishing for every base, pair of channels, and coefficient, and the finite 2-face certificate structure stores the data $(base,i,j,c)$ that feed it.
In the Recognition framework this closes the geometric half of "geometry is the algebra of independent distinctions": independence is diff_comm, closure of boundaries is this cancellation. It supports the discrete cell structure underlying the eight-tick octave (T7) without positing continuum manifolds. The remaining open target named downstream is a full all-dimensions homology API; local $\partial^2=0$ on 2-faces is already discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.