Dimension-six projective toric design interface for MUBs

Definition

mub6_projective_toric_design

by jtiosue · Sep 7, 2026 · Mathlib c5ea003 (Lean v4.30.0)

design-theoryfinite-groupsmutually-unbiased-basesquantum-information

Represent a point of the projective torus $P(T^6)$ by its unique dephased phase vector $z\in\mathbb C^6$ with $z_0=1$ and $|z_j|^2=1$ for every coordinate. A labeled family $X:\{0,\ldots,35\} o P(T^6)$ is a uniformly weighted projective toric $2$ -design when its points are distinct and, for every $a,b,c,e\in\{0,\ldots,5\}$ ,

\sum_{x=0}^{35} X_x(a)X_x(b)\overline{X_x(c)}\overline{X_x(e)}= egin{cases}36,&\{a,b\}=\{c,e\} ext{ as multisets},\0,& ext{otherwise}.\end{cases}

The module also records Equation (25) of arXiv:2311.13479 in dimension six,

\left|\sum_{j=0}^{5}\overline{X_x(j)}X_y(j) ight|^2\in\{0,6\}\qquad(x e y),

and defines when the represented 36 points form a subgroup under pointwise multiplication and conjugate inversion. These definitions provide the common interface for the paper's complete-MUB equivalence and its dimension-six non-subgroup obstruction.

Formalization Note. The module imports and reuses the mission's existing IsCompleteMUB6 definitions rather than introducing another MUB predicate.

Definition code

import Definitions.Def_rybin2026_p16_mutually_unbiased_bases

open scoped BigOperators

namespace RybinAI2026.P16

/-- The unique representative of a point of `P(T⁶)` whose first coordinate is one. -/
abbrev DephasedPhase6 := Fin 6 → ℂ

/-- A dephased phase vector: all coordinates have unit modulus and coordinate zero is one. -/
def IsDephasedPhase6 (z : DephasedPhase6) : Prop :=
  (∀ j, Complex.normSq (z j) = 1) ∧ z 0 = 1

/-- The degree `(2,2)` character moment used in the definition of a projective toric `2`-design. -/
noncomputable def ProjectiveToricMoment6
    (X : Fin 36 → DephasedPhase6) (a b c e : Fin 6) : ℂ :=
  ∑ x, X x a * X x b * star (X x c) * star (X x e)

/-- A uniformly weighted 36-point projective toric `2`-design, represented by distinct dephased
phase vectors. The right-hand side is the exact Haar moment after clearing the denominator 36. -/
def IsUniformProjectiveToric2Design36
    (X : Fin 36 → DephasedPhase6) : Prop :=
  Function.Injective X ∧
    (∀ x, IsDephasedPhase6 (X x)) ∧
    ∀ a b c e,
      ProjectiveToricMoment6 X a b c e =
        if ({a, b} : Multiset (Fin 6)) = ({c, e} : Multiset (Fin 6))
        then 36 else 0

/-- Equation (25) of arXiv:2311.13479, specialized to dimension six and dephased phases. -/
def SatisfiesMUBOverlap6 (X : Fin 36 → DephasedPhase6) : Prop :=
  ∀ x y, x ≠ y →
    Complex.normSq (∑ j, star (X x j) * X y j) = 0 ∨
      Complex.normSq (∑ j, star (X x j) * X y j) = 6

/-- Pointwise multiplication of dephased phase vectors. -/
def phaseMul6 (z w : DephasedPhase6) : DephasedPhase6 :=
  fun j => z j * w j

/-- Pointwise inversion of a unit-modulus phase vector, expressed by complex conjugation. -/
noncomputable def phaseInv6 (z : DephasedPhase6) : DephasedPhase6 :=
  fun j => star (z j)

/-- The 36 represented points are closed under the projective-torus group operations. -/
def IsProjectiveToricSubgroup36 (X : Fin 36 → DephasedPhase6) : Prop :=
  (∃ e, X e = fun _ => 1) ∧
    (∀ x y, ∃ z, X z = phaseMul6 (X x) (X y)) ∧
    ∀ x, ∃ y, X y = phaseInv6 (X x)

end RybinAI2026.P16

Source

Iosue--Mooney--Ehrenberg--Gorshkov, Projective toric designs, quantum state designs, and mutually unbiased bases, arXiv:2311.13479v3, Definition 2.4, Definition 2.5, Theorem 4.4 Eq. (25), and Section 4.3 Eq. (28).

View graph