OAI/Analysis/MutuallyUnbiased/MixedSemantics/Rules.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Sound rules for mixed certificate normalization

Generated witnesses may only permute rows or factors, negate all charges, remove zero rows or factors, and injectively rename labels. The equalities here justify those operations for the actual finite mixed moments.

  1. theorem OAI.MUB6.Certificate.MixedSemantics.permute line 21
  2. theorem OAI.MUB6.Certificate.MixedSemantics.delete_zero_row line 28
  3. theorem OAI.MUB6.Certificate.MixedSemantics.delete_zero_factor line 35
  4. theorem OAI.MUB6.Certificate.MixedSemantics.rename_labels line 43
  5. theorem OAI.MUB6.Certificate.MixedSemantics.singleton_first line 50