OAI/Analysis/MutuallyUnbiased/Cubic/NormalizedCodes.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

A second finite presentation of the five-cycle classification. A row has two positive signs among four off-diagonal positions, hence six choices.

  1. def OAI.MUB6.fourChoices line 11
  2. def OAI.MUB6.offDiagonalIndex line 16
  3. def OAI.MUB6.fiveRowChoice line 21
  4. def OAI.MUB6.normalizedCodeGraph line 24
  5. theorem OAI.MUB6.rowChoice_complete line 27
  6. def OAI.MUB6.normalizedCodeOrthogonal line 32
  7. def OAI.MUB6.normalizedCodeClassified line 37
  8. theorem OAI.MUB6.normalizedCodes_00 line 42
  9. theorem OAI.MUB6.normalizedCodes_01 line 47
  10. theorem OAI.MUB6.normalizedCodes_02 line 52
  11. theorem OAI.MUB6.normalizedCodes_03 line 57
  12. theorem OAI.MUB6.normalizedCodes_04 line 62
  13. theorem OAI.MUB6.normalizedCodes_05 line 67
  14. theorem OAI.MUB6.normalizedCodes_10 line 72
  15. theorem OAI.MUB6.normalizedCodes_11 line 77
  16. theorem OAI.MUB6.normalizedCodes_12 line 82
  17. theorem OAI.MUB6.normalizedCodes_13 line 87
  18. theorem OAI.MUB6.normalizedCodes_14 line 92
  19. theorem OAI.MUB6.normalizedCodes_15 line 97
  20. theorem OAI.MUB6.normalizedCodes_20 line 102
  21. theorem OAI.MUB6.normalizedCodes_21 line 107
  22. theorem OAI.MUB6.normalizedCodes_22 line 112
  23. theorem OAI.MUB6.normalizedCodes_23 line 117
  24. theorem OAI.MUB6.normalizedCodes_24 line 122
  25. theorem OAI.MUB6.normalizedCodes_25 line 127
  26. theorem OAI.MUB6.normalizedCodes_30 line 132
  27. theorem OAI.MUB6.normalizedCodes_31 line 137
  28. theorem OAI.MUB6.normalizedCodes_32 line 142
  29. theorem OAI.MUB6.normalizedCodes_33 line 147
  30. theorem OAI.MUB6.normalizedCodes_34 line 152
  31. theorem OAI.MUB6.normalizedCodes_35 line 157
  32. theorem OAI.MUB6.normalizedCodes_40 line 162
  33. theorem OAI.MUB6.normalizedCodes_41 line 167
  34. theorem OAI.MUB6.normalizedCodes_42 line 172
  35. theorem OAI.MUB6.normalizedCodes_43 line 177
  36. theorem OAI.MUB6.normalizedCodes_44 line 182
  37. theorem OAI.MUB6.normalizedCodes_45 line 187
  38. theorem OAI.MUB6.normalizedCodes_50 line 192
  39. theorem OAI.MUB6.normalizedCodes_51 line 197
  40. theorem OAI.MUB6.normalizedCodes_52 line 202
  41. theorem OAI.MUB6.normalizedCodes_53 line 207
  42. theorem OAI.MUB6.normalizedCodes_54 line 212
  43. theorem OAI.MUB6.normalizedCodes_55 line 217
  44. theorem OAI.MUB6.normalizedCodes_classified line 222