File size: 889 Bytes
d6f21bb | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 | -- Braid-word surfaces used by the resource backend.
namespace BraidCompilation
structure BraidOp where
sigma : Nat
forward : Bool
deriving Repr, DecidableEq
def op (sigma : Nat) : BraidOp := { sigma := sigma, forward := true }
def H : List BraidOp := [op 0, op 1, op 0, op 1, op 0]
def X : List BraidOp := [op 0, op 0]
def S : List BraidOp := [op 0, op 0]
def CNOT : List BraidOp := [op 2, op 1, op 0, op 1, op 2]
def CCX : List BraidOp :=
[op 4, op 5, op 4, op 5, op 4,
op 2, op 3, op 4, op 2, op 3, op 4,
op 4, op 5, op 4, op 5, op 4]
def invertOp (b : BraidOp) : BraidOp := { b with forward := !b.forward }
def invertWord (word : List BraidOp) : List BraidOp :=
word.reverse.map invertOp
theorem cnot_braid_length : CNOT.length = 5 := by
rfl
theorem ccx_braid_length : CCX.length = 16 := by
rfl
end BraidCompilation
|