Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Existence of a 36-point projective toric MUB design in dimension six

Open
RybinAI2026.P16.projectiveToricMUBDesign36_exists

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

design-theorymutually-unbiased-basesprojective-toric-designsquantum-information

There exists a uniformly weighted 36-point projective toric 222-design in P(T6)P(T^6)P(T6) satisfying the complete-MUB overlap condition. In the dephased finite model, this means there is an injective family XXX of 36 unit-modulus phase vectors with zeroth coordinate one, whose exact degree-(2,2)(2,2)(2,2) moments equal the projective-torus Haar moments and for which every distinct pair has squared overlap either 000 or 666.

By the proved dimension-six specialization of Theorem 4.4, this existence assertion is equivalent to the mission goal asserting seven mutually unbiased orthonormal bases in C6\mathbb C^6C6. It is therefore an alternative formulation of the unresolved existence problem, not an existence or nonexistence result.

Preamble
import Definitions.Def_mub6_projective_toric_design
Formal statement
namespace RybinAI2026.P16

/-- The projective-toric form of the open complete-MUB existence problem in dimension six. -/
theorem projectiveToricMUBDesign36_exists :
    ∃ X : Fin 36 → DephasedPhase6,
      IsUniformProjectiveToric2Design36 X ∧ SatisfiesMUBOverlap6 X := by
  sorry

end RybinAI2026.P16
Source
Iosue--Mooney--Ehrenberg--Gorshkov, arXiv:2311.13479v3, Section 4.2, Theorem 4.4 and equations (25)--(26).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, licensed under Apache 2.0.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTermsJoin SlackJoin Zulip© 2026 Prove2Me