BoundaryPair
plain-language theorem explainer
Packages a two-step chain complex: maps from 2-chains to 1-chains and 1-chains to 0-chains whose composition is identically zero. Anyone wiring multi-distinction or cubical boundaries in the Primitive Recognition Calculus cites this carrier. It is a pure structure definition; the square-zero law is a field, not a derived theorem.
Claim. A structure over types $C_2$, $C_1$, $C_0$ (with a zero element on $C_0$) consisting of maps $d_2 : C_2 \to C_1$ and $d_1 : C_1 \to C_0$ such that $d_1(d_2(c)) = 0$ for every $c \in C_2$.
background
In algebraic topology a chain complex is a sequence of modules with boundary maps satisfying $d \circ d = 0$. Here the same idea is stripped to two steps and typed over bare Lean types rather than abelian groups: only $C_0$ needs a zero so the identity $d_1 \circ d_2 = 0$ is well-formed.
The ambient module is the Primitive Recognition Calculus cubical layer. Multi-distinction geometry supplies concrete chain spaces $C_2$, $C_1$, $C_0$ and explicit boundary operators built from distinction acts and ratio orbits. The structure does not itself mention the J-cost or the phi-ladder; it only records the nilpotency law that those geometric boundaries must obey.
Upstream material (one-step trace extension by $\delta$, the ratio orbit $2$, continuum Laplacian identifications) motivates why a two-face square appears, but is not required to read the structure itself.
proof idea
No proof body. The declaration is a structure with three fields: the two boundary maps and a propositional field asserting that boundary after boundary vanishes on every 2-chain. Instantiations discharge square_zero by citing a concrete nilpotency lemma (for example the multi-distinction boundary_squared_zero).
why it matters
This is the minimal interface that lets the cubical PRC layer talk about $d^2 = 0$ without fixing a particular geometry. The immediate consumer is squareBoundaryPair, which fills the three fields with the multi-distinction operators $d_2$, $d_1$ and proves square-zero by the ambient boundary-squared lemma. Sibling results (ambient_two_face_square_zero, twoFaceCert_boundary_squared_zero, the finite two-face ledger square-zero theorem, and the cubical chain-complex headline) all sit on top of that pattern.
In the Recognition forcing picture the eight-tick octave and $D = 3$ eventually need a discrete exterior calculus whose boundaries square to zero; this structure is the local algebraic placeholder for that requirement. It does not yet force dimension or tick period; it only standardizes the nilpotency certificate those later steps will reuse.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.