phaseCharacter_zero
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not treat non-zero displacements.
- Does not construct the full tensor-Weyl monomial.
- Does not address infinite-site or continuous limits.
Lean usage
ext ψ s; simp [tensorWeylMonomial, phaseCharacter_zero, shiftedConfig_zero]formal statement (Lean)
140lemma phaseCharacter_zero {N : ℕ} (s : CoupledCoreIndex N) :
141 phaseCharacter 0 s = 1 := by
proof body
Term-mode proof.
142 simp [phaseCharacter]
143
144/-- Zero displacement leaves a coupled-core configuration unchanged. -/