add4_sub4_cancel
plain-language theorem explainer
Mod-4 addition undoes mod-4 subtraction on the residues modulo 4. Workers on finite-state operator algebras or ququart representations would cite this inverse property when composing Weyl monomials. The proof reduces the statement to reflexivity by exhaustive enumeration of the four possible values for each argument.
Claim. For all $m,a$ in the cyclic group of order 4, addition modulo 4 applied to $a$ and the result of subtraction modulo 4 of $m$ by $a$ recovers $m$.
background
Addition modulo 4 is defined by lifting the integer sum and reducing modulo 4 on Fin 4; subtraction modulo 4 is defined by adding the complement to 4 before reducing. The CoupledRecognitionCores module develops these operations together with ququart states and basis kets to support coupled recognition operators. The lemma depends directly on the two definitions supplied in the same module and on the alias exported from the OperatorCore submodule.
proof idea
The term proof applies fin_cases to both arguments, generating sixteen exhaustive cases, each of which reduces immediately to reflexivity.
why it matters
The identity supplies the left-inverse property required for the local Weyl monomials that appear in the definitions of ququartX and ququartZ. It therefore closes a basic algebraic step inside the foundation layer that later supports the Recognition Composition Law in finite-dimensional settings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.