TaoCompleteFamily.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.MUB6.matrix_family_not_equivalent_tao line 14
Source documentation
The Tao class is excluded by the exact certificate, without choosing a restricted phase convention for any of the six matrices.
```
theorem matrix_family_not_equivalent_tao (H : Coord → CMatrix)
    (hH : ∀ t, IsHadamard (H t))
    (hcross : ∀ t s, t ≠ s → ∀ k l,
      Complex.normSq (∑ i, H t i k * conj (H s i l)) = 6)
    (horder : ∀ a, Balanced a → order a = 2 → ∑ t, g (H t) a = 0)
    (s : Coord) : ¬Equivalent (H s) tao := by
…
```
Mentions: OAI.MUB6.Coord, OAI.MUB6.CMatrix, OAI.MUB6.IsHadamard, OAI.MUB6.Balanced, OAI.MUB6.order, OAI.MUB6.g, OAI.MUB6.Equivalent, OAI.MUB6.tao
theorem OAI.MUB6.complete_family_not_equivalent_tao line 26
Source documentation
No transition matrix of a complete mutually unbiased family can belong to Tao's cubic equivalence class.
```
theorem complete_family_not_equivalent_tao (B : Fin 7 → Basis) (hB : IsMUBFamily B)
    (r : Fin 7) (s : Coord) : ¬Equivalent (relativeMatrix B r s) tao := by
…
```
Mentions: OAI.MUB6.Basis, OAI.MUB6.IsMUBFamily, OAI.MUB6.Coord, OAI.MUB6.Equivalent, OAI.MUB6.relativeMatrix, OAI.MUB6.tao
theorem OAI.MUB6.complete_family_square_not_hadamard line 35
Source documentation
Proposition (cubic-exclusion) in the manuscript.
```
theorem complete_family_square_not_hadamard (B : Fin 7 → Basis) (hB : IsMUBFamily B)
    (r : Fin 7) (s : Coord) :
    ¬IsHadamard (fun i j => relativeMatrix B r s i j ^ 2) := by
…
```
Mentions: OAI.MUB6.Basis, OAI.MUB6.IsMUBFamily, OAI.MUB6.Coord, OAI.MUB6.IsHadamard, OAI.MUB6.relativeMatrix