TaoSymmetry.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The cubic symmetry lemma for Tao's matrix and its normalized characters.

The natural exponents of MUB6.tao and the signed five-cycle exponents of HadamardSix.taoMatrix agree modulo three. This identifies their characters and transfers the row symmetry and signed charge invariance.

theorem OAI.MUB6.tao_eq_hadamardSix line 15
Source documentation
The two five-cycle exponent conventions define the same complex matrix.
```
theorem tao_eq_hadamardSix : tao = HadamardSix.taoMatrix := by
…
```
Mentions: OAI.MUB6.tao, OAI.HadamardSix.taoMatrix

theorem OAI.MUB6.CubicSymmetry.every_row_permutation_complex line 27

Source documentation

Every row permutation of Tao's matrix extends by column permutations, unit phases, and optional complex conjugation.

theorem every_row_permutation_complex (p : Equiv.Perm Coord) :
    ∃ (q : Equiv.Perm Coord) (conjugate : Bool) (U V : Coord → ℂ),
      (∀ i, ‖U i‖ = 1) ∧ (∀ j, ‖V j‖ = 1) ∧
      ∀ i j, tao (p i) (q j) =
        U i * V j * (if conjugate then star (tao i j) else tao i j) := by
…

Mentions: OAI.MUB6.Coord, OAI.MUB6.tao

theorem OAI.MUB6.CubicSymmetry.norm_g_signed_permute line 36
Source documentation
On balanced charges the Fourier norm is invariant under signed permutations.
```
theorem norm_g_signed_permute (a : Charge) (ha : Balanced a)
    (p : Equiv.Perm Coord) (negate : Bool) :
    ‖g tao (if negate then -(permuteCharge p a) else permuteCharge p a)‖ =
      ‖g tao a‖ := by
…
```
Mentions: OAI.MUB6.Charge, OAI.MUB6.Balanced, OAI.MUB6.Coord, OAI.MUB6.g, OAI.MUB6.tao, OAI.MUB6.permuteCharge

theorem OAI.MUB6.CubicSymmetry.cubic_symmetry line 48

Source documentation

The cubic symmetry lemma: matrix symmetries and invariance of Fourier norms on the signed permutation orbits of balanced charges.

theorem cubic_symmetry :
    (∀ p : Equiv.Perm Coord,
      ∃ (q : Equiv.Perm Coord) (conjugate : Bool) (U V : Coord → ℂ),
        (∀ i, ‖U i‖ = 1) ∧ (∀ j, ‖V j‖ = 1) ∧
        ∀ i j, tao (p i) (q j) =
          U i * V j * (if conjugate then star (tao i j) else tao i j)) ∧
    (∀ a : Charge, Balanced a → ∀ (p : Equiv.Perm Coord) (negate : Bool),
      ‖g tao (if negate then -(permuteCharge p a) else permuteCharge p a)‖ =
        ‖g tao a‖) :=
…

Mentions: OAI.MUB6.Coord, OAI.MUB6.tao, OAI.MUB6.Charge, OAI.MUB6.Balanced, OAI.MUB6.g, OAI.MUB6.permuteCharge