phaseCharacter_zero
plain-language theorem explainer
The phase character of the zero displacement on any coupled ququart configuration equals unity. Researchers building tensor-Weyl monomials in the Recognition Science foundation cite this to reduce the identity case. The proof is a direct simplification of the product definition when the first configuration argument is zero.
Claim. For any natural number $N$ and any configuration $s : (Fin N) → (Fin 4)$, the phase character of the zero configuration and $s$ equals $1$, where the phase character is the product over sites $x$ of $i$ raised to the product of the ququart values of the two configurations at $x$.
background
CoupledCoreIndex N is the type Fin N → Fin 4, the finite-site configuration space of coupled ququart cores that serves as the concrete Hilbert carrier. The phaseCharacter function maps a pair of such configurations to a complex number via the product over all sites of i to the power of the product of their ququart values. This lemma sits in the CoupledRecognitionCores module that assembles the basic operators on these carriers.
proof idea
The proof is a one-line wrapper that applies the definition of phaseCharacter and reduces the product to 1 when the displacement configuration is identically zero.
why it matters
This lemma supplies the zero case needed by tensorWeylMonomial_zero_zero, which establishes that the trivial Weyl monomial acts as the identity operator on the coupled-core space. It closes the base case in the phase-character construction for tensor-Weyl expansions inside the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.