shiftedConfig_zero
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish the action of nonzero displacements.
- Does not extend the result to infinite $N$.
- Does not address the continuous limit of the ququart system.
- Does not connect to the J-cost or phi-ladder constructions.
Lean usage
simp [shiftedConfig_zero]formal statement (Lean)
145lemma shiftedConfig_zero {N : ℕ} (s : CoupledCoreIndex N) :
146 shiftedConfig 0 s = s := by
proof body
Term-mode proof.
147 funext x
148 apply Fin.ext
149 simp [shiftedConfig, sub4]
150
151/-- Shifting after adding the same displacement returns the original configuration. -/