add4_eq_add4_iff_left_core
plain-language theorem explainer
Addition modulo 4 is left-injective for any fixed second argument. Researchers modeling ququart operators cite this when establishing label recovery in coupled cores. The proof exhausts all cases in the finite set of order 4 and decides the resulting equalities.
Claim. For any fixed $s$ in the cyclic group of order 4, $a + s = a' + s$ holds if and only if $a = a'$, where $+$ denotes addition modulo 4.
background
The CoupledRecognitionCores module models ququart states via indices in Fin 4. The operator add4 is defined by componentwise addition modulo 4 on representatives. Upstream, the canonical arithmetic object supplies the initial Peano structure that this finite realization specializes.
proof idea
The term proof invokes fin_cases successively on a, a', and s to split into all 64 combinations, after which the decide tactic verifies the biconditional in each case.
why it matters
It is used directly by the wrapper add4_eq_add4_iff_left and by the analogous statement for addedConfig. This supports uniqueness of displacement labels in the Recognition Science treatment of coupled recognition cores, feeding into higher-level operator definitions such as ququartX and ququartZ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.