tensorWeylMonomial_basisKet
plain-language theorem explainer
The tensor-Weyl monomial operator maps a standard basis ket labeled by configuration s to a phase factor times the ket for the configuration obtained by adding displacement a, with the phase supplied by the character of b at the new configuration. Workers on finite ququart representations or coupled-core operators cite this identity when computing actions on basis states or verifying unitarity. The proof proceeds by extensionality on the output index followed by case split on whether the index matches the shifted configuration, using the mutual
Claim. For configurations $a,b,s$ in the space of maps from $N$ sites to four levels, the tensor-Weyl monomial $W(a,b)$ satisfies $W(a,b)|s⟩ = χ_b(a+s) |a+s⟩$, where $|⋅⟩$ denotes the standard basis vector of the coupled-core Hilbert space, addition is componentwise modulo 4, and $χ_b$ is the phase character associated to label $b$.
background
CoupledCoreIndex N is the finite configuration space consisting of all maps from N sites to the four ququart levels. The vector coupledBasisKet s is the indicator function that equals 1 precisely at configuration s. The map addedConfig a s performs componentwise addition modulo 4 of the two configurations, while shiftedConfig supplies the inverse operation. The phaseCharacter b c returns the multiplicative phase attached to label b at configuration c. This identity lives inside the module that equips the tensor product of N ququarts with the family of tensor-Weyl monomials that generalize the single-site Pauli operators. It rests on the inversion lemma addedConfig_shiftedConfig, which states that adding a displacement and then shifting by the same displacement recovers the original configuration.
proof idea
The proof applies extensionality to the output configuration t. It splits on the predicate t = addedConfig a s. In the affirmative case substitution and simplification with the definitions of tensorWeylMonomial and coupledBasisKet together with the inversion lemma yield the claimed phase times the target ket. In the complementary case the assumption that shiftedConfig a t equals s is shown to contradict the case hypothesis via the same inversion, after which simplification produces zero on both sides.
why it matters
The identity is invoked directly by tensorWeylMonomial_basis_image_orthogonal, which establishes that distinct displacement labels produce orthogonal images of any basis state, and by tensorWeylMonomial_self_inner, which shows that each monomial has Hilbert-Schmidt norm equal to the dimension of the carrier. It supplies the concrete action needed to verify that the tensor-Weyl operators realize a representation of the finite Weyl-Heisenberg group on the coupled-core space, consistent with the Recognition Science construction of finite-dimensional carriers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.