shiftedConfig
plain-language theorem explainer
shiftedConfig defines the pointwise mod-4 subtraction of a displacement a from a configuration s on the finite set of N coupled ququart cores. Researchers building tensor-Weyl monomials on the coupled-core space cite this when defining shift actions on basis states. The definition is realized directly as the lambda expression that applies sub4 at each site.
Claim. For positive integer $N$ and maps $a,s :$ Fin $N$ to Fin $4$, the shifted map is given by $xmapsto s(x)-a(x) mod 4$.
background
CoupledCoreIndex $N$ is the set of functions Fin $N$ to Fin $4$, serving as the configuration space for $N$ coupled ququart cores. sub4 is the mod-4 subtraction on Fin $4$ that satisfies the cancellation identities sub4_add4_cancel_core and add4_sub4_cancel_core. The module equips this space with group operations under mod-4 arithmetic to support Weyl-type operators on the finite lattice.
proof idea
One-line wrapper that returns the function sending each site $x$ to sub4 applied to the values of $s$ and $a$ at $x$.
why it matters
This supplies the inverse to addedConfig, enabling the mutual-inverse theorems addedConfig_shiftedConfig and shiftedConfig_addedConfig. It is invoked inside tensorWeylMonomial to realize the shift action on CoupledCoreSpace. The construction supports displacement operators on the finite ququart lattice within the Recognition Science framework for coupled cores.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.