ququartX_basisKet
plain-language theorem explainer
The theorem states that the ququart shift operator X maps each standard basis ket |m⟩ to the shifted ket |m+1 mod 4⟩. Modelers of finite qudit systems in discrete recognition frameworks cite this when confirming operator actions on computational basis vectors. The verification reduces the functional equality to pointwise checks and resolves them by exhaustive case analysis over Fin 4 followed by direct simplification.
Claim. For each $m$ in the finite set of four indices, the shift operator $X$ satisfies $X |m⟩ = |m+1 mod 4⟩$, where $|m⟩$ denotes the standard basis vector that evaluates to 1 at index $m$ and 0 elsewhere.
background
QuquartState denotes the vector space of functions from Fin 4 to ℂ. The basis ket |m⟩ is the indicator function returning 1 precisely at index m. The operator ququartX is the linear map sending a state ψ to the state whose value at m equals ψ evaluated at prev4 m, where prev4 computes the predecessor index modulo 4 via (m.val + 3) % 4. Addition modulo 4 is the componentwise sum reduced by omega. These definitions appear in the CoupledRecognitionCores module, which assembles the basic shift and basis operators for four-level systems used in the Recognition Science foundation layer.
proof idea
The proof applies function extensionality to obtain pointwise equality. It then exhausts all combinations of the output index n and input index m via nested fin_cases tactics. Each of the sixteen cases simplifies directly using the definitions of ququartX, basisKet, prev4, and add4, confirming the required index shift.
why it matters
This identity verifies the concrete action of the canonical shift operator on basis states, anchoring the ququartX definition within the foundation module. It supplies the discrete shift convention required for subsequent operator constructions in CoupledRecognitionCores. No downstream theorems are listed as direct users, indicating the result functions as a primitive verification step rather than an intermediate lemma in a longer chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.