logo

Axioms for the theory of proveit.physics.quantum

In [1]:
import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit import k, n, x, y, alpha, U, f, fx, fy, ExprArray, ExprTuple
from proveit.linear_algebra import MatrixProd, TensorProd, SU, ScalarProd
from proveit.logic import Equals, Forall, Iff, InSet, Set
from proveit.numbers import zero, one, two, frac, Integer, NaturalPos, Complex, Exp
from proveit.numbers import Add, Exp, sqrt, subtract
from proveit.numbers.number_sets import Interval
from proveit.physics.quantum import Input, Output, RegisterKet
from proveit.physics.quantum.circuit import Gate, MultiQubitGate, CircuitEquiv, Circuit, MultiWire
# from proveit.physics.quantum import Bra, Ket, RegisterBra, Meas, MultiWire, Circuit
from proveit.physics.quantum import ket0, ket1, ket_plus, H, QubitSpace, RegisterSU, I, CONTROL
# from proveit.physics.quantum import I, X, Y, Z, RegisterSU
from proveit.physics.quantum import QubitRegisterSpace
In [2]:
%begin axioms
Defining axioms for theory 'proveit.physics.quantum'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions
In [3]:
ket_zero_in_qubit_space = InSet(ket0, QubitSpace)
Out[3]:
ket_zero_in_qubit_space:
In [4]:
ket_one_in_qubit_space = InSet(ket1, QubitSpace)
Out[4]:
ket_one_in_qubit_space:
In [5]:
single_qubit_register_zero = Equals(RegisterKet(zero, one), ket0)
Out[5]:
single_qubit_register_zero:
In [6]:
single_qubit_register_one = Equals(RegisterKet(one, one), ket1)
Out[6]:
single_qubit_register_one:
In [7]:
# Not clear why this is here, and we suspect it is incorrect:
# shouldn't the extra qbit be on the left instead of on the right
Forall(k, Equals(RegisterKet(k, Add(n, one)), 
                 TensorProd(RegisterKet(k, n), ket0)),
      domain=Interval(zero, subtract(Exp(two, n), one)))
Out[7]:
In [8]:
expand_register_with_zero_ket = Forall(
        n,
        Forall(k,
               Equals(RegisterKet(k, Add(n, one)),
                      TensorProd(RegisterKet(k, n), ket0)),
               domain=Interval(zero, subtract(Exp(two, n), one))),
        domain=NaturalPos)
Out[8]:
expand_register_with_zero_ket:
In [9]:
expand_register_with_one_ket = Forall(
        n, 
        Forall(k, Equals(RegisterKet(Add(k, Exp(two, n)), Add(n, one)),
                         TensorProd(RegisterKet(k, n), ket1)),
               domain=Interval(zero, subtract(Exp(two, n), one))),
        domain=NaturalPos)
Out[9]:
expand_register_with_one_ket:
In [10]:
ket_plus_def = Equals(ket_plus, frac(Add(ket0, ket1), sqrt(two)))
Out[10]:
ket_plus_def:
In [11]:
hadamard_on_zero = Equals(MatrixProd(H, ket0), ket_plus)
Out[11]:
hadamard_on_zero:
In [12]:
empty_gate = Equals(Gate(), I.with_styles(representation="explicit")) # base case
Out[12]:
empty_gate:
In [13]:
substitution = Forall((f, x, y), CircuitEquiv(fx, fy), conditions=CircuitEquiv(x, y))
Out[13]:
substitution:

And then we have several axioms involving the Circuit class, which class itself still needs updating
(in particular, the Circuit class needs an appropriate substitute for the ExpressionTensor class -- perhaps ExprArray).

In [14]:
circuit_gate_application = Forall(
    U, 
    Forall((x, y),
           Iff(Circuit(ExprArray(ExprTuple(Input(x), Gate(U), Output(y)))),
               Equals(y, MatrixProd(U, x))),
           domain=QubitSpace),
    domain=SU(two))
Out[14]:
circuit_gate_application:
In [15]:
circuit_multi_gate_application = Forall(
    n,
    Forall(U,
           Forall((x, y),
                  Iff(Circuit(ExprArray(ExprTuple(Input(x), MultiWire(n), Gate(U), Output(y)))),
                      Equals(y, MatrixProd(U, x))),
                  domain=QubitRegisterSpace(n)),
           domain=RegisterSU(n)),
    domain=NaturalPos)
Out[15]:
circuit_multi_gate_application:
In [16]:
zero_controlled_ngate = Forall(
    n,
    Forall(U,
           Forall(x,
                  Forall(alpha,
                         Circuit(ExprArray(ExprTuple(Input(ScalarProd(alpha, ket0)),
                                   I,
                                   MultiQubitGate(CONTROL, Set(one, two)),
                                   Output(ScalarProd(alpha, ket0))),
                                  ExprTuple(Input(x), MultiWire(n), MultiQubitGate(U, Set(one, two)), Output(x)))),
                         domain=Complex),
                  domain=QubitRegisterSpace(n)),
           domain=SU(Exp(two, n))),
    domain=NaturalPos)
Out[16]:
zero_controlled_ngate:
In [17]:
one_controlled_ngate = Forall(
    n,
    Forall(U,
           Forall(x,
                  Forall(alpha,
                         Circuit(ExprArray(ExprTuple(Input(ScalarProd(alpha, ket1)),
                                   I,
                                   MultiQubitGate(CONTROL, Set(one, two)),
                                   Output(ScalarProd(alpha, ket1))),
                                  ExprTuple(Input(x), MultiWire(n), MultiQubitGate(U, Set(one, two)), Output(MatrixProd(U, x))))),
                         domain=Complex),
                  domain=QubitRegisterSpace(n)),
           domain=SU(Exp(two, n))),
    domain=NaturalPos)
Out[17]:
one_controlled_ngate:
In [18]:
%end axioms
These axioms may now be imported from the theory package: proveit.physics.quantum