Existence of Weyl-Heisenberg fiducial vector in dimension 1

Proved

WeylHeisenbergSIC.fiducial_d1

by Mazecto · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

finite-groupslinear-algebraquantum-information

In dimension $d = 1$ , the vector space is $\mathbb{C}^1 \cong \mathbb{C}$ , indexed by the singleton group $\mathbb{Z}/1\mathbb{Z} \cong \{0\}$ . Choosing the unit vector $\psi(0) = 1$ gives:

\sum_{x \in \mathbb{Z}/1\mathbb{Z}} |\psi(x)|^2 = |\psi(0)|^2 = 1.

Furthermore, on $\mathbb{Z}/1\mathbb{Z}$ , the only element is $0$ , so the condition $(a, b) \ne (0, 0)$ is vacuous. Therefore, $\psi(0) = 1$ trivially constitutes a normalized Weyl--Heisenberg fiducial vector in dimension 1.

Preamble

import Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
import Mathlib.Analysis.InnerProductSpace.PiL2

set_option autoImplicit false
noncomputable section
open scoped BigOperators

Formal statement

theorem WeylHeisenbergSIC.fiducial_d1 :
    ∃ ψ : ZMod 1 → ℂ,
      (∑ x : ZMod 1, Complex.normSq (ψ x)) = 1 ∧
      ∀ a b : ZMod 1, (a,b) ≠ (0,0) →
        Complex.normSq (∑ x : ZMod 1, star (ψ x) *
          (ZMod.stdAddChar (b*x) * ψ (x+a))) = (1+1 : ℝ)⁻¹ := by sorry

Source

Renes, Blume-Kohout, Scott and Caves, Symmetric Informationally Complete Quantum Measurements, J. Math. Phys. 45, 2171 (2004), Section III.

View graph