shiftedConfig_zero
plain-language theorem explainer
Zero displacement leaves any coupled ququart configuration unchanged. Workers on the Recognition Science operator algebra cite this identity when reducing tensor Weyl monomials to the identity map. The short proof applies function extensionality, extends the finite index equality, and simplifies directly via the definitions of shiftedConfig and sub4.
Claim. Let $N$ be a natural number and let $s$ be any map from the finite set of $N$ sites to the four ququart values. The configuration obtained by shifting $s$ by the zero displacement vector equals $s$.
background
CoupledCoreIndex $N$ denotes the type of all functions from Fin $N$ to Fin 4, the concrete carrier for the state space of $N$ coupled recognition cores. The operation shiftedConfig $a$ $s$ produces the new configuration whose value at each site $x$ is sub4 $(s x)$ $(a x)$, where sub4 implements modular subtraction modulo 4. The upstream definition of sub4 is the map sending $a,b$ to the representative of $a.val + (4 - b.val)$ modulo 4. This zero-shift lemma supplies the identity case for the displacement action used throughout the coupled-core operator algebra.
proof idea
The term proof first invokes funext to reduce the function equality to a pointwise statement, then applies Fin.ext to reduce further to equality of the underlying natural numbers, and finally calls simp on the definitions of shiftedConfig and sub4. The simplifier immediately yields the required identity when the displacement component is zero.
why it matters
The lemma is invoked inside the proof of tensorWeylMonomial_zero_zero, which establishes that the trivial Weyl monomial equals the identity linear map on the coupled-core Hilbert space. It therefore closes the zero-displacement case in the foundation layer that constructs the discrete operator algebra before any lift to the continuous forcing chain or the J-cost structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.