add4
plain-language theorem explainer
Addition modulo 4 on Fin 4 equips the cyclic group of order 4 with its natural operation for labeling shifts in ququart states. Researchers constructing Weyl monomials or displaced configurations in coupled recognition cores cite this definition when composing index displacements. The implementation is a direct modular reduction of integer addition, with the result bound verified by the omega tactic in the core definition.
Claim. For $a, b : Fin 4$, define $a +_4 b := (a.val + b.val) mod 4$ as an element of $Fin 4$.
background
The CoupledRecognitionCores module models ququart states via Fin 4 indices for coupled core spaces. Addition modulo 4 supplies the group law underlying shift operators such as ququartX and the displacement map addedConfig. The upstream definition in the imported CoupledRecognitionCores module computes the sum of representatives and reduces modulo 4, with the Fin membership proved by omega.
proof idea
This declaration is a one-line abbreviation that directly references the core definition of modular addition from CoupledRecognitionCores.
why it matters
The definition feeds thirteen downstream results, including add4_eq_add4_iff_left for left-operand recovery, add4_sub4_cancel for inverse cancellation, and addedConfig for configuration displacement. It also supports localWeylMonomial_basisKet and localWeylMonomial_phase_orthogonal. In the Recognition framework it supplies the discrete symmetry group for ququart representations that appear in the eight-tick octave construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.