d2
plain-language theorem explainer
Defines the integer 2-boundary of the unit square face as a 1-chain: coefficient c on bottom and right edges, −c on top and left (counterclockwise orientation). Anyone proving ∂²=0 on the square or assembling the cubical chain complex cites it. The body is a four-case match on the oriented edge type.
Claim. For an integer coefficient $c\in\mathbb{Z}$, the 2-boundary $\partial_2 c$ is the 1-chain on the square with $(\partial_2 c)(B)=c$, $(\partial_2 c)(R)=c$, $(\partial_2 c)(T)=-c$, $(\partial_2 c)(L)=-c$, where $B,R,T,L$ are the bottom, right, top, and left edges.
background
Multi-distinction geometry treats geometry as the algebra of several independent distinction channels. On the explicit unit square one works with oriented edges $B,T,L,R$ and integer chain groups: 0-chains are functions on the four vertices, 1-chains are functions $\mathrm{Edge}\to\mathbb{Z}$, and the 2-chain group is simply $\mathbb{Z}$ (one face).
The companion operator $\partial_1$ sends each oriented edge to head minus tail at vertices. The present map is the face boundary $\partial_2$: it posts the single face coefficient onto the four boundary edges with the standard counterclockwise sign pattern (bottom and right positive, top and left negative).
This is the elementary cell used before the general ambient-$n$ face cancellation: first prove $\partial_1\circ\partial_2=0$ on the square, then lift to every oriented 2-face in an $n$-channel cube.
proof idea
Pure definition by cases. On input $c:\mathbb{Z}$ return the function that assigns $c$ to edges $B$ and $R$, and $-c$ to edges $T$ and $L$. No lemmas are invoked; the match exhausts the inductive edge type.
why it matters
This is the concrete $\partial_2$ that makes the square a chain complex. Downstream, boundary_squared_zero shows $\partial_1(\partial_2 c)=0$ by evaluating at each vertex and cancelling opposite contributions; that identity is one conjunct of the Phase 6 headline multi_distinction_geometry, which asserts that independent distinction channels commute and that assembled oriented cell complexes have $\partial^2=0$.
squareBoundaryPair packages $\partial_2$ and $\partial_1$ into an explicit two-step BoundaryPair over $\mathbb{Z}$. In the broader Recognition story this is the load-bearing algebraic fact that geometry (coordinate independence plus closed boundaries) is forced by multi-distinction structure rather than posited. It sits under the cubical chain complex used on the path toward continuum and Regge-type gravity bridges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.