Translation preserves 36-point toric design and MUB overlap data

Proved

RybinAI2026.P16.projectiveToricData36_translate

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

design-theorymutually-unbiased-bases

Translation by any projective-torus phase preserves both the uniformly weighted 36-point projective toric $2$ -design equations and Equation (25). Character moments acquire a common character factor, which is one on the nonzero Haar moments and irrelevant on zero moments; in pairwise overlaps the translating phase cancels exactly.

Preamble

import Definitions.Def_mub6_projective_toric_translation

Formal statement

namespace RybinAI2026.P16

theorem projectiveToricData36_translate
    (a : DephasedPhase6) (X : Fin 36 → DephasedPhase6)
    (ha : IsDephasedPhase6 a)
    (hdesign : IsUniformProjectiveToric2Design36 X)
    (hoverlap : SatisfiesMUBOverlap6 X) :
    IsUniformProjectiveToric2Design36 (translatePhaseFamily6 a X) ∧
      SatisfiesMUBOverlap6 (translatePhaseFamily6 a X) := by sorry

end RybinAI2026.P16

Source

A Translation Observation for Three Conjectures on Projective Toric Designs, Translation Lemma; arXiv:2311.13479v3, Definition 2.5 and Eq. (25).

View graph