add4_sub4_cancel_core
plain-language theorem explainer
Mod-4 addition undoes mod-4 subtraction on the cyclic group of order 4. Researchers building coupled recognition cores cite this identity to recover original configurations after displacement shifts. The proof exhausts all 16 pairs of elements in Fin 4 by case analysis and reduces each to reflexivity.
Claim. For all $m,a$ in the cyclic group of order 4, addition modulo 4 of $a$ and (subtraction modulo 4 of $m$ and $a$) equals $m$.
background
In CoupledRecognitionCores, addition modulo 4 is defined by add4(a,b) = (a.val + b.val) mod 4 and subtraction modulo 4 by sub4(a,b) = (a.val + (4 - b.val)) mod 4. These operations act on Fin 4 elements that label ququart basis states and displacements. The lemma belongs to the foundation layer that assembles coupled cores from primitive distinctions and simplicial ledger structures.
proof idea
The term proof applies exhaustive case analysis via fin_cases on both arguments, then reduces each of the 16 concrete cases to reflexivity.
why it matters
This cancellation supplies the key step in addedConfig_shiftedConfig, which recovers the original configuration after a shift, and in localWeylMonomial_basisKet, which tracks the action on basis kets. It closes a discrete inversion identity required by the eight-tick octave structure in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.