Translation of dimension-six projective toric phase families

Definition

mub6_projective_toric_translation

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

design-theorymutually-unbiased-bases

For a dephased phase vector $a\in P(T^6)$ and a labeled 36-point phase family $X$ , define the translate $aX$ by coordinatewise multiplication:

(aX)_x(j)=a(j)X_x(j).

This is additive translation in phase notation. It is the operation under which projective toric character moments and the pairwise MUB overlap expression are invariant.

Definition code

import Definitions.Def_mub6_projective_toric_design

namespace RybinAI2026.P16

/-- Translate every represented projective-torus point by the same dephased phase vector. -/
def translatePhaseFamily6
    (a : DephasedPhase6) (X : Fin 36 → DephasedPhase6) :
    Fin 36 → DephasedPhase6 :=
  fun x => phaseMul6 a (X x)

end RybinAI2026.P16

Source

A Translation Observation for Three Conjectures on Projective Toric Designs, Sections 2--3 (user-supplied manuscript); arXiv:2311.13479v3, Definitions 2.4--2.5 and Eq. (25).

View graph