Explicit fiducial vector on ZMod 2

Proved

WeylHeisenbergSIC.fiducial_d2_explicit

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

linear-algebraquantum-informationqubitsic-povm

An explicit qubit fiducial vector $\psi : \mathbb{Z}/2\mathbb{Z} \to \mathbb{C}$ for the Weyl--Heisenberg group is given by setting the amplitude ratios to match the vertices of a regular tetrahedron inscribed in the Bloch sphere:

\psi(0) = \cos(\theta/2), \quad \psi(1) = e^{i\pi/4} \sin(\theta/2)

where $\cos\theta = 1/\sqrt{3}$ . Its norm is $1$ and its overlaps with all nonidentity displacements satisfy $|\langle \psi, D(a,b) \psi \rangle|^2 = 1/3$ .

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_d2_explicit :
    ∃ ψ : ZMod 2 → ℂ,
      (∑ x : ZMod 2, Complex.normSq (ψ x)) = 1 ∧
      ∀ a b : ZMod 2, (a,b) ≠ (0,0) →
        Complex.normSq (∑ x : ZMod 2, star (ψ x) *
          (ZMod.stdAddChar (b*x) * ψ (x+a))) = (2+1 : ℝ)⁻¹ := by sorry

Source

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

View graph