tensorWeylMonomial_self_inner
plain-language theorem explainer
Tensor-Weyl monomials on the space of N coupled ququart cores satisfy that their Hilbert-Schmidt self-inner product equals the cardinality of the configuration space. Researchers constructing finite-dimensional operator bases or displacement operators in quantum information would cite the result for normalization. The tactic proof unfolds the inner-product definition, reduces each fixed-basis sum to one via the scaled ket inner product and phase unit-modulus lemma, then counts the basis vectors by finiteness.
Claim. Let $N$ be a natural number and let $a,b$ belong to the configuration space of $N$ coupled ququart cores. Let $T_{a,b}$ be the associated tensor-Weyl monomial operator. Then the Hilbert-Schmidt inner product of $T_{a,b}$ with itself equals the dimension $4^N$ of the configuration space.
background
CoupledCoreIndex N is the finite configuration space of N coupled ququart cores, concretely the set of all maps from N sites to four states. coupledBasisKet sends each configuration to the corresponding standard basis vector in the linear space of operators. coupledOperatorInner is the Hilbert-Schmidt pairing realized as the double sum over configurations s and t of the conjugate of the first operator applied to the basis ket at s, evaluated at t, times the second operator applied to the same ket at s evaluated at t.
proof idea
The proof unfolds coupledOperatorInner into the double sum. An auxiliary claim shows that for each fixed s the inner sum over t equals one: substitute the explicit action of the monomial on basis kets, apply scaled_coupledBasisKet_inner after rewriting with addedConfig, then invoke phaseCharacter_star_mul_self to obtain unit modulus. The outer sum therefore becomes a constant sum of ones whose value is the cardinality by Finset.sum_const and card_univ.
why it matters
The theorem supplies the squared norm for tensor-Weyl monomials inside the coupled recognition core algebra. It is referenced by the alias tensorWeylMonomial_self_inner in the OperatorCore module, which re-exports the result for downstream operator constructions. Within the Recognition Science foundation the normalization anchors the algebraic layer that supports the forcing chain from J-uniqueness through the eight-tick octave to three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.