tensorWeylMonomial
The tensor-Weyl monomial defines the linear operator on the coupled-core space that implements a combined phase and shift action labeled by two indices a and b. Quantum information theorists modeling finite Weyl systems or recognition algebras would reference this when building operator bases. The declaration consists of a single-line abbreviation that forwards to the concrete implementation in the CoupledRecognitionCores module.
claimFor a natural number $N$, and indices $a,b$ in the coupled-core index set, the tensor-Weyl monomial is the linear map $T$ on the coupled-core space satisfying $(T_{a,b}ψ)(s) = χ_b(s) ⋅ ψ(σ_a(s))$, where $χ_b$ is the phase character and $σ_a$ the shifted configuration map.
background
In the CoupledRecognitionCores module the coupled-core carrier is the finite-dimensional Hilbert space whose orthonormal basis is indexed by CoupledCoreIndex N. The tensor-Weyl monomial is built from the phaseCharacter function, which supplies a complex phase factor, and the shiftedConfig map, which translates the configuration index by a. This definition sits inside the foundation layer that imports the core coupled recognition structures. The upstream result supplies the explicit toFun clause together with the linearity proof via map_add'.
proof idea
The declaration is a one-line wrapper that applies the tensorWeylMonomial definition from the CoupledRecognitionCores module by specializing the parameter N.
why it matters in Recognition Science
This definition is invoked by six downstream results, including the theorem that the monomial maps a basis ket to a phased shifted ket, the self-inner-product theorem showing its Hilbert-Schmidt norm equals the dimension, and orthogonality statements for distinct labels. It thereby supplies the concrete operators needed to realize the Weyl relations in the coupled-core setting of the Recognition Science framework.
scope and limits
- Does not derive the phase character or shifted configuration from more primitive axioms.
- Does not prove linearity beyond the imported definition.
- Does not specialize to particular values of N.
- Does not connect to the J-cost or phi-ladder structures.
formal statement (Lean)
16abbrev tensorWeylMonomial {N : ℕ} :=
proof body
Definition body.
17 IndisputableMonolith.Foundation.CoupledRecognitionCores.tensorWeylMonomial (N := N)