Axioms for the theory of proveit.physics.quantum.algebra¶
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 (Function, Lambda, Conditional, Composition,
ExprTuple, ExprRange)
from proveit import a, b, c, i, k, m, n, x, y, A, B, M, P, X, Y, Px, Py
from proveit.core_expr_types import a_i, a_1_to_k, A_1_to_m
from proveit.logic import (And, Or, Iff, Forall, Exists, Equals,
Set, InSet, NotInSet, SubsetEq, CartExp, InClass)
from proveit.numbers import NaturalPos, Complex, zero, one, two
from proveit.numbers import Neg, Mult, frac, sqrt, Bit, BinarySequence
from proveit.linear_algebra import (
LinMap, VecAdd, VecNeg, VecZero, MatrixSpace, MatrixMult, ScalarMult,
HilbertSpaces, Hspace, InnerProd, TensorProd)
from proveit.physics.quantum import (
Bra, Ket, ket0, ket1, ket_plus, ket_minus, Qmult,
psi, varphi, ket_psi, ket_varphi, bra_varphi,
var_ket_psi, var_ket_varphi, var_ket_v, NumBra, NumKet)
from proveit.physics.quantum.algebra import QmultCodomain
%begin axioms
Define basis kets¶
ket_zero_def = Equals(ket0, ExprTuple(one, zero))
ket_one_def = Equals(ket1, ExprTuple(zero, one))
ket_plus_def = Equals(
ket_plus, ScalarMult(frac(one, sqrt(two)),
VecAdd(ket0, ket1)))
ket_minus_def = Equals(
ket_minus, ScalarMult(frac(one, sqrt(two)),
VecAdd(ket0, VecNeg(ket1))))
num_ket_def = Forall(
k, Forall(a_1_to_k,
Equals(NumKet(BinarySequence(a_1_to_k), k),
TensorProd(ExprRange(i, Ket(a_i), one, k))),
domain=Bit),
domain=NaturalPos)
Define the bra notation from the corresponding ket¶
A 'bra', such as $\langle \psi \rvert$, defines a linear map from a Hilbert space to a complex scalar via the inner product of the Hilbert space.
bra_def = Forall(
Hspace,
Forall(
varphi, Equals(
bra_varphi,
Lambda(var_ket_psi,
Conditional(InnerProd(ket_varphi, var_ket_psi),
InSet(var_ket_psi, Hspace)))),
condition=InSet(ket_varphi, Hspace)),
domain=HilbertSpaces)
Qmult and QmultCodomain¶
A Qmult Operation can string together a sequences of quantum operators and/or kets. Properly defined, a ket is a vector in a Hilbert space and a quantum operator acts (under Qmult) as a linear map from a Hilbert space to a Hilbert space or a complex number. The latter is called a bra.
The result of a Qmult Operation, if and only if it is well-formed (in a valid sequence), will be in the QmultCodomain class which includes all vectors in any vector space over complex numbers or linear maps between vectors of vector spaces over complex numbers:
Forall(x, Equals(InClass(x, QmultCodomain),
Or(Exists(Hspace, InSet(x, Hspace),
domain=HilbertSpaces),
Exists((Hspace, X), InSet(x, LinMap(Hspace, X)),
domain=HilbertSpaces))
.with_wrap_after_operator()))
One important note is that we assume, here, that the complex numbers are, as a trivial special case, a Hilbert space: $\mathbb{C} \underset{{\scriptscriptstyle c}}{\in} \textrm{HilbertSpaces}$.
When a Qmult has a single ket operand (or complex number, as a special case), it simply represents that ket.
qmult_of_ket = Forall(
Hspace, Forall(var_ket_psi,
Equals(Qmult(var_ket_psi), var_ket_psi),
domain=Hspace),
domain=HilbertSpaces)
When a Qmult has a single quantum operator or bra operand, it represents the corresponding linear mapping of the operand and we format it as the operand wrapped in square brackets.
The corresponding linear map for the matrix performs the matrix multiplication:
qmult_of_matrix = Forall(
(m, n), Forall(M, Equals(Qmult(M),
Lambda(x, Conditional(
MatrixMult(M, x),
InSet(x, CartExp(Complex, n))))),
domain=MatrixSpace(Complex, m, n)),
domain=NaturalPos)
The corresponding linear map for a linear map is the linear map itself:
qmult_of_linmap = Forall(
(Hspace, X), Forall(A, Equals(Qmult(A), A),
domain=LinMap(Hspace, X)),
domain=HilbertSpaces)
A Qmult of a bra or operator applied to a ket is the application of the corresponding mapping (from Hilbert space to a c-number or Hilbert space to Hilbert space):
qmult_op_ket = Forall(
(Hspace, X), Forall(
A, Forall(var_ket_psi, Equals(Qmult(A, var_ket_psi),
Function(Qmult(A), var_ket_psi)),
domain=Hspace),
condition=InSet(Qmult(A),
LinMap(Hspace, X))),
domain=HilbertSpaces)
We define the Qmult of two operators as the composition of the operators:
qmult_op_op = Forall(
(Hspace, X, Y), Forall(
(A, B), Equals(Qmult(A, B),
Composition(Qmult(A),
Qmult(B))),
conditions=[InSet(Qmult(A), LinMap(X, Y)),
InSet(Qmult(B), LinMap(Hspace, X))]),
domain=HilbertSpaces)
We define the Qmult of two kets as the tensor product of the kets.
qmult_ket_ket = Forall(
Hspace, Forall(
(var_ket_psi, var_ket_varphi),
Equals(
Qmult(var_ket_psi, var_ket_varphi),
TensorProd(var_ket_psi, var_ket_varphi)),
domain=Hspace),
domain=HilbertSpaces)
We define the Qmult of a ket followed by a bra as the outer product mapping which is consistent with Qmult associativity:
qmult_ket_bra = Forall(
(Hspace, X), Forall(
var_ket_psi, Forall(
varphi, Equals(
Qmult(var_ket_psi, bra_varphi),
Lambda(var_ket_v, Conditional(
ScalarMult(Qmult(bra_varphi, var_ket_v),
var_ket_psi),
InSet(var_ket_v, Hspace)))),
condition=InSet(Ket(varphi), Hspace)),
domain=X),
domain=HilbertSpaces)
We define the Qmult of a c-number with anything, with the c-number on either side, as the scalar multiplication of the c number with the other operand:
qmult_complex_complex = Forall((a, b), Equals(Qmult(a, b),
Mult(a, b)),
domain=Complex)
qmult_complex_left = Forall(
c, Forall(X, Equals(Qmult(c, X), ScalarMult(c, X)),
domain=QmultCodomain),
domain=Complex)
qmult_complex_right = Forall(
c, Forall(X, Equals(Qmult(X, c), ScalarMult(c, X)),
domain=QmultCodomain),
domain=Complex)
By the following axiom, we can know that a Qmult only results in an element of its codomain if it is well-formed (the operands are in a valid sequence of op-ket, ket-bra, op-op, complex-any, or any-complex):
qmult_in_codomain_only_if_valid = Forall(
(A, B), Exists(
(Hspace, X, Y),
InSet(ExprTuple(Qmult(A), Qmult(B)),
Set(ExprTuple(LinMap(Hspace, X), Hspace),
ExprTuple(X, LinMap(Hspace, Complex)),
ExprTuple(LinMap(X, Y), LinMap(Hspace, X)),
ExprTuple(Complex, QmultCodomain),
ExprTuple(QmultCodomain, Complex))),
domain=HilbertSpaces),
condition=InClass(Qmult(A, B),
QmultCodomain))
A Qmult of multiple operands is defined as the binary expansion:
multi_qmult_def = \
Forall(m, Forall((A_1_to_m, B),
Equals(Qmult(A_1_to_m, B),
Qmult(Qmult(A_1_to_m), B))
.with_wrap_after_operator()),
domain=NaturalPos)
%end axioms