add4_eq_add4_iff_left
plain-language theorem explainer
add4_eq_add4_iff_left establishes left-cancellativity of addition modulo 4: for fixed s the equality add4 a s = add4 a' s holds precisely when a equals a'. Researchers building orthogonal bases for ququart operators in Recognition Science cite the result to separate distinct shift labels in local Weyl monomials. The argument is a one-line wrapper that invokes the exhaustive case-analysis core lemma.
Claim. Let $+_4$ denote addition in the cyclic group of order 4. Then for all $a,a',s$, $a +_4 s = a' +_4 s$ if and only if $a = a'$.
background
The CoupledRecognitionCores module equips the four-dimensional space Fin 4 with cyclic addition to realize discrete shift operators on ququart states. The function add4 implements this group law by add4 a b := (a.val + b.val) mod 4. The present theorem records the resulting left-cancellativity for any fixed second argument.
proof idea
One-line wrapper that applies add4_eq_add4_iff_left_core, which exhausts all 64 triples via fin_cases on a, a', s and decides the resulting equalities.
why it matters
The lemma is invoked inside localWeylMonomial_shift_orthogonal to obtain a = a' from operator equality, thereby forcing Hilbert-Schmidt orthogonality of distinct-shift monomials. It supplies a basic algebraic fact required for the modular realizations and spectral emergence constructions that sit above the eight-tick octave in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.