diff_comm
plain-language theorem explainer
Mixed second differences along two binary distinction channels commute for any configuration space of n channels. Anyone building multi-channel recognition geometry or the Phase 6 cell-complex argument cites this. The proof splits on whether the channels coincide, then uses update-commutation and a four-term ring identity when they differ.
Claim. For any $n\in\mathbb{N}$, channels $i,j\in\{0,\ldots,n-1\}$, and integer-valued $f$ on configurations $\mathrm{Config}_n=(\mathrm{Fin}\,n\to\mathrm{Bool})$, the channel difference operators satisfy $\partial_i(\partial_j f)=\partial_j(\partial_i f)$, where $(\partial_k g)(v)=g(v[k\mapsto\mathsf{true}])-g(v[k\mapsto\mathsf{false}])$.
background
In MultiDistinctionGeometry, 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 every other channel fixed: $(\partial_i f)(v)=f(v[i\mapsto\mathsf{true}])-f(v[i\mapsto\mathsf{false}])$.
The local setting is the algebra of several independent distinctions before any continuum geometry is assumed. Commutation of mixed second differences is the discrete statement that the channels behave as independent coordinate directions. The same module later assembles these operators into an oriented cell complex whose boundary squares to zero.
Upstream, $\partial_i$ is the only nontrivial ingredient; Mathlib supplies Function.update_comm for swapping two distinct pointwise updates of a function.
proof idea
Term-mode proof by cases on whether $i=j$.
If $i=j$, substitute and both sides are identical by definition, so rfl closes.
If $i\neq j$, extensionality on the configuration $v$ reduces the claim to an equality of integers. Unfold $\partial$ twice; each side becomes a four-term alternating sum of $f$ at the four corners obtained by setting channels $i$ and $j$ independently to true/false. Four applications of Function.update_comm (for the pairs of updates with values true/true, true/false, false/true, false/false) align the arguments, after which ring cancels the alternating sums.
why it matters
This is the first load-bearing piece of the Phase 6 headline multi_distinction_geometry: independent distinction channels commute for general $n$, and assembled into an oriented cell complex their boundary squares to zero. The parent packages this lemma as the left conjunct of that conjunction, then pairs it with $d_1\circ d_2=0$ on the explicit square and on every oriented 2-face of an ambient $n$-cube.
In Recognition Science terms, geometry (independence of coordinate directions, closure of boundaries) is forced as the algebra of several independent distinctions rather than posited. That feeds the broader forcing chain: once multi-channel independence is algebraic, the eight-tick octave and $D=3$ spatial dimensions (T7–T8) sit on a discrete skeleton that already knows how to commute mixed differences. No open scaffold remains here; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.