OAI/Analysis/MutuallyUnbiased/TaoCertificate/Conclusion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.TaoCertificate.source_eq_target line 9
2. theorem OAI.MUB6.TaoCertificate.tao_exclusion line 12

   Source documentation

   The exact source-derived Tao exclusion certificate contradicts cubic positivity.

   theorem tao_exclusion (f : Charge → ℂ)
       (hcross : ∀ a c, Balanced a → Balanced c →
         offDiagSum (fun i j => f (a + difference i j) *
           star (g tao (c + difference i j))) = 0)
       (horder : OrderTwoValues f)
       (hpositive : 0 ≤ 6 + offDiagSum (fun i j => (f ((3 : ℤ) • difference i j)).re)) : False := by
   …

   Mentions: OAI.MUB6.Charge, OAI.MUB6.Balanced, OAI.MUB6.offDiagSum, OAI.MUB6.difference, OAI.MUB6.g, OAI.MUB6.tao