OAI/Computability/UniqueGames/Reduction/BinaryCoordinates.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Dimension-independent transport between the compact bit-vector coordinates of the finite motif and the coordinate functions used by the later constructions. The vector-space addition involved here is XOR, not modular integer addition.

  1. abbrev OAI.UniqueGamesTheorem.Integration.BinaryCoordinates.Coordinates line 14
  2. def OAI.UniqueGamesTheorem.Integration.BinaryCoordinates.pack line 16
  3. def OAI.UniqueGamesTheorem.Integration.BinaryCoordinates.unpack line 20
  4. theorem OAI.UniqueGamesTheorem.Integration.BinaryCoordinates.pack_get line 23
  5. theorem OAI.UniqueGamesTheorem.Integration.BinaryCoordinates.unpack_pack line 32
  6. theorem OAI.UniqueGamesTheorem.Integration.BinaryCoordinates.pack_unpack line 36
  7. theorem OAI.UniqueGamesTheorem.Integration.BinaryCoordinates.unpack_injective line 41
  8. theorem OAI.UniqueGamesTheorem.Integration.BinaryCoordinates.pack_injective line 46
  9. theorem OAI.UniqueGamesTheorem.Integration.BinaryCoordinates.unpack_xor line 51
  10. theorem OAI.UniqueGamesTheorem.Integration.BinaryCoordinates.pack_xor line 56
  11. theorem OAI.UniqueGamesTheorem.Integration.BinaryCoordinates.unpack_zero line 61
  12. theorem OAI.UniqueGamesTheorem.Integration.BinaryCoordinates.pack_zero line 65