shiftedConfig_addedConfig
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not extend to infinite N or continuous configuration spaces.
- Does not incorporate phase factors or complex amplitudes.
- Does not address site-to-site interactions beyond the product structure.
- Does not prove uniqueness of the inverse beyond this explicit construction.
formal statement (Lean)
152theorem shiftedConfig_addedConfig {N : ℕ} (a s : CoupledCoreIndex N) :
153 shiftedConfig a (addedConfig a s) = s := by
proof body
Term-mode proof.
154 funext x
155 exact sub4_add4_cancel_core (a x) (s x)
156
157/-- Adding after shifting the same displacement returns the original configuration. -/