tensorWeylMonomial
plain-language theorem explainer
The tensor-Weyl monomial defines a linear operator on the Hilbert space of N coupled ququart cores by multiplying a state by a site-wise phase factor and shifting its configuration label. Researchers constructing operator bases for coupled recognition systems cite this when deriving orthogonality and norm identities. The definition supplies the explicit action and verifies linearity through direct simplification and ring arithmetic on the phase and shift maps.
Claim. For $a,b$ in the configuration space $(Fin 4)^N$, the operator $T_{a,b}$ on the Hilbert space of functions from configurations to $ℂ$ acts by $(T_{a,b} ψ)(s) = χ_b(s) ⋅ ψ(s - a)$, where $χ_b(s) = ∏_{x} i^{b_x s_x}$ is the phase character and $s - a$ is the componentwise subtraction in $Fin 4$.
background
In the CoupledRecognitionCores module the coupled-core space models N ququart systems. CoupledCoreIndex N is the finite configuration space Fin N → Fin 4. CoupledCoreSpace N is the Hilbert space of all functions from these configurations to ℂ, of dimension 4^N. phaseCharacter b s computes the complex phase ∏_x i^{(b x)⋅(s x)} over sites. shiftedConfig a s returns the configuration obtained by subtracting a from s at each site via sub4. These definitions sit immediately upstream of the monomial and supply the concrete carrier for the tensor-Weyl construction.
proof idea
The definition supplies the explicit action toFun ψ s := phaseCharacter b s * ψ (shiftedConfig a s). Linearity is verified by extensionality on the codomain, simplification of phaseCharacter, and ring arithmetic on ℂ for both additivity and scalar multiplication.
why it matters
This supplies the concrete displacement operators whose images and inner products are controlled by the downstream theorems tensorWeylMonomial_basisKet, tensorWeylMonomial_self_inner, tensorWeylMonomial_basis_image_orthogonal and tensorWeylMonomial_shift_orthogonal. In the Recognition Science framework it realizes the Weyl-Heisenberg generators needed for the coupled cores that appear after the J-uniqueness and phi-ladder steps of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.