tensorWeylMonomial_zero_zero
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish properties for non-zero indices.
- Does not derive any commutation relations or spectra.
- Does not connect the identity to physical constants or ladders.
formal statement (Lean)
21abbrev tensorWeylMonomial_zero_zero {N : ℕ} :=
proof body
Definition body.
22 IndisputableMonolith.Foundation.CoupledRecognitionCores.tensorWeylMonomial_zero_zero (N := N)