multi_distinction_geometry
plain-language theorem explainer
Independent binary distinction channels commute for any ambient dimension n, and the oriented boundary operators on the two-channel square (and on every 2-face of an n-cube) square to zero. Anyone building discrete geometry or cell complexes from Recognition distinctions would cite this. The proof is a three-conjunct term that packages the already-proved commutation and ∂²=0 lemmas.
Claim. For every $n\in\mathbb{N}$, channels $i,j\in\mathrm{Fin}\,n$, and integer-valued functions $f$ on $n$-channel configurations, the mixed second differences commute: $\partial_i\partial_j f=\partial_j\partial_i f$. Moreover $\partial_1\circ\partial_2=0$ on the oriented square face, and for every base configuration, pair of channels, and coefficient the ambient $n$-face boundary-of-boundary vanishes identically.
background
A configuration of $n$ independent binary distinctions is a map $\mathrm{Config},n:=\mathrm{Fin},n\to\mathrm{Bool}$: each channel sits on one of two sides. The difference operator of channel $i$ compares the two sides of that distinction while holding all other channels fixed, producing an integer-valued function on configurations.
On the explicit two-channel square the module builds a tiny oriented cell complex: four vertices, four edges (bottom, right, top, left), and one face. The face boundary $\partial_2$ sends a coefficient $c$ to the 1-chain with $+c$ on bottom and right and $-c$ on top and left. The edge boundary $\partial_1$ sends a 1-chain to the 0-chain of head-minus-tail contributions at each vertex.
Upstream, diff_comm already shows mixed second differences are symmetric in the two channels ("the channels are genuinely independent coordinate directions"). Separately, boundary_squared_zero proves $\partial_1(\partial_2 c)=0$ by case analysis on the four vertices, and the general ambient-$n$ face lemma extends the same cancellation to every oriented 2-face of an $n$-cube.
proof idea
Term-mode packaging of three prior results as a conjunction. The first conjunct is discharged by applying the mixed-difference commutation lemma at arbitrary $n$, channels $i,j$, and $f$. The second conjunct is exactly the square identity $\partial_1\circ\partial_2=0$. The third conjunct is the general ambient-$n$ face cancellation: for any base configuration, pair of channels, and coefficient, the composed face-boundary operator is the zero 0-chain. No new algebra is done here; the headline simply bundles the three load-bearing pieces.
why it matters
Phase 6 headline of the Primitive Recognition Calculus: geometry, in its two load-bearing pieces (independence of coordinate directions and closure of boundaries), is the algebra of several independent distinctions rather than an extra posit. That reading feeds the Delta-native strong-closure certificate, which assembles the closed theorem surface used downstream in the foundation stack.
In the broader Recognition forcing chain this is pre-physics scaffolding: it justifies treating multi-channel distinction space as a genuine discrete geometry before the T5–T8 steps (J-uniqueness, $\varphi$, eight-tick octave, $D=3$) are imposed. Without commuting differences and $\partial^2=0$, later constructions that treat channels as spatial or temporal coordinates would rest on an unforced geometric assumption.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.