localWeylMonomial
plain-language theorem explainer
localWeylMonomial supplies a module-local alias for the single-core ququart Weyl monomial operator that maps a state ψ at label s to i to the power b times s, times ψ shifted by a. Researchers constructing finite-dimensional Weyl-Heisenberg bases or coupled ququart models cite the alias when assembling local operator families for orthogonality and tensor-product arguments. The implementation is a direct abbreviation of the core linear-map definition supplied in the CoupledRecognitionCores module.
Claim. For integers a, b in {0,1,2,3}, the operator W_{a,b} acts on a ququart state ψ by (W_{a,b} ψ)(s) = i^{b s} ψ(s - a) where s ranges over Z/4Z.
background
The single-core carrier is the four-dimensional complex vector space QuquartState whose orthonormal basis is indexed by Fin 4. The upstream definition states that the local ququart Weyl monomial X^a Z^b is written directly on the single-core carrier and gives the explicit action toFun := fun ψ s => Complex.I ^ (b.val * s.val) * ψ (sub4 s a), together with the additivity check. This separates the phase factor generated by Z^b from the shift generated by X^a, preparing the ground for later Hilbert-Schmidt inner-product calculations.
proof idea
The declaration is a one-line abbreviation that directly re-exports the definition from the CoupledRecognitionCores module without further computation or proof obligations.
why it matters
The alias anchors the family of local Weyl monomials whose basis action, phase orthogonality, shift orthogonality and self-inner-product equal to 4 are proved in the downstream theorems localWeylMonomial_basisKet, localWeylMonomial_phase_orthogonal, localWeylMonomial_shift_orthogonal and localWeylMonomial_self_inner. These results in turn support the tensorWeylMonomial construction and the coupled-core relations that realize the Recognition Composition Law at the operator level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.