add4
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.
claimFor $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 in Recognition Science
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.
scope and limits
- Does not define subtraction modulo 4.
- Does not extend the operation to moduli other than 4.
- Does not prove associativity or other group axioms.
Lean usage
def displaced {N} (a s : CoupledCoreIndex N) : CoupledCoreIndex N := addedConfig a sformal statement (Lean)
11abbrev add4 := IndisputableMonolith.Foundation.CoupledRecognitionCores.add4