tensorWeylMonomial_self_inner
plain-language theorem explainer
The tensor-Weyl monomial self-inner product equals the cardinality of the coupled core index set. Researchers normalizing operators or computing traces in the Recognition framework cite this identity. The proof is a direct delegation to the base theorem that unfolds the Hilbert-Schmidt inner product and sums over the finite index set.
Claim. For any natural number $N$ and indices $a,b$ in the coupled core index set, the Hilbert-Schmidt inner product of the tensor-Weyl monomial operator with itself equals the cardinality of the coupled core index set.
background
CoupledCoreIndex N is the finite set of indices labeling the coupled recognition cores for parameter N. tensorWeylMonomial a b builds an operator on the tensor product space from a pair of such indices. coupledOperatorInner is the Hilbert-Schmidt inner product on these operators. The abbreviation sits in the OperatorCore submodule, which imports the core coupled-core constructions to separate operator-level statements from the base recognition definitions.
proof idea
This is a one-line wrapper that delegates directly to the theorem tensorWeylMonomial_self_inner in the CoupledRecognitionCores module.
why it matters
The identity supplies the squared norm required for normalization of monomial operators inside the Recognition Science operator algebra. It supports trace and inner-product calculations that appear in the coupled-core layer of the forcing chain. The result feeds downstream operator identities within the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.