OAI/Analysis/MutuallyUnbiased/MixedSemantics/GroupedColumns4.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Explicit four-column grouping formulas for the fifteen equality patterns used by the exact pair certificate.

  1. theorem OAI.MUB6.groupedColumns_family4_0 line 11
  2. theorem OAI.MUB6.groupedColumns_family4_1 line 19
  3. theorem OAI.MUB6.groupedColumns_family4_2 line 26
  4. theorem OAI.MUB6.groupedColumns_family4_3 line 33
  5. theorem OAI.MUB6.groupedColumns_family4_4 line 40
  6. theorem OAI.MUB6.groupedColumns_family4_5 line 47
  7. theorem OAI.MUB6.groupedColumns_family4_6 line 54
  8. theorem OAI.MUB6.groupedColumns_family4_7 line 61
  9. theorem OAI.MUB6.groupedColumns_family4_8 line 68
  10. theorem OAI.MUB6.groupedColumns_family4_9 line 75
  11. theorem OAI.MUB6.groupedColumns_family4_10 line 82
  12. theorem OAI.MUB6.groupedColumns_family4_11 line 89
  13. theorem OAI.MUB6.groupedColumns_family4_12 line 96
  14. theorem OAI.MUB6.groupedColumns_family4_13 line 103
  15. theorem OAI.MUB6.groupedColumns_family4_14 line 110