diff_self_comm
plain-language theorem explainer
The second difference of an integer-valued function on n-channel configurations, taken twice along the same channel, equals itself. Cited when treating self-commutation as the degenerate case of channel independence on the multi-distinction complex. The proof is pure definitional reflexivity.
Claim. For every $n\in\mathbb{N}$, channel index $i\in\{0,\ldots,n-1\}$, and $f:\{\text{configs of $n$ binary distinctions}\}\to\mathbb{Z}$, the second difference along channel $i$ satisfies $\Delta_i(\Delta_i f)=\Delta_i(\Delta_i f)$.
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 channel difference $\Delta_i f$ compares the two sides of distinction $i$ while holding every other channel fixed: $$(\Delta_i f)(v)=f(v[i\mapsto\mathsf{true}])-f(v[i\mapsto\mathsf{false}]).$$
The ambient module builds the oriented 2-channel cell complex (the square) and aims at $\partial^2=0$. The mixed second-difference identity (independent channels commute) is the nontrivial sibling; the present statement is the diagonal case $i=i$, where order is automatic.
Doc-comment framing: a channel applied twice annihilates configs constant along that channel; more basically, the second difference along one channel is itself a difference, so order never matters even in the degenerate case.
proof idea
Term-mode proof by rfl. Both sides of the equality are definitionally the same expression $\Delta_i(\Delta_i f)$, so Lean closes the goal by reflexivity with no lemmas and no unfolding of diff.
why it matters
Sits in Primitive Recognition Calculus multi-distinction geometry, the discrete substrate in which independent binary channels act as coordinate directions before continuum geometry is recovered. Together with the mixed commutator diff_comm, it records that second differences are symmetric in channel order, including the self case.
Downstream the module develops vertices and edges of the square, coboundary operators $d_1,d_2$, and boundary_squared_zero ($\partial^2=0$). That nilpotency is the combinatorial skeleton behind eight-tick octave structure (T7) and three spatial dimensions (T8) in the forcing chain. No parent theorem currently cites this lemma (used_by is empty); it is bookkeeping that keeps the self-channel case from being a special hole when later identities quantify over all pairs of channels.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.