addedConfig
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not extend to infinite or continuous index sets.
- Does not embed phase factors or complex multipliers.
- Does not claim commutativity or associativity beyond the obvious properties of mod-4 addition.
- Does not address measurement or dynamics on the resulting states.
formal statement (Lean)
136def addedConfig {N : ℕ} (a s : CoupledCoreIndex N) : CoupledCoreIndex N :=
proof body
Definition body.
137 fun x => add4 (a x) (s x)
138
139/-- Zero phase character. -/