Theorems (or conjectures) for the theory of proveit.physics.quantum¶
In [1]:
import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit import (Operation, Function, IndexedVar,
ExprTuple, ExprRange, var_range, ExprArray)
from proveit import (a, b, c, d, f, g, h, i, j, k, l, m, n, p,
t, u, x, y, z, alpha,
A, B, C, D, E, F, G, P, Q, R, S, U, V, W, X, Y,
Psi, Px, Py)
from proveit.core_expr_types import (
x_1_to_n, b_1_to_j, A_1_to_l, A_1_to_m, B_1_to_i,
B_1_to_m, C_1_to_n)
from proveit.core_expr_types.expr_arrays import Aij, Bij, Cij, Dij, Eij, Pij, Qij, Rij, Sij, B11_to_Bmn, D11_to_Dmn, S11_to_Smn
from proveit.linear_algebra import VecAdd, VecSum, LinMap, TensorProd
from proveit.logic import (Implies, Iff, And, Equals, Forall,
Set, InSet, Union, InClass)
from proveit.numbers import (zero, one, two, three, subtract,
Abs, Add, Complex, Exp, Mult,
Natural, NaturalPos, Sum)
from proveit.numbers.number_sets import Interval
from proveit.physics.quantum import (
Ket, Meas, QubitRegisterSpace,
NumKet, NumBra, Qmult)
from proveit.physics.quantum import (
H, inv_root2, ket0, ket1, ket_plus, QubitSpace, SPACE, CONTROL, I)#, pregated_controlled_ngate,
#pregated_controlled_ngate_with_merge)
from proveit.statistics import Prob
# from proveit.physics.quantum.common import I, H, Hgate, CTRL_DN, WIRE_DN, WIRE_LINK, PASS, \
# , QubitRegisterSpace, RegisterSU
from proveit.linear_algebra import MatrixMult, ScalarMult, Unitary
In [2]:
%begin theorems
The following 3 cells require updates to Circuit class before they can proceed.
These then affect a handful of theorems/expressions below that refer to the Circuits.¶
In [3]:
def controlled_ngate(a, b, x, y):
return Circuit(ExprArray(ExprTuple(Input(a), I, MultiQubitGate(CONTROL, Set(one, two)), Output(b)),
ExprTuple(Input(x), MultiWire(n), MultiQubitGate(U, Set(one, two)), Output(y))))
In [4]:
ket_plus_distributed = Equals(
ket_plus, Add(ScalarMult(inv_root2, ket0),
ScalarMult(inv_root2, ket1)))
In [5]:
scaled_qubit_state_in_qubit_space = Forall(
x,
Forall(alpha,
InSet(ScalarMult(alpha, x), QubitSpace),
domain=Complex),
domain=QubitSpace)
In [6]:
transformed_qubit_state_in_qubit_space = Forall(
x,
Forall(U,
InSet(Qmult(U, x), QubitSpace),
domain=Unitary(two)),
domain=QubitSpace)
In [7]:
# See prepend_num_ket_with_one_ket in quantum.algebra
# multi_tensor_prod_induct_1 = Forall(t,
# Forall(k,
# Equals(TensorProd(Ket(one), NumKet(k, t)),
# NumKet(Add(Exp(two, t), k), Add(t, one))),
# domain=Interval(zero, subtract(Exp(two, t), one))),
# domain=NaturalPos)
In [8]:
# See prepend_num_ket_with_zero_ket in quantum.algebra
# multi_tensor_prod_induct_0 = Forall(t,
# Forall(k,
# Equals(TensorProd(Ket(zero), NumKet(k, t)),
# NumKet(k, Add(t, one))),
# domain=Interval(zero, subtract(Exp(two, t), one))),
# domain=NaturalPos)
In [9]:
# single_time_equiv = Forall ((h, k, m), Forall((var_range(A, [one, one], [m, k]), var_range(B, one, m),
# var_range(C, [one, one], [m, h]), var_range(D, one, m),
# var_range(S, one, m), var_range(R, [one, one], [m, k]),
# var_range(Q, [one, one], [m, h])),
# Implies(
# CircuitEquiv(
# Circuit(ExprArray(ExprRange(i, ExprTuple(MultiQubitGate(IndexedVar(B, i), IndexedVar(S, i))), one, m))),
# Circuit(ExprArray(ExprRange(i, ExprTuple(MultiQubitGate(IndexedVar(D, i), IndexedVar(S, i))), one, m)))
# ),
# CircuitEquiv(
# Circuit(ExprArray(ExprRange(i, ExprTuple(ExprRange(j, MultiQubitGate(Aij, Rij), one, k),
# MultiQubitGate(IndexedVar(B, i), IndexedVar(S, i)),
# ExprRange(j, MultiQubitGate(Cij, Qij), one, h)),
# one, m))),
# Circuit(ExprArray(ExprRange(i, ExprTuple(ExprRange(j, MultiQubitGate(Aij, Rij), one, k),
# MultiQubitGate(IndexedVar(D, i), IndexedVar(S, i)),
# ExprRange(j, MultiQubitGate(Cij, Qij), one, h)),
# one, m)))
# )
# ).with_wrapping_at(2)
# ).wrap_params(), domain=NaturalPos)
In [10]:
# single_time_equiv_judgement = Forall ((h, k, m), Forall((var_range(A, [one, one], [m, k]), var_range(B, one, m),
# var_range(C, [one, one], [m, h]), var_range(D, one, m),
# var_range(S, one, m), var_range(R, [one, one], [m, k]),
# var_range(Q, [one, one], [m, h])),
# Implies(And(
# CircuitEquiv(
# Circuit(ExprArray(ExprRange(i, ExprTuple(MultiQubitGate(IndexedVar(B, i), IndexedVar(S, i))), one, m))),
# Circuit(ExprArray(ExprRange(i, ExprTuple(MultiQubitGate(IndexedVar(D, i), IndexedVar(S, i))), one, m)))
# ), Circuit(ExprArray( ExprRange(i, ExprTuple(ExprRange(j, MultiQubitGate(Aij, Rij), one, k),
# MultiQubitGate(IndexedVar(B, i), IndexedVar(S, i)),
# ExprRange(j, MultiQubitGate(Cij, Qij), one, h)),
# one, m)))),
# Circuit(ExprArray(ExprRange(i, ExprTuple(ExprRange(j, MultiQubitGate(Aij, Rij), one, k),
# MultiQubitGate(IndexedVar(D, i), IndexedVar(S, i)),
# ExprRange(j, MultiQubitGate(Cij, Qij), one, h)),
# one, m))
# )
# ).with_wrapping_at(2)
# ).wrap_params(), domain=NaturalPos)
In [11]:
# temporal_circuit_substitution = Forall ((g, h, k, m, n),
# Forall((var_range(A, [one, one], [m, g]), var_range(B, [one, one], [m, h]),
# var_range(C, [one, one], [m, k]), D11_to_Dmn,
# var_range(P, [one, one], [m, g]), var_range(Q, [one, one], [m, h]),
# var_range(R, [one, one], [m, k]), S11_to_Smn),
# Implies(
# And(CircuitEquiv(
# Circuit(ExprArray(ExprRange(i, ExprTuple(ExprRange(j, MultiQubitGate(Bij, Qij), one, h)), one, m))),
# Circuit(ExprArray(ExprRange(i, ExprTuple(ExprRange(j, MultiQubitGate(Dij, Sij), one, n)), one, m)))
# ),
# Circuit(ExprArray(ExprRange(i, ExprTuple(ExprRange(j, MultiQubitGate(Aij, Pij), one, g),
# ExprRange(j, MultiQubitGate(Bij, Qij), one, h),
# ExprRange(j, MultiQubitGate(Cij, Rij), one, k)),
# one, m)))),
# Circuit(ExprArray(ExprRange(i, ExprTuple(ExprRange(j, MultiQubitGate(Aij, Pij), one, g),
# ExprRange(j, MultiQubitGate(Dij, Sij), one, n),
# ExprRange(j, MultiQubitGate(Cij, Rij), one, k)),
# one, m)))
# ).with_wrapping_at(2)
# ).wrap_params(), domain=NaturalPos)
In [ ]:
In [12]:
# temporal_circuit_equiv = Forall ((h, k, m, n), Forall((var_range(A, [one, one], [m, k]), B11_to_Bmn,
# var_range(C, [one, one], [m, h]), D11_to_Dmn,
# S11_to_Smn, var_range(R, [one, one], [m, k]),
# var_range(Q, [one, one], [m, h])),
# Implies(
# CircuitEquiv(
# Circuit(ExprArray(ExprRange(i, ExprTuple(ExprRange(j, MultiQubitGate(Bij, Sij), one, n)), one, m))),
# Circuit(ExprArray(ExprRange(i, ExprTuple(ExprRange(j, MultiQubitGate(Dij, Sij), one, n)), one, m)))
# ),
# CircuitEquiv(
# Circuit(ExprArray(ExprRange(i, ExprTuple(ExprRange(j, MultiQubitGate(Aij, Rij), one, k),
# ExprRange(j, MultiQubitGate(Bij, Sij), one, n),
# ExprRange(j, MultiQubitGate(Cij, Qij), one, h)),
# one, m))),
# Circuit(ExprArray(ExprRange(i, ExprTuple(ExprRange(j, MultiQubitGate(Aij, Rij), one, k),
# ExprRange(j, MultiQubitGate(Dij, Sij), one, n),
# ExprRange(j, MultiQubitGate(Cij, Qij), one, h)),
# one, m)))
# )
# ).with_wrapping_at(2)
# ).wrap_params(), domain=NaturalPos)
In [13]:
# single_space_equiv = Forall((k, m, n), Forall((var_range(A, [one, one], [m, n]), var_range(B, one, n),
# var_range(C, [one, one], [k, n]), var_range(D, one, n),
# S11_to_Smn, var_range(Q, one, n),
# var_range(R, [one, one], [k, n])),
# Implies(
# CircuitEquiv(
# Circuit(ExprArray(ExprTuple(ExprRange(j, Gate(IndexedVar(B, j)), one, n)))),
# Circuit(ExprArray(ExprTuple(ExprRange(j, Gate(IndexedVar(D, j)), one, n))))
# ),
# CircuitEquiv(
# Circuit(ExprArray(ExprRange(i, ExprTuple(ExprRange(j, MultiQubitGate(Aij, Sij), one, n)), one, m),
# ExprTuple(ExprRange(j, Gate(IndexedVar(B, j)), one, n)),
# ExprRange(i, ExprTuple(ExprRange(j, MultiQubitGate(Cij, Rij), one, n)), one, k))),
# Circuit(ExprArray(ExprRange(i, ExprTuple(ExprRange(j, MultiQubitGate(Aij, Sij), one, n)), one, m),
# ExprTuple(ExprRange(j, Gate(IndexedVar(D, j)), one, n)),
# ExprRange(i, ExprTuple(ExprRange(j, MultiQubitGate(Cij, Rij), one, n)), one, k)))
# )
# ).with_wrapping_at(2)
# ).wrap_params(), domain=NaturalPos)
In [14]:
# double_space_equiv = Forall((h, k, m, n), Forall((var_range(A, [one, one], [m, n]), var_range(B, one, n),
# var_range(C, [one, one], [k, n]), var_range(D, one, n),
# var_range(E, [one, one], [h, n]), var_range(F, one, n),
# var_range(G, one, n),
# S11_to_Smn, var_range(Q, [one, one], [h, n]),
# var_range(R, [one, one], [k, n])),
# Implies(
# CircuitEquiv(
# Circuit(ExprArray(ExprTuple(ExprRange(j, MultiQubitGate(IndexedVar(B, j), Set(Add(m, one), Add(m, k, two))), one, n)),
# ExprTuple(ExprRange(j, MultiQubitGate(IndexedVar(D, j), Set(Add(m, one), Add(m, k, two))), one, n)))),
# Circuit(ExprArray(ExprTuple(ExprRange(j, MultiQubitGate(IndexedVar(F, j), Set(Add(m, one), Add(m, k, two))), one, n)),
# ExprTuple(ExprRange(j, MultiQubitGate(IndexedVar(G, j), Set(Add(m, one), Add(m, k, two))), one, n))))
# ),
# CircuitEquiv(
# Circuit(ExprArray(ExprRange(i, ExprTuple(ExprRange(j, MultiQubitGate(Aij, Sij), one, n)), one, m),
# ExprTuple(ExprRange(j, MultiQubitGate(IndexedVar(B, j), Set(Add(m, one), Add(m, k, two))), one, n)),
# ExprRange(i, ExprTuple(ExprRange(j, MultiQubitGate(Cij, Rij), one, n)), one, k),
# ExprTuple(ExprRange(j, MultiQubitGate(IndexedVar(D, j), Set(Add(m, one), Add(m, k, two))), one, n)),
# ExprRange(i, ExprTuple(ExprRange(j, MultiQubitGate(Eij, Qij), one, n)), one, h))),
# Circuit(ExprArray(ExprRange(i, ExprTuple(ExprRange(j, MultiQubitGate(Aij, Sij), one, n)), one, m),
# ExprTuple(ExprRange(j, MultiQubitGate(IndexedVar(F, j), Set(Add(m, one), Add(m, k, two))), one, n)),
# ExprRange(i, ExprTuple(ExprRange(j, MultiQubitGate(Cij, Rij), one, n)), one, k),
# ExprTuple(ExprRange(j, MultiQubitGate(IndexedVar(G, j), Set(Add(m, one), Add(m, k, two))), one, n)),
# ExprRange(i, ExprTuple(ExprRange(j, MultiQubitGate(Eij, Qij), one, n)), one, h))))
# ).with_wrapping_at(2)
# ).wrap_params(), domain=NaturalPos)
In [15]:
# # need to form an Iter to replace x_etc here
# # summed_qubit_state_in_qubit_space = Forall(x_etc, InSet(Add(x_etc), QubitSpace), domain=QubitSpace)
# summed_qubit_state_in_qubit_space = Forall(
# n,
# Forall(
# x_1_to_n,
# InSet(Add(x_1_to_n), QubitSpace),
# domain=QubitSpace),
# domain=NaturalPos)
In [16]:
# scaled_qubit_register_state_in_qubit_register_space = Forall(
# n,
# Forall(x,
# Forall(alpha, InSet(ScalarMult(alpha, x), QubitRegisterSpace(n)),
# domain=Complex),
# domain=QubitRegisterSpace(n)),
# domain=NaturalPos)
In [17]:
# register_ket_in_qubit_register_space = Forall(
# n,
# Forall(k, InSet(NumKet(k, n), QubitRegisterSpace(n)),
# domain = Interval(zero, subtract(Exp(two, n), one))),
# domain=NaturalPos)
In [18]:
# register_qubit_complex_amplitude = Forall(
# n,
# Forall(k,
# Forall(Psi,
# InSet(Qmult(NumBra(k, n), Ket(Psi)), Complex),
# conditions = [InSet(Ket(Psi), QubitRegisterSpace(n))]),
# domain=Interval(zero, subtract(Exp(two, n),one))),
# domain=NaturalPos)
In [19]:
# register_qubit_born_rule = Forall(
# n,
# Forall(k,
# Forall((Psi, m),
# Equals(Prob(Equals(m, k), m),
# Exp(Abs(Qmult(NumBra(k, n), Ket(Psi))), two)),
# conditions = [InSet(Ket(Psi), QubitRegisterSpace(n)), Equals(m, Meas(Ket(Psi)))]),
# domain=Interval(zero, subtract(Exp(two, n), one))),
# domain=NaturalPos)
In [20]:
# register_qubit_all_probs = Forall(
# n,
# Forall((Psi, m),
# Equals(Sum(k, Prob(Equals(m, k), m),
# domain=Interval(zero, subtract(Exp(two, n), one))),
# one),
# conditions = [InSet(Ket(Psi), QubitRegisterSpace(n)), Equals(m, Meas(Ket(Psi)))]),
# domain=NaturalPos)
In [21]:
# ## This one requires pregated_controlled_ngate, defined at the top of this page,
# ## but that pregated_controlled_ngate requires the Circuit class
# pregated_controlled_ngate_equiv = Forall(
# n,
# Forall(U,
# Forall(u,
# Forall((a, b),
# Forall((x, y),
# Equals(pregated_controlled_ngate,
# controlled_ngate(
# Qmult(u, a), b, x, y)),
# domain=QubitRegisterSpace(n)),
# domain=QubitSpace),
# domain=SU(two)),
# domain=RegisterSU(n)),
# domain=NaturalPos)
In [22]:
# ## This one requires controlled_ngate, defined at the top of this page,
# ## but that controlled_ngate requires the Circuit class
# controlled_ngate_equiv = Forall(
# n,
# Forall(U,
# Forall((a, b, c),
# Forall((x, y, z),
# Iff(Equals(controlled_ngate(a, b, x, y),
# controlled_ngate(a, c, x, z)),
# Equals(TensorProd(b, y), TensorProd(c, z))),
# domain=QubitRegisterSpace(n)),
# domain=QubitSpace),
# domain=RegisterSU(n)),
# domain=NaturalPos)
In [23]:
# ## This one requires controlled_ngate, defined at the top of this page,
# ## but that controlled_ngate requires the Circuit class
# superposition_controlled_ngate = Forall(
# n,
# Forall(U,
# Forall((a, b, c, d),
# Forall((x, y),
# Implies(And(controlled_ngate(a, c, x, y),
# controlled_ngate(b, d, x, y)),
# controlled_ngate(Add(a, b), Add(c, d), x, y)),
# domain=QubitRegisterSpace(n)),
# domain=QubitSpace),
# domain=RegisterSU(n)),
# domain=NaturalPos)
In [24]:
# ## This one requires pregated_controlled_ngate, defined at the top of this page,
# ## but that pregated_controlled_ngate requires the Circuit class
# pregated_controlled_ngate_merger = Forall(
# (n, k),
# Forall(U,
# Forall(u,
# Forall((a, b),
# Forall(c,
# Forall(d,
# Forall((x, y),
# Implies(pregated_controlled_ngate,
# Implies(pregated_controlled_ngate_with_merge,
# Equals(d, TensorProd(c, b)))),
# domain=QubitRegisterSpace(n)),
# domain=QubitRegisterSpace(Add(k, one))),
# domain=QubitRegisterSpace(k)),
# domain=QubitSpace),
# domain=SU(two)),
# domain=RegisterSU(n)),
# domain=NaturalPos)
In [25]:
# TOOK REALLY LONG TO RUN... MORE TESTING NEEDED
#register_bra_over_summed_ket = Forall(
# n,
# Forall(U,
# Forall(l,
# Forall(f,
# Equals(MatrixProd(RegisterBra(l, n),
# MatrixProd(U, Sum(k, ScalarProd(Operation(f, k), RegisterKet(k, n)),
# domain=Interval(zero, subtract(Exp(two, n), one))))),
# Sum(k, Mult(Operation(f, k),
# MatrixProd(RegisterBra(l, n), U, RegisterKet(k, n))),
# domain=Interval(zero, subtract(Exp(two, n), one))))),
# domain=Interval(zero, subtract(Exp(two, n), one))),
#domain=SU(Exp(two, n))),
#domain=NaturalPos)
In [26]:
%end theorems