localWeylMonomial
plain-language theorem explainer
The definition supplies the explicit action of the local Weyl monomial operator labeled by shift a and phase b on the ququart carrier space. Researchers constructing finite-dimensional Weyl-Heisenberg algebras or discrete operator bases for recognition cores would cite it as the concrete single-core building block. The map is realized by a phase multiplication followed by modular shift, with linearity verified by direct ring simplification on components.
Claim. Let $H$ be the space of functions from the cyclic group of order 4 to the complex numbers. For $a,b$ in that group, the linear operator $W_{a,b}:H→H$ acts by $(W_{a,b}ψ)(s)=i^{b·s}ψ(s-a)$, where subtraction is taken modulo 4 and $i=√-1$.
background
QuquartState is the carrier for a single quarter-turn core, realized concretely as the vector space of functions from Fin 4 to ℂ. The auxiliary sub4 implements subtraction in this cyclic group of order 4 and satisfies the cancellation identity that addition and subtraction are mutual inverses. The definition sits inside the CoupledRecognitionCores module, which assembles the local operator algebra on these discrete cores as the foundation layer for the Recognition Science framework.
proof idea
The definition is given directly by the toFun clause. Linearity is established in two separate blocks: map_add' reduces componentwise to ring arithmetic on ℂ, and map_smul' follows by the identical simplification.
why it matters
This supplies the concrete realization of the local Weyl monomials that feed the downstream theorems localWeylMonomial_basisKet, localWeylMonomial_self_inner, localWeylMonomial_orthogonal_of_ne and their siblings. Those results establish that the family is orthogonal with Hilbert-Schmidt norm squared equal to 4, furnishing the discrete position-momentum shifts required for the operator core. The construction aligns with the eight-tick octave structure in the forcing chain by using a period-4 carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.