squareBoundaryPair
plain-language theorem explainer
Packages the multi-distinction square (one face, four edges, four vertices) as an explicit two-step chain complex over ℤ with ∂₁∘∂₂ = 0. Anyone citing the cubical chain-complex headline uses this object as the concrete square interface. The construction is a thin structure instance: the two boundary maps are the ambient d₂ and d₁, and square-zero is the existing cancellation theorem.
Claim. The multi-distinction square carries a two-step chain complex with $C_2 = \mathbb{Z}$, $C_1 = (\mathrm{Edge} \to \mathbb{Z})$, $C_0 = (\mathrm{Vtx} \to \mathbb{Z})$, boundary maps $d_2 : C_2 \to C_1$ and $d_1 : C_1 \to C_0$ from multi-distinction geometry, and $d_1(d_2 c) = 0$ for every $c \in \mathbb{Z}$.
background
Multi-distinction geometry models a single square face with integer chains: 0-chains are functions from the four vertices to ℤ, 1-chains from the four oriented edges to ℤ, and the 2-chain group is just ℤ (one face). The face boundary $d_2$ is the counterclockwise 1-chain (bottom and right positive, top and left negative); $d_1$ is the usual edge-to-vertex incidence.
BoundaryPair is the local packaging of a two-step complex: maps $d_2 : C_2 \to C_1$, $d_1 : C_1 \to C_0$, and the law $\forall c,, d_1(d_2 c)=0$. Upstream, boundary_squared_zero already proves that law on this square: "the boundary of the boundary of the face is the zero 0-chain... oriented edges around the face cancel at every vertex."
This module sits in Primitive Recognition Calculus: it turns that geometric cancellation into a reusable chain-complex interface rather than leaving ∂²=0 as a bare lemma.
proof idea
Definitional structure instance, not a deep proof. Set $d_2$ to the ambient multi-distinction face boundary and $d_1$ to the edge boundary. Discharge square_zero by introducing an arbitrary 2-chain coefficient $c$ and applying boundary_squared_zero directly. No new algebra: the cancellation is imported wholesale from MultiDistinctionGeometry.
why it matters
This is the concrete square half of the cubical chain packaging headline. That headline asserts both (i) square-zero on this packaged pair and (ii) square-zero for every ambient 2-face in an $n$-channel cube; the first conjunct is exactly squareBoundaryPair.square_zero.
In the Recognition foundation stack, local ∂²=0 on the elementary square is the minimal chain-complex fact needed before ambient multi-channel faces and finite two-face ledgers. The headline itself notes the remaining stronger target is a full all-dimensions homology API, not this local law. The construction does not yet touch T7 (eight-tick octave) or T8 ($D=3$), but it is the 2-skeleton substrate those discrete geometric claims sit on once cubes and higher cells are assembled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.