tensorWeylMonomial_zero_zero
plain-language theorem explainer
The declaration supplies the zero-zero case of the tensor Weyl monomial as the identity linear map on the coupled-core space. Researchers building operator algebras or monomial expansions in Recognition Science cite it for the trivial element. It is realized as a one-line abbreviation that directly re-exports the corresponding theorem from the CoupledRecognitionCores module.
Claim. For any natural number $N$, the tensor Weyl monomial at indices zero and zero equals the identity linear map on the coupled-core carrier space.
background
The CoupledRecognitionCores setting equips the ququart state space with Weyl monomials built from phase characters and shifted configurations. The upstream theorem states that tensorWeylMonomial (N := N) 0 0 equals LinearMap.id, proved by extensionality and simplification with phaseCharacter_zero and shiftedConfig_zero. The present abbreviation re-exports that result into the OperatorCore module for local use.
proof idea
One-line wrapper that applies the theorem tensorWeylMonomial_zero_zero from CoupledRecognitionCores by instantiating the parameter N.
why it matters
This supplies the identity base case for tensor Weyl monomials, feeding constructions that rely on the trivial monomial in operator cores. It aligns with the Recognition framework's use of linear maps on state spaces and supports expansions that begin from the identity element.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.