phaseCharacter
phaseCharacter supplies the complex phase factor for any pair of finite ququart configurations in the coupled-core model. Workers constructing tensor-Weyl monomials or proving their orthogonality and norms cite this factor when building operators on the N-site Hilbert space. The definition is realized directly as a product over the N sites of i raised to the product of the local indices.
claimFor natural number $N$ and configurations $b,s :$ Fin $N$ $→$ Fin $4$, the phase character is defined by $χ(b,s) = ∏_{x∈Fin N} i^{b(x)·s(x)}$ where $i=√{-1}$.
background
CoupledCoreIndex N is the finite configuration space Fin N → Fin 4, serving as the concrete carrier for N coupled ququart cores. Each site index runs over {0,1,2,3} and the whole space becomes the Hilbert space on which the tensor-Weyl monomial acts by phase multiplication and configuration shift. The module imports only Mathlib and builds directly on this configuration type; no further Recognition Science primitives such as J-cost or the phi-ladder appear locally.
proof idea
One-line definition that unfolds to the product over Fin N of Complex.I raised to the product of the two Fin 4 valuations at each site.
why it matters in Recognition Science
The definition supplies the phase that appears inside tensorWeylMonomial, which is the parent operator used by tensorWeylMonomial_basisKet, tensorWeylMonomial_basis_image_orthogonal, and tensorWeylMonomial_self_inner. These results establish that distinct displacement labels produce orthogonal images and that the operator has Hilbert-Schmidt norm equal to the dimension of the configuration space. The construction therefore closes the algebraic foundation for finite coupled recognition cores before any embedding into the larger phi-ladder or eight-tick structure.
scope and limits
- Does not extend the product to infinite N or continuous indices.
- Does not incorporate J-cost, defectDist, or phi-ladder arithmetic.
- Does not evaluate the phase for concrete numerical b and s beyond the product formula.
- Does not address measurement, entanglement, or dynamics on the coupled space.
formal statement (Lean)
128def phaseCharacter {N : ℕ} (b s : CoupledCoreIndex N) : ℂ :=
proof body
Definition body.
129 Finset.univ.prod fun x : Fin N => Complex.I ^ ((b x).val * (s x).val)
130
131/-- Shift a coupled-core configuration by a finite ququart displacement. -/