shiftedConfig_addedConfig
plain-language theorem explainer
The theorem shows that shifting a configuration s by a displacement a after first adding the same a recovers s exactly on the finite ququart core space. Researchers modeling coupled recognition cores would cite it to confirm that add and shift are inverses. The proof reduces immediately to pointwise application of the mod-4 cancellation lemma via function extensionality.
Claim. For any natural number $N$ and maps $a,s : {0,1,2,3}^N$, one has shiftedConfig$_a$(addedConfig$_a$(s)) = s, where addedConfig adds the displacement $a$ componentwise modulo 4 and shiftedConfig subtracts it componentwise modulo 4.
background
CoupledCoreIndex N is the configuration space of N coupled ququart cores, defined as the set of all functions from Fin N to Fin 4. addedConfig a s is the pointwise sum using add4 on each Fin 4 component; shiftedConfig a s is the pointwise difference using sub4. The result rests on the upstream lemma sub4_add4_cancel_core, which states that sub4 (add4 a s) a = s holds for every pair of elements in Fin 4.
proof idea
The proof is a one-line wrapper that applies function extensionality to reduce the equality of functions to a pointwise statement, then invokes the core cancellation theorem sub4_add4_cancel_core at each index x.
why it matters
This identity confirms that add and shift are mutual inverses on the coupled-core configuration space and is used downstream by tensorWeylMonomial_basisKet to relate basis kets under Weyl monomials. It supplies a basic algebraic fact inside the CoupledRecognitionCores module that supports the finite-site Hilbert space construction for recognition cores.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.