OAI/Computability/MaxCut/Encoding/BinaryCoordinates.lean

GitHub source file

33 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.MaxCutGames.Integration.BinaryCoordinates.Coordinates line 13
  2. def OAI.MaxCutGames.Integration.BinaryCoordinates.pack line 15
  3. def OAI.MaxCutGames.Integration.BinaryCoordinates.unpack line 19
  4. theorem OAI.MaxCutGames.Integration.BinaryCoordinates.pack_get line 22
  5. theorem OAI.MaxCutGames.Integration.BinaryCoordinates.unpack_pack line 31
  6. theorem OAI.MaxCutGames.Integration.BinaryCoordinates.pack_unpack line 35
  7. theorem OAI.MaxCutGames.Integration.BinaryCoordinates.unpack_injective line 40
  8. theorem OAI.MaxCutGames.Integration.BinaryCoordinates.pack_injective line 45
  9. theorem OAI.MaxCutGames.Integration.BinaryCoordinates.unpack_xor line 50
  10. theorem OAI.MaxCutGames.Integration.BinaryCoordinates.pack_xor line 55
  11. theorem OAI.MaxCutGames.Integration.BinaryCoordinates.unpack_zero line 60
  12. theorem OAI.MaxCutGames.Integration.BinaryCoordinates.pack_zero line 64
  13. abbrev OAI.MaxCutGames.Integration.BinaryLinear.F2 line 75
  14. abbrev OAI.MaxCutGames.Integration.BinaryLinear.Vector line 76
  15. def OAI.MaxCutGames.Integration.BinaryLinear.ofBit line 78
  16. def OAI.MaxCutGames.Integration.BinaryLinear.toBit line 79
  17. theorem OAI.MaxCutGames.Integration.BinaryLinear.scalar_cases line 81
  18. theorem OAI.MaxCutGames.Integration.BinaryLinear.ofBit_toBit line 82
  19. theorem OAI.MaxCutGames.Integration.BinaryLinear.toBit_ofBit line 83
  20. theorem OAI.MaxCutGames.Integration.BinaryLinear.ofBit_xor line 84
  21. theorem OAI.MaxCutGames.Integration.BinaryLinear.toBit_add line 85
  22. def OAI.MaxCutGames.Integration.BinaryLinear.toVector line 87
  23. def OAI.MaxCutGames.Integration.BinaryLinear.fromVector line 88
  24. theorem OAI.MaxCutGames.Integration.BinaryLinear.toVector_fromVector line 90
  25. theorem OAI.MaxCutGames.Integration.BinaryLinear.fromVector_toVector line 94
  26. def OAI.MaxCutGames.Integration.BinaryLinear.coordinatesEquiv line 98
  27. theorem OAI.MaxCutGames.Integration.BinaryLinear.toVector_xor line 104
  28. theorem OAI.MaxCutGames.Integration.BinaryLinear.fromVector_add line 109
  29. theorem OAI.MaxCutGames.Integration.BinaryLinear.toVector_zero line 113
  30. theorem OAI.MaxCutGames.Integration.BinaryLinear.fromVector_zero line 118
  31. def OAI.MaxCutGames.Integration.BinaryLinear.liftLinear line 122

    Source documentation

    A zero-preserving XOR-additive map becomes a genuine binary linear map.

    def liftLinear {n m : Nat} (f : BitVec n → BitVec m)
    (hzero : f 0 = 0) (hadd : ∀ x y, f (x ^^^ y) = f x ^^^ f y) :
    Vector n →ₗ[F2] Vector m where
…

    Mentions: OAI.MaxCutGames.Integration.BinaryLinear.Vector, OAI.MaxCutGames.Integration.BinaryLinear.F2

  32. theorem OAI.MaxCutGames.Integration.BinaryLinear.liftLinear_apply line 133
  33. theorem OAI.MaxCutGames.Integration.BinaryLinear.finrank_vector line 138