d1
plain-language theorem explainer
The first boundary map on the unit square sends a 1-chain (integer weights on the four edges) to a 0-chain (integer weights on the four vertices) by the usual head-minus-tail rule. Anyone building the two-step cubical complex or proving ∂²=0 on the face cites it. The body is an exhaustive case split on the four vertices, assembling the signed edge contributions.
Claim. Define the boundary operator $\partial_1 : C_1 \to C_0$ on the square by sending each integer-valued edge weighting $g$ to the vertex weighting whose value at a vertex is the signed sum of incident edge weights (head $+$, tail $-$). Explicitly: $\partial B = v_{10}-v_{00}$, $\partial T = v_{11}-v_{01}$, $\partial L = v_{01}-v_{00}$, $\partial R = v_{11}-v_{10}$, extended $\mathbb{Z}$-linearly.
background
In this module, 0-chains are integer functions on the four square vertices $v_{00},v_{10},v_{01},v_{11}$, and 1-chains are integer functions on the four oriented edges $B,T,L,R$. The 2-chain group is simply $\mathbb{Z}$ (one face). The dual second boundary $\partial_2$ orients that face counterclockwise: bottom and right positive, top and left negative.
The local setting is primitive multi-distinction geometry: independent binary distinction channels assemble into an oriented cell complex. Closure of boundaries ($\partial^2=0$) is not an extra geometric axiom; it is forced by the two-channel cell structure once edges are oriented consistently around the face.
Related upstream language (domain coarsening boundaries, polarized interface edges) counts forced distinctions between adjacent cells. Here the same idea is packaged as the algebraic boundary of a 1-chain on the elementary square.
proof idea
Definition by cases, not a derived proof. On input $g:C_1$, evaluate the output 0-chain at each of the four vertices by matching on the vertex constructor and summing the incident edge weights of $g$ with the standard orientation signs: at $v_{00}$ both bottom and left enter negatively; at $v_{10}$ bottom is positive and right negative; at $v_{01}$ top is negative and left positive; at $v_{11}$ top and right are positive. That is exactly the linear extension of head-minus-tail on each edge.
why it matters
This map is half of the explicit square chain complex. Downstream, boundary_squared_zero proves $\partial_1\circ\partial_2=0$ by simplifying against this definition, and multi_distinction_geometry packages that identity with channel-commutation as the Phase 6 headline: geometry (independent directions plus closed boundaries) is the algebra of several independent distinctions.
squareBoundaryPair installs $\partial_1$ and $\partial_2$ as a BoundaryPair over $\mathbb{Z}$. Gravity-side consumers (Regge/Bloch midpoint identities and the conditional quantum-gravity master theorem) reuse the same square boundary data when they need a certified 2-face cancellation kernel. In the broader RS forcing picture this is scaffolding for D=3 and the eight-tick cell structure: boundaries must close before higher-dimensional recognition geometry can be forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.