sub4_add4_cancel
plain-language theorem explainer
Mod-4 subtraction reverses mod-4 addition on Fin 4. Researchers modeling ququart states or discrete operator cores in Recognition Science cite the cancellation when composing reversible transitions. The argument exhausts the 16 pairs of inputs by case analysis on both Fin 4 arguments and closes each by reflexivity.
Claim. For all $a,s$ in the cyclic group of order 4, subtraction modulo 4 applied after addition modulo 4 recovers the shift: $sub_4(add_4(a,s),a)=s$.
background
In CoupledRecognitionCores, add4 and sub4 are defined on Fin 4 by integer addition and subtraction followed by reduction modulo 4. add4 computes (a.val + b.val) % 4; sub4 computes (a.val + (4 - b.val)) % 4. These supply the arithmetic for ququart states, basis vectors, and the X/Z operators appearing as siblings in the same module.
proof idea
The proof applies fin_cases to a, then to s, producing 16 subgoals that are each discharged by rfl.
why it matters
The cancellation supplies the left-inverse property required for consistent state recovery in ququart representations. It supports the reversible transitions used by ququartX and ququartZ without introducing extra hypotheses. In the Recognition framework the result aligns with the discrete symmetries of the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.