# Axioms for the theory of proveit.physics.quantum.circuits¶

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, l, A, B, S
from proveit.logic import Forall, Equals
from proveit.numbers import one, NaturalPos
from proveit.core_expr_types.expr_arrays import (
A11_to_Akl, B11_to_Bkl, A11_to_Akl_varray, B11_to_Bkl_varray)
from proveit.physics.quantum.circuits import (
Input, Output, Measure, Gate, MultiQubitElem)
from proveit.physics.quantum.circuits import circuit_Akl, circuit_Bkl

In [2]:
%begin axioms

Defining axioms for theory 'proveit.physics.quantum.circuits'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions


Quantum circuits of the same dimension are equal if and only if their contents are equal.

In [3]:
qcircuit_eq_def = Forall(
(k, l), Forall(
(A11_to_Akl, B11_to_Bkl),
Equals(Equals(circuit_Akl, circuit_Bkl),
Equals(A11_to_Akl_varray, B11_to_Bkl_varray))
.with_wrap_after_operator()).with_wrapping(),
domain=NaturalPos)

qcircuit_eq_def:

Quantum circuit inputs/outputs are equal only when their output states are equal

In [4]:
qcircuit_input_eq_def = Forall(
(A, B), Equals(Equals(Input(A), Input(B)),
Equals(A, B)))

qcircuit_input_eq_def:
In [5]:
qcircuit_output_eq_def = Forall(
(A, B), Equals(Equals(Output(A), Output(B)),
Equals(A, B)))

qcircuit_output_eq_def:
In [6]:
qcircuit_input_part_eq_def = Forall(
k, Forall(
(A, B, S), Equals(Equals(MultiQubitElem(Input(A, part=k),
targets=S),
MultiQubitElem(Input(B, part=k),
targets=S)),
Equals(A, B))),
domain=NaturalPos)

qcircuit_input_part_eq_def:
In [7]:
qcircuit_output_part_eq_def = Forall(
k, Forall(
(A, B, S), Equals(Equals(MultiQubitElem(Output(A, part=k),
targets=S),
MultiQubitElem(Output(B, part=k),
targets=S)),
Equals(A, B))),
domain=NaturalPos)

qcircuit_output_part_eq_def:
In [8]:
%end axioms

These axioms may now be imported from the theory package: proveit.physics.quantum.circuits