phaseCharacter_star_mul_self
plain-language theorem explainer
The phase character on coupled ququart cores is unimodular. Researchers constructing tensor-Weyl monomials in the Recognition Science foundation would cite this to normalize Hilbert-Schmidt inner products. The proof first reduces the squared modulus to a product of unit factors via the multiplicative property of normSq, then applies the identity relating norm squared to conjugate multiplication.
Claim. For any natural number $N$ and configurations $b,s$ in the space of coupled ququart cores (functions from a set of size $N$ to four states), if the phase character is defined by the product over sites of $i$ raised to the product of local indices, then the complex conjugate of this phase character satisfies $overline{phi(b,s)} cdot phi(b,s) = 1$.
background
CoupledCoreIndex N is the finite configuration space of N coupled ququart cores, realized as the function type Fin N to Fin 4. The phaseCharacter is the product over all sites x of Complex.I raised to the power (b(x).val * s(x).val). This construction lives in the CoupledRecognitionCores module, which supplies the algebraic carrier for finite collections of recognition units in a ququart basis.
proof idea
The tactic proof first unfolds phaseCharacter and rewrites the squared norm as a product over the finite index set. It then applies Finset.prod_eq_one together with the fact that normSq of any power of I equals 1. The second half invokes the general identity normSq(z) = conj(z) * z, substitutes the computed norm value of 1, and concludes by symmetry.
why it matters
This lemma supplies the unit-modulus fact required by the downstream theorem tensorWeylMonomial_self_inner, which equates the Hilbert-Schmidt norm squared of a tensor-Weyl monomial to the cardinality of the coupled-core space. It closes a normalization step inside the algebraic treatment of coupled recognition cores, consistent with the discrete structure of the phi-ladder and the eight-tick octave. No open scaffolding questions are touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.