localOperatorInner
localOperatorInner defines the Hilbert-Schmidt inner product on linear operators over the four-dimensional ququart space. Workers proving orthogonality and norm relations for local Weyl monomials cite this pairing to obtain explicit inner-product values. The definition expands directly to a double finite sum over the standard basis vectors with no auxiliary lemmas.
claimFor linear maps $A, B$ from the space of functions $Fin 4 to ℂ$ to itself, the pairing is $⟨A, B⟩ := ∑_{s=0}^3 ∑_{t=0}^3 conj((A |s⟩)_t) ⋅ (B |s⟩)_t$, where $|s⟩$ is the standard basis vector that equals 1 at index $s$ and 0 elsewhere.
background
QuquartState is the carrier type Fin 4 → ℂ that models the local quarter-turn core. basisKet supplies the standard orthonormal basis vectors |m⟩, each defined by the Kronecker delta on this finite index set. The definition resides in the CoupledRecognitionCores module, which assembles single-core operator structures ahead of the Weyl monomial family.
proof idea
The declaration is a direct double summation over Fin 4. For each basis vector basisKet s the images under A and B are formed, the t-components are extracted, the first is conjugated, and the products are accumulated. No lemmas or tactics intervene; the expression is the explicit Hilbert-Schmidt product in the chosen basis.
why it matters in Recognition Science
This pairing is invoked by the four downstream theorems localWeylMonomial_self_inner, localWeylMonomial_phase_orthogonal, localWeylMonomial_shift_orthogonal and localWeylMonomial_orthogonal_of_ne. It supplies the concrete inner-product structure required to establish that distinct local Weyl monomials are orthogonal and that each has squared norm 4, thereby supporting the local operator algebra inside the Recognition framework's single-core layer.
scope and limits
- Does not extend to operators on spaces whose dimension differs from 4.
- Does not incorporate any weighting, trace factor, or normalization.
- Does not apply to non-linear maps or infinite-dimensional Hilbert spaces.
- Does not encode forcing relations, J-cost, or phi-ladder structure.
formal statement (Lean)
261def localOperatorInner (A B : QuquartState →ₗ[ℂ] QuquartState) : ℂ :=
proof body
Definition body.
262 ∑ s : Fin 4, ∑ t : Fin 4, star (A (basisKet s) t) * B (basisKet s) t
263
264/-- The standard ququart basis is orthonormal for the explicit finite sum. -/