diff
plain-language theorem explainer
Discrete first difference along one binary distinction channel: for an integer function on n-bit configurations, flip channel i to true versus false and subtract, holding every other channel fixed. Cited by anyone proving channel independence, mixed second differences, or the multi-distinction cell complex (∂² = 0). Pure definition by pointwise configuration update; no proof obligations.
Claim. Fix $n\in\mathbb{N}$, a channel index $i\in\{0,\ldots,n-1\}$, and an integer-valued function $f$ on configurations of $n$ independent binary distinctions (maps $\{0,\ldots,n-1\}\to\{\mathrm{true},\mathrm{false}\}$). The difference of $f$ along channel $i$ is the function $(\partial_i f)(v)=f(v|_{i\mapsto\mathrm{true}})-f(v|_{i\mapsto\mathrm{false}})$.
background
In the primitive recognition calculus, a configuration of $n$ independent binary distinctions is simply a map from channel indices to sides: $\mathrm{Config},n := \mathrm{Fin},n \to \mathrm{Bool}$. Each coordinate is one on/off distinction; there is no continuous ambient space yet.
The local module builds multi-distinction geometry from that discrete cube: first differences along channels, then mixed second differences, then an oriented 2-face complex with $\partial^2=0$. Upstream, independence of claims and of RS axes supplies the conceptual warrant that distinct channels are separate coordinate directions, not coupled primitives.
The difference operator is the discrete analogue of a partial derivative: it isolates the jump of an integer observable when one named distinction flips, with all other channels held fixed by Function.update.
proof idea
One-line definition, not a theorem. The body is the lambda $v \mapsto f(v[i\mapsto\mathrm{true}]) - f(v[i\mapsto\mathrm{false}])$, using Mathlib configuration update. No lemmas are applied; well-typedness is immediate from the Config abbreviation and integer subtraction.
why it matters
This is the atomic operator of multi-distinction geometry. Downstream, channel independence is exactly commutativity of mixed second differences (diff_comm: $\partial_i\partial_j f = \partial_j\partial_i f$), and the Phase 6 headline multi_distinction_geometry packages that commutativity with boundary-squared-zero on every oriented 2-face of the $n$-cube: geometry (independent coordinates plus closed boundaries) is the algebra of several independent distinctions, not an extra posit.
It also feeds PRC one-primitive comparison (actJudgment_diff, comparison-is-derived), the d'Alembert entanglement-gate mixed difference identity, and is referenced from the C-010 cosmological-constant certificate chain. In the forcing picture it is the discrete skeleton behind independent channels before continuous J-cost and the eight-tick octave enter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.