addedConfig_shiftedConfig
plain-language theorem explainer
The result shows that applying a displacement shift followed by the matching addition recovers any configuration in the finite ququart core space. Workers on the Recognition Science monolith cite this to confirm that the shift and add operations are mutual inverses on the left. The proof reduces the claim pointwise via function extensionality to the mod-4 cancellation identity.
Claim. For all natural numbers $N$, and all maps $a, s : Fin N → Fin 4$, the pointwise mod-4 addition of the displacement $a$ to the pointwise mod-4 subtraction of $a$ from the configuration $s$ equals the original $s$.
background
CoupledCoreIndex N denotes the configuration space consisting of all functions from the finite set of N sites to the four ququart states. The operation addedConfig a s adds the displacement a to the configuration s by applying mod-4 addition at each site. shiftedConfig a s subtracts the displacement a from s using mod-4 subtraction at each site.
proof idea
The proof is a term-mode one-liner that first applies funext to reduce to pointwise equality, then invokes add4_sub4_cancel_core on the values at each site x, with m set to s x and a set to a x.
why it matters
This lemma confirms the invertibility needed for the displacement operations in the coupled core model. It is invoked by tensorWeylMonomial_basisKet to establish that the tensor-Weyl monomial maps a coupled basis ket to a phased version of the shifted ket. In the Recognition Science framework it closes a basic algebraic identity in the foundation layer before lifting to the full forcing chain and phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.