tensorWeylMonomial_basis_image_orthogonal
plain-language theorem explainer
Distinct displacement labels a and a' map any fixed coupled basis state s to orthogonal vectors under the tensor-Weyl monomials. Researchers building the coupled-core Hilbert space in the Recognition Science foundation cite this when proving operator-level orthogonality. The tactic proof rewrites the monomials via the basisKet expansion, derives index inequality from the addedConfig equivalence, and reduces the sum with the scaled inner-product lemma.
Claim. Let $a,a'$ be distinct maps from Fin $N$ to Fin 4. For arbitrary maps $b,b',s$ of the same type, the inner product of the images of the standard basis vector at $s$ under the tensor-Weyl monomials labeled $(a,b)$ and $(a',b')$ vanishes: $∑_t$ conjugate of the value at $t$ of the first image times the value at $t$ of the second image equals zero.
background
CoupledCoreIndex N is the space of all maps Fin N → Fin 4, serving as the configuration space for N coupled ququart cores. The coupledBasisKet at s is the vector equal to 1 at configuration s and 0 elsewhere. addedConfig a s performs pointwise addition (via add4) of displacement a to configuration s. phaseCharacter b s returns the product over sites of i raised to the product of the two Fin 4 values. scaled_coupledBasisKet_inner states that the inner product of two scaled basis vectors equals the product of the scalars times 1 if the indices agree and 0 otherwise.
proof idea
The proof rewrites both tensorWeylMonomial applications with the basisKet lemma. It establishes addedConfig a s ≠ addedConfig a' s by applying the equivalence theorem addedConfig_eq_addedConfig_iff_left and contraposing. It then feeds the resulting phases phaseCharacter b (addedConfig a s) and phaseCharacter b' (addedConfig a' s) into scaled_coupledBasisKet_inner and simplifies with the index inequality via simpa.
why it matters
The result supplies the fixed-s orthogonality used to prove the full Hilbert-Schmidt orthogonality of distinct tensor-Weyl monomials in the downstream theorem tensorWeylMonomial_shift_orthogonal. It closes a step in the construction of orthogonal operator bases inside the CoupledRecognitionCores module, supporting the discrete Hilbert space that underlies the J-uniqueness and phi-ladder steps of the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.