Construct a complete dimension-six MUB from a 36-point toric design

Proved

RybinAI2026.P16.projectiveToricDesign36_to_completeMUB6

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

design-theorymutually-unbiased-bases

If a uniformly weighted 36-point projective toric $2$ -design in $P(T^6)$ satisfies Equation (25), then its flat phase vectors, together with the six computational-basis vectors, form seven mutually unbiased orthonormal bases. This is the “if” direction of Theorem 4.4, specialized to dimension six; it is a conditional construction, not an existence result.

Preamble

import Definitions.Def_mub6_projective_toric_design

Formal statement

namespace RybinAI2026.P16

theorem projectiveToricDesign36_to_completeMUB6 :
    (∃ X : Fin 36 → DephasedPhase6,
      IsUniformProjectiveToric2Design36 X ∧ SatisfiesMUBOverlap6 X) →
        ∃ B : Fin 7 → Matrix (Fin 6) (Fin 6) ℂ, IsCompleteMUB6 B := by sorry

end RybinAI2026.P16

Source

arXiv:2311.13479v3, Section 4.2, Theorem 4.4, proof sketch and Eq. (26).

View graph