tensorWeylMonomial_zero_zero
plain-language theorem explainer
The theorem establishes that the zero-index tensor Weyl monomial operator equals the identity linear map on the coupled-core space for any natural number N. Researchers building operator algebras in recognition foundations cite it as the trivial base case. The proof reduces the claim via extensionality on states and indices followed by direct simplification with the zero-phase and zero-shift lemmas.
Claim. For any natural number $N$, the tensor Weyl monomial operator with zero phase and zero shift indices equals the identity linear map on the space of coupled-core states: $M_{0,0} = id$.
background
The CoupledRecognitionCores module defines algebraic structures for coupled cores using phase characters and shifted configurations. The phase character at zero index evaluates to the constant function 1, while the zero-displacement shifted configuration returns the original index tuple unchanged. These rest on the identity automorphism from CostAlgebra and the identity homomorphism from ArithmeticOf, together with carrier-frequency definitions from the engineering modules.
proof idea
Extensionality equates the two linear maps on every state and index. Simplification then unfolds the monomial definition and applies the zero-phase character lemma together with the zero-shift configuration lemma to obtain the identity.
why it matters
This supplies the trivial case re-exported as an abbrev in the OperatorCore module. It anchors expansions of recognition operators in the foundation layer and supports the base of the forcing chain by confirming that the zero monomial acts as the identity automorphism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.