sub4_add4_cancel_core
plain-language theorem explainer
Mod-4 subtraction undoes mod-4 addition on Fin 4, recovering the original shift after an add4 followed by sub4. Researchers modeling ququart states or Weyl operators in the coupled cores would cite this for configuration recovery. The proof exhausts the 16 cases by fin_cases on both arguments and closes each by reflexivity.
Claim. For all $a,s$ in the cyclic group of order 4, subtraction modulo 4 after addition modulo 4 recovers the shift: sub$_4$(add$_4$(a,s),a) = s.
background
The CoupledRecognitionCores module defines addition and subtraction on Fin 4 to handle discrete shifts for ququart states and basis kets. add4 is the map (a.val + b.val) mod 4; sub4 is the map (a.val + (4 - b.val)) mod 4. These operations appear in the operator core layer and support the local Weyl monomial construction. The theorem depends directly on the two sibling definitions add4 and sub4.
proof idea
The term proof applies fin_cases to a and then to s, producing 16 exhaustive cases. Each case reduces the modular expressions to concrete integers whose equality is settled by rfl.
why it matters
The result supplies the cancellation step used by shiftedConfig_addedConfig to prove that shifting after adding the same displacement returns the original configuration, and by localWeylMonomial_basisKet to track phased basis kets. It closes a basic algebraic identity required for the foundation layer that later feeds the eight-tick octave structures in the Recognition Science chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.