addedConfig
plain-language theorem explainer
This definition equips the finite configuration space of N coupled ququart cores with pointwise addition of a displacement label a to a base state s. Workers on tensor-Weyl monomials and coupled basis states cite it when recovering displacements or composing operators. The body is a direct pointwise wrapper around modular addition on Fin 4.
Claim. Let $C_N$ be the set of maps from a finite index set of size $N$ to the cyclic group of order 4. For displacement $a$ and base configuration $s$ in $C_N$, the added configuration is the map $xmapsto a(x)+s(x) mod 4$.
background
CoupledCoreIndex N is the finite-site configuration space of coupled ququart cores, concretely the set of functions Fin N to Fin 4. The operation add4 on Fin 4 is defined by componentwise sum reduced modulo 4 via (a.val + b.val) % 4. The module sits inside the foundation layer for coupled recognition cores and imports the eight-tick phase construction from upstream.
proof idea
One-line wrapper that applies add4 pointwise to the two input configurations.
why it matters
The definition supplies the group law used by addedConfig_shiftedConfig and shiftedConfig_addedConfig to recover the original configuration, and by tensorWeylMonomial_basisKet to produce phased shifted basis states. It therefore anchors the algebraic structure needed for the orthogonal-image theorems on tensor-Weyl monomials and for the eight-tick octave structure in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.