logo

Theorem circuit_equiv_qubit_permutation of type Forall

from the theory of proveit.physics.quantum.circuits

see dependencies

In [1]:
import proveit
# Automation is not needed when only building an expression:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%load_theorem_expr # Load the stored theorem expression as 'stored_expr'
# import the special expression
from proveit.physics.quantum.circuits import circuit_equiv_qubit_permutation
In [2]:
# check that the built expression is the same as the stored expression
assert circuit_equiv_qubit_permutation.expr == stored_expr
assert circuit_equiv_qubit_permutation.expr._style_id == stored_expr._style_id
print("Passed sanity check: circuit_equiv_qubit_permutation matches stored_expr")

Passed sanity check: circuit_equiv_qubit_permutation matches stored_expr
In [3]:
# Show the LaTeX representation of the expression for convenience if you need it.
print(stored_expr.latex())

\forall_{k, m, n \in \mathbb{N}^+}~\left[\forall_{p \in \textrm{Perm}\left(\{1~\ldotp \ldotp~k\}\right)}~\left[\begin{array}{l}\forall_{A_{1, 1}, A_{1, 2}, \ldots, A_{1, m}, A_{2, 1}, A_{2, 2}, \ldots, A_{2, m}, \ldots\ldots, A_{k, 1}, A_{k, 2}, \ldots, A_{k, m}, R_{1, 1}, R_{1, 2}, \ldots, R_{1, m}, R_{2, 1}, R_{2, 2}, \ldots, R_{2, m}, \ldots\ldots, R_{k, 1}, R_{k, 2}, \ldots, R_{k, m}, B_{1, 1}, B_{1, 2}, \ldots, B_{1, n}, B_{2, 1}, B_{2, 2}, \ldots, B_{2, n}, \ldots\ldots, B_{k, 1}, B_{k, 2}, \ldots, B_{k, n}, S_{1, 1}, S_{1, 2}, \ldots, S_{1, n}, S_{2, 1}, S_{2, 2}, \ldots, S_{2, n}, \ldots\ldots, S_{k, 1}, S_{k, 2}, \ldots, S_{k, n}}~\\
\left(\begin{array}{c} \begin{array}{l} \left(\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
& \gate{A_{1, 1}~\mbox{on}~R_{1, 1}} \qwx[1] & \gate{A_{2, 1}~\mbox{on}~R_{2, 1}} \qwx[1] & \gate{\cdots} \qwx[1] & \gate{A_{m, 1}~\mbox{on}~R_{m, 1}} \qwx[1] & \qw \\
& \gate{A_{1, 2}~\mbox{on}~R_{1, 2}} \qwx[1] & \gate{A_{2, 2}~\mbox{on}~R_{2, 2}} \qwx[1] & \gate{\cdots} \qwx[1] & \gate{A_{m, 2}~\mbox{on}~R_{m, 2}} \qwx[1] & \qw \\
& \gate{\vdots} \qwx[1] & \gate{\vdots} \qwx[1] & \gate{\ddots} \qwx[1] & \gate{\vdots} \qwx[1] & \qw \\
& \gate{A_{1, k}~\mbox{on}~R_{1, k}} & \gate{A_{2, k}~\mbox{on}~R_{2, k}} & \gate{\cdots} & \gate{A_{m, k}~\mbox{on}~R_{m, k}} & \qw
} \end{array}\right) \cong \left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
& \gate{B_{1, 1}~\mbox{on}~S_{1, 1}} \qwx[1] & \gate{B_{2, 1}~\mbox{on}~S_{2, 1}} \qwx[1] & \gate{\cdots} \qwx[1] & \gate{B_{n, 1}~\mbox{on}~S_{n, 1}} \qwx[1] & \qw \\
& \gate{B_{1, 2}~\mbox{on}~S_{1, 2}} \qwx[1] & \gate{B_{2, 2}~\mbox{on}~S_{2, 2}} \qwx[1] & \gate{\cdots} \qwx[1] & \gate{B_{n, 2}~\mbox{on}~S_{n, 2}} \qwx[1] & \qw \\
& \gate{\vdots} \qwx[1] & \gate{\vdots} \qwx[1] & \gate{\ddots} \qwx[1] & \gate{\vdots} \qwx[1] & \qw \\
& \gate{B_{1, k}~\mbox{on}~S_{1, k}} & \gate{B_{2, k}~\mbox{on}~S_{2, k}} & \gate{\cdots} & \gate{B_{n, k}~\mbox{on}~S_{n, k}} & \qw
} \end{array}\right)\right) =  \\ \left(\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
& \gate{A_{p\left(1\right), 1}~\mbox{on}~p^{\leftarrow}\left(R_{p\left(1\right), 1}\right)} \qwx[1] & \gate{A_{p\left(2\right), 1}~\mbox{on}~p^{\leftarrow}\left(R_{p\left(2\right), 1}\right)} \qwx[1] & \gate{\cdots} \qwx[1] & \gate{A_{p\left(m\right), 1}~\mbox{on}~p^{\leftarrow}\left(R_{p\left(m\right), 1}\right)} \qwx[1] & \qw \\
& \gate{A_{p\left(1\right), 2}~\mbox{on}~p^{\leftarrow}\left(R_{p\left(1\right), 2}\right)} \qwx[1] & \gate{A_{p\left(2\right), 2}~\mbox{on}~p^{\leftarrow}\left(R_{p\left(2\right), 2}\right)} \qwx[1] & \gate{\cdots} \qwx[1] & \gate{A_{p\left(m\right), 2}~\mbox{on}~p^{\leftarrow}\left(R_{p\left(m\right), 2}\right)} \qwx[1] & \qw \\
& \gate{\vdots} \qwx[1] & \gate{\vdots} \qwx[1] & \gate{\ddots} \qwx[1] & \gate{\vdots} \qwx[1] & \qw \\
& \gate{A_{p\left(1\right), k}~\mbox{on}~p^{\leftarrow}\left(R_{p\left(1\right), k}\right)} & \gate{A_{p\left(2\right), k}~\mbox{on}~p^{\leftarrow}\left(R_{p\left(2\right), k}\right)} & \gate{\cdots} & \gate{A_{p\left(m\right), k}~\mbox{on}~p^{\leftarrow}\left(R_{p\left(m\right), k}\right)} & \qw
} \end{array}\right) \cong \left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
& \gate{B_{p\left(1\right), 1}~\mbox{on}~p^{\leftarrow}\left(S_{p\left(1\right), 1}\right)} \qwx[1] & \gate{B_{p\left(2\right), 1}~\mbox{on}~p^{\leftarrow}\left(S_{p\left(2\right), 1}\right)} \qwx[1] & \gate{\cdots} \qwx[1] & \gate{B_{p\left(n\right), 1}~\mbox{on}~p^{\leftarrow}\left(S_{p\left(n\right), 1}\right)} \qwx[1] & \qw \\
& \gate{B_{p\left(1\right), 2}~\mbox{on}~p^{\leftarrow}\left(S_{p\left(1\right), 2}\right)} \qwx[1] & \gate{B_{p\left(2\right), 2}~\mbox{on}~p^{\leftarrow}\left(S_{p\left(2\right), 2}\right)} \qwx[1] & \gate{\cdots} \qwx[1] & \gate{B_{p\left(n\right), 2}~\mbox{on}~p^{\leftarrow}\left(S_{p\left(n\right), 2}\right)} \qwx[1] & \qw \\
& \gate{\vdots} \qwx[1] & \gate{\vdots} \qwx[1] & \gate{\ddots} \qwx[1] & \gate{\vdots} \qwx[1] & \qw \\
& \gate{B_{p\left(1\right), k}~\mbox{on}~p^{\leftarrow}\left(S_{p\left(1\right), k}\right)} & \gate{B_{p\left(2\right), k}~\mbox{on}~p^{\leftarrow}\left(S_{p\left(2\right), k}\right)} & \gate{\cdots} & \gate{B_{p\left(n\right), k}~\mbox{on}~p^{\leftarrow}\left(S_{p\left(n\right), k}\right)} & \qw
} \end{array}\right)\right) \end{array} \end{array}\right)\end{array}\right]\right]
In [4]:
stored_expr.style_options()
namedescriptiondefaultcurrent valuerelated methods
with_wrappingIf 'True', wrap the Expression after the parametersNoneNone/False('with_wrapping',)
condition_wrappingWrap 'before' or 'after' the condition (or None).NoneNone/False('with_wrap_after_condition', 'with_wrap_before_condition')
wrap_paramsIf 'True', wraps every two parameters AND wraps the Expression after the parametersNoneNone/False('with_params',)
justificationjustify to the 'left', 'center', or 'right' in the array cellscentercenter('with_justification',)
In [5]:
# display the expression information
stored_expr.expr_info()
 core typesub-expressionsexpression
0Operationoperator: 21
operand: 2
1ExprTuple2
2Lambdaparameters: 3
body: 4
3ExprTuple89, 73, 75
4Conditionalvalue: 5
condition: 6
5Operationoperator: 21
operand: 10
6Operationoperator: 8
operands: 9
7ExprTuple10
8Literal
9ExprTuple11, 12, 13
10Lambdaparameter: 123
body: 14
11Operationoperator: 23
operands: 15
12Operationoperator: 23
operands: 16
13Operationoperator: 23
operands: 17
14Conditionalvalue: 18
condition: 19
15ExprTuple89, 20
16ExprTuple73, 20
17ExprTuple75, 20
18Operationoperator: 21
operand: 25
19Operationoperator: 23
operands: 24
20Literal
21Literal
22ExprTuple25
23Literal
24ExprTuple123, 26
25Lambdaparameters: 27
body: 28
26Operationoperator: 29
operand: 37
27ExprTuple31, 32, 33, 34
28Operationoperator: 35
operands: 36
29Literal
30ExprTuple37
31ExprRangelambda_map: 38
start_index: 88
end_index: 89
32ExprRangelambda_map: 39
start_index: 88
end_index: 89
33ExprRangelambda_map: 40
start_index: 88
end_index: 89
34ExprRangelambda_map: 41
start_index: 88
end_index: 89
35Literal
36ExprTuple42, 43
37Operationoperator: 44
operands: 45
38Lambdaparameter: 125
body: 46
39Lambdaparameter: 125
body: 47
40Lambdaparameter: 125
body: 48
41Lambdaparameter: 125
body: 49
42Operationoperator: 51
operands: 50
43Operationoperator: 51
operands: 52
44Literal
45ExprTuple88, 89
46ExprRangelambda_map: 53
start_index: 88
end_index: 73
47ExprRangelambda_map: 54
start_index: 88
end_index: 73
48ExprRangelambda_map: 55
start_index: 88
end_index: 75
49ExprRangelambda_map: 56
start_index: 88
end_index: 75
50ExprTuple57, 58
51Literal
52ExprTuple59, 60
53Lambdaparameter: 122
body: 100
54Lambdaparameter: 122
body: 101
55Lambdaparameter: 122
body: 102
56Lambdaparameter: 122
body: 103
57Operationoperator: 64
operands: 61
58Operationoperator: 64
operands: 62
59Operationoperator: 64
operands: 63
60Operationoperator: 64
operands: 65
61ExprTuple66
62ExprTuple67
63ExprTuple68
64Literal
65ExprTuple69
66ExprRangelambda_map: 70
start_index: 88
end_index: 73
67ExprRangelambda_map: 71
start_index: 88
end_index: 75
68ExprRangelambda_map: 72
start_index: 88
end_index: 73
69ExprRangelambda_map: 74
start_index: 88
end_index: 75
70Lambdaparameter: 125
body: 76
71Lambdaparameter: 125
body: 77
72Lambdaparameter: 125
body: 78
73Variable
74Lambdaparameter: 125
body: 79
75Variable
76ExprTuple80
77ExprTuple81
78ExprTuple82
79ExprTuple83
80ExprRangelambda_map: 84
start_index: 88
end_index: 89
81ExprRangelambda_map: 85
start_index: 88
end_index: 89
82ExprRangelambda_map: 86
start_index: 88
end_index: 89
83ExprRangelambda_map: 87
start_index: 88
end_index: 89
84Lambdaparameter: 122
body: 90
85Lambdaparameter: 122
body: 91
86Lambdaparameter: 122
body: 92
87Lambdaparameter: 122
body: 94
88Literal
89Variable
90Operationoperator: 98
operands: 95
91Operationoperator: 98
operands: 96
92Operationoperator: 98
operands: 97
93ExprTuple122
94Operationoperator: 98
operands: 99
95NamedExprselement: 100
targets: 101
96NamedExprselement: 102
targets: 103
97NamedExprselement: 104
targets: 105
98Literal
99NamedExprselement: 106
targets: 107
100IndexedVarvariable: 109
indices: 108
101IndexedVarvariable: 118
indices: 108
102IndexedVarvariable: 111
indices: 108
103IndexedVarvariable: 119
indices: 108
104IndexedVarvariable: 109
indices: 120
105Operationoperator: 112
operand: 114
106IndexedVarvariable: 111
indices: 120
107Operationoperator: 112
operand: 117
108ExprTuple125, 122
109Variable
110ExprTuple114
111Variable
112Operationoperator: 115
operand: 123
113ExprTuple117
114IndexedVarvariable: 118
indices: 120
115Literal
116ExprTuple123
117IndexedVarvariable: 119
indices: 120
118Variable
119Variable
120ExprTuple121, 122
121Operationoperator: 123
operand: 125
122Variable
123Variable
124ExprTuple125
125Variable