Theorems (or conjectures) for the theory of proveit.physics.quantum.circuits

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 defaults
#defaults.automation = True # Hack for ExprRange simplification to go through

from proveit import a, b, i, j, k, l, m, n, p, t, A, B, C, N, P, Q, S, U, X
from proveit import Function, Lambda, ExprRange, var_range, IndexedVar, VertExprArray
from proveit.core_expr_types import (
    a_1_to_k, b_1_to_k, c_1_to_k, i_1_to_m, j_1_to_m, n_1_to_m,
    A_1_to_j, A_1_to_m, B_1_to_k, B_1_to_m, B_1_to_n, C_1_to_l, 
    D_1_to_m, U_1_to_i, U_1_to_m, V_1_to_j)
from proveit.core_expr_types.expr_arrays import (
    A11_to_Akl, A11_to_Akm, B11_to_Bkl, B11_to_Bkm, B11_to_Bkn, 
    C11_to_Clm, C11_to_Ckm, D11_to_Dkn,
    R11_to_Rkm, S11_to_Skm, S11_to_Skn, T11_to_Tlm, T11_to_Tkm, U11_to_Ukn, V11_to_Vkm,
    A11_to_Akl_varray, B11_to_Bkl_varray)
from proveit.logic import (And, Implies, Iff, Forall, Equals, NotEquals,
                           Set, InSet, SetOfAll, EmptySet, InClass,
                           Bijections)
from proveit.numbers import (
    Natural, NaturalPos, Interval, Abs, Mult, Exp, sqrd, zero, one, two, exp2pi_i)
from proveit.linear_algebra import ScalarMult, MatrixMult, TensorProd, Unitary
from proveit.statistics import Prob, ProbOfAll, prob_domain, SampleSpaces
from proveit.physics.quantum import (
    QubitSpace,SPACE, var_ket_psi, varphi, nk_ket_domain, m_ket_domain, var_ket_u, 
    normalized_var_ket_u, var_ket_v, Z, m_bit_interval, 
    var_ket_psi, l_ket_domain, m_ket_domain, normalized_var_ket_psi,
    RegisterU)
from proveit.physics.quantum import (
    Qmult, Ket, Bra, NumKet, NumBra)
from proveit.physics.quantum.circuits import (
    Qcircuit, QcircuitEquiv, Gate, MultiQubitElem, Input, Output, Measure,
    multi_input_entries, multi_output_entries)
from proveit.physics.quantum.circuits import (
    unitary_gate_op, qubit_meas, register_meas,
    circuit_Am, circuit_Bn, circuit_Bk, circuit_Dm,
    circuit_AjBkCl, circuit_AjDmCl,
    circuit_aUb, circuit_aU, circuit_Ua, circuit_Ub, circuit_b,
    circuit_Akl, circuit_Bkl,
    circuit_Akm, circuit_Bkm, circuit_Bkn, circuit_Ckm, circuit_Dkn,
    circuit_permuted_Akm, circuit_permuted_Bkn,
    circuit_AkClm, circuit_BkClm, no_1tok_in_Ts,
    circuit_compressed_inputAm, circuit_compressed_outputAm,
    circuit_expanded_inputBm, circuit_expanded_outputBm,
    input_Ak_nk, output_Ak_nk, N_0_to_m, N_m, each_Nk_is_partial_sum,
    consolidated_input_A_1_to_m, consolidated_output_A_1_to_m,
    circuit_Ui_psi_m, circuit_psi_m_Vj, circuit_Ui_Vj,
    circuit__u_Akl_v, circuit__psi_m__u_Akl_v, circuit__u_Akl_v__psi_m,
    phase_kickback_circuit, phase_kickback_on_register_circuit
    )
#from proveit.physics.quantum.circuit import CircuitEquiv
#from proveit.physics.quantum.circuits import (
#    circuit_aUVc, circuit_aUb, circuit_bVc, 
#    circuit_A_detailed, circuit_B_detailed, permuted_circuit_A, permuted_circuit_B,
#    circuit_B, circuit_D, circuit_ABCvert, circuit_ADCvert
#)

#defaults.automation = False # Hack for ExprRange simplification to go through
%begin theorems
#defaults.automation = True # Hack for ExprRange simplification to go through
#print("We need automation to simplify ExprRanges in Qcircuits")

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

MultiQubitElem unary reduction

# for use in reducing a MultiQubitElem to a gate within a Circuit.
unary_multi_qubit_elem_reduction = Forall(
    X, Equals(MultiQubitElem(X, EmptySet), X))

unary_multi_qubit_elem_reduction (conjecture without proof):

unary_multi_gate_reduction = Forall(
    A, Forall(
        k, Equals(MultiQubitElem(Gate(A, part=one), 
                                 Interval(k, k)),                   
                  Gate(A)),
        domain=NaturalPos))

unary_multi_gate_reduction (conjecture without proof):

unary_multi_input_reduction = Forall(
    var_ket_psi, Forall(
        k, Equals(MultiQubitElem(Input(var_ket_psi, part=one), 
                                 Interval(k, k)),                   
                  Input(var_ket_psi)),
        domain=NaturalPos))

unary_multi_input_reduction (conjecture without proof):

unary_multi_output_reduction = Forall(
    var_ket_psi, Forall(
        k, Equals(MultiQubitElem(Output(var_ket_psi, part=one), 
                                 Interval(k, k)),                   
                  Output(var_ket_psi)),
        domain=NaturalPos))

unary_multi_output_reduction (conjecture without proof):

unary_multi_meas_reduction = Forall(
    B, Forall(
        k, Equals(MultiQubitElem(Measure(B, part=one), 
                                 Interval(k, k)),                   
                  Measure(B)),
        domain=NaturalPos))

unary_multi_meas_reduction (conjecture without proof):

Unitary gate

unitary_gate_operation = Forall(m, Forall((U, var_ket_psi), Equals(Prob(unitary_gate_op), one),
                                   domains=(RegisterU(m), m_ket_domain)),
                                domain=NaturalPos)

unitary_gate_operation (conjecture without proof):

Equality of quantum circuit elements

qcircuit_input_eq = Forall(
    (A, B), Equals(Input(A), Input(B)), condition=Equals(A, B))

qcircuit_input_eq (conjecture without proof):

qcircuit_input_neq = Forall(
    (A, B), NotEquals(Input(A), Input(B)), condition=NotEquals(A, B))

qcircuit_input_neq (conjecture without proof):

qcircuit_output_eq = Forall(
    (A, B), Equals(Output(A), Output(B)), condition=Equals(A, B))

qcircuit_output_eq (conjecture without proof):

qcircuit_output_neq = Forall(
    (A, B), NotEquals(Output(A), Output(B)), condition=NotEquals(A, B))

qcircuit_output_neq (conjecture without proof):

qcircuit_input_part_eq = Forall(
    k, Forall(
        (A, B, S), Equals(MultiQubitElem(Input(A, part=k), targets=S),
                          MultiQubitElem(Input(B, part=k), targets=S)),
        condition=Equals(A, B)),
    domain=NaturalPos)

qcircuit_input_part_eq (conjecture without proof):

qcircuit_input_part_neq = Forall(
    k, Forall(
        (A, B, S), NotEquals(MultiQubitElem(Input(A, part=k), targets=S),
                             MultiQubitElem(Input(B, part=k), targets=S)),
        condition=NotEquals(A, B)),
    domain=NaturalPos)

qcircuit_input_part_neq (conjecture without proof):

qcircuit_output_part_eq = Forall(
    k, Forall(
        (A, B, S), Equals(MultiQubitElem(Output(A, part=k), targets=S),
                          MultiQubitElem(Output(B, part=k), targets=S)),
        condition=Equals(A, B)),
    domain=NaturalPos)

qcircuit_output_part_eq (conjecture without proof):

qcircuit_output_part_neq = Forall(
    k, Forall(
        (A, B, S), NotEquals(MultiQubitElem(Output(A, part=k), targets=S),
                             MultiQubitElem(Output(B, part=k), targets=S)),
        condition=NotEquals(A, B)),
    domain=NaturalPos)

qcircuit_output_part_neq (conjecture without proof):

qcircuit_eq = Forall(
    (k, l), Forall(
        (A11_to_Akl, B11_to_Bkl),
        Implies(Equals(A11_to_Akl_varray, B11_to_Bkl_varray),
                Equals(circuit_Akl, circuit_Bkl))
        .with_wrap_after_operator()).with_wrapping(),
    domain=NaturalPos)

qcircuit_eq (conjecture without proof):

qcircuit_neq = Forall(
    (k, l), Forall(
        (A11_to_Akl, B11_to_Bkl),
        Implies(NotEquals(A11_to_Akl_varray, B11_to_Bkl_varray),
                NotEquals(circuit_Akl, circuit_Bkl))
        .with_wrap_after_operator()).with_wrapping(),
    domain=NaturalPos)

qcircuit_neq (conjecture without proof):

Quantum measurement probabilities and sample spaces

(These may need to be promoted to axioms.)

born_rule_on_qubit = Forall(
    (var_ket_psi, b), 
    Equals(Prob(qubit_meas),
           sqrd(Abs(Qmult(Bra(b), var_ket_psi)))),
    domains=(QubitSpace, Set(zero, one)),
    condition=normalized_var_ket_psi)

born_rule_on_qubit (conjecture without proof):

born_rule_on_register = Forall(
    m, Forall(
        n, Forall(var_ket_psi, 
                  Equals(Prob(register_meas),
                         sqrd(Abs(Qmult(NumBra(n, m), var_ket_psi)))),
                  domain=m_ket_domain,
                  condition=normalized_var_ket_psi),
        domain=m_bit_interval),
    domain=NaturalPos)

born_rule_on_register (conjecture without proof):

qubit_meas_sample_space = Forall(
    var_ket_psi, InClass(SetOfAll(b, qubit_meas, domain=Set(zero, one)),
                         SampleSpaces),
    domain=QubitSpace, condition=normalized_var_ket_psi)

qubit_meas_sample_space (conjecture without proof):

qubit_meas_bijection = Forall(
    var_ket_psi, 
    InSet(Lambda(b, qubit_meas),
          Bijections(Set(zero, one), 
                     SetOfAll(b, qubit_meas, domain=Set(zero, one))))
    .with_wrap_after_operator(),
    domain=QubitSpace, condition=normalized_var_ket_psi)

qubit_meas_bijection (conjecture without proof):

register_meas_sample_space = Forall(
    (m, var_ket_psi), InClass(SetOfAll(n, register_meas, 
                                       domain=m_bit_interval),
                              SampleSpaces),
    domains=(NaturalPos, m_ket_domain),
    condition=normalized_var_ket_psi)

register_meas_sample_space (conjecture without proof):

register_meas_bijection = Forall(
    (m, var_ket_psi), 
    InSet(Lambda(n, register_meas),
          Bijections(m_bit_interval,
                     SetOfAll(n, register_meas, domain=m_bit_interval)))
    .with_wrap_after_operator(),
    domains=(NaturalPos, m_ket_domain),
    condition=normalized_var_ket_psi)

register_meas_bijection (conjecture without proof):

Circuit equivalences and uses

Circuits are equivalent when the function in the same way -- they have the same output for any possible input.

equiv_symmetry = Forall(
    (A, B), Equals(QcircuitEquiv(B, A), QcircuitEquiv(A, B)))

equiv_symmetry (conjecture without proof):

equiv_reversal= Forall(
    (A, B), QcircuitEquiv(B, A), condition=QcircuitEquiv(A, B))

equiv_reversal (conjecture without proof):

equiv_transitivity = Forall(
    (A, B, C), QcircuitEquiv(A, C), 
    conditions=[QcircuitEquiv(A, B), QcircuitEquiv(B, C)])

equiv_transitivity (conjecture without proof):

Circuits are equivalent when they are the same except for a temporal section which is equivalent. The up/down arrows denote entire columns which may be instantiated with ExprTuples.

circuit_equiv_temporal_sub = Forall(
    (j, k, l, m), Forall(
        (A_1_to_j, B_1_to_k, C_1_to_l, D_1_to_m),
        Implies(QcircuitEquiv(circuit_Bk, circuit_Dm),
                QcircuitEquiv(circuit_AjBkCl, circuit_AjDmCl).with_wrap_before_operator())
        .with_wrap_after_operator()).with_wrapping(),
    domain=Natural)

circuit_equiv_temporal_sub (conjecture without proof):

If a quantum circuit is "true", meaning that its inputs and outputs have all been specified and are consistent, then an equivalent quantum circuit is also true. Note that a circuit cannot be provably "true" if it has any non-specified inputs or outputs.

prob_eq_via_equiv = Forall((A, B), Equals(Prob(A), Prob(B)), 
                           conditions=QcircuitEquiv(A, B))

prob_eq_via_equiv (conjecture without proof):

rhs_prob_via_equiv = Forall(Q, Forall((A, B), Function(Q, Prob(B)), 
                                      conditions=(Function(Q, Prob(A)),
                                                  QcircuitEquiv(A, B))))

rhs_prob_via_equiv (conjecture without proof):

lhs_prob_via_equiv = Forall(Q, Forall((A, B), Function(Q, Prob(A)), 
                                      conditions=(Function(Q, Prob(B)),
                                                  QcircuitEquiv(A, B))))

lhs_prob_via_equiv (conjecture without proof):

A quantum circuit applied to some input is equivalent to its output in the form of a circuit input. That is, if a circuit produces some output, it is interchangable with that output when fed as an input in a broader circuit.

circuit_output_equiv = Forall(
    (k, m), Forall(
        (a, b, U_1_to_m),
        Implies(circuit_aUb, 
                QcircuitEquiv(circuit_aU, circuit_b))),
    domain=NaturalPos)

circuit_output_equiv (conjecture without proof):

Circuit equivalence is preserved under the permutation of qubit row indices.

from proveit import Literal, Function
circuit_equiv_qubit_permutation = Forall(
    (k, m, n),
    Forall(p,
           Forall((A11_to_Akm, R11_to_Rkm, B11_to_Bkn, S11_to_Skn),
                  Equals(QcircuitEquiv(circuit_Akm, circuit_Bkn),
                         QcircuitEquiv(circuit_permuted_Akm, circuit_permuted_Bkn))
                  .with_wrap_after_operator()).with_wrapping(),
           domain=Function(Literal('Perm', latex_format=r'\textrm{Perm}'),
                           Interval(one, k))), # TODO, ADD Perm\n",
    domain=NaturalPos)

circuit_equiv_qubit_permutation (conjecture without proof):

circuit_equiv_qubit_permutation.instance_expr.instance_expr.instance_expr.operands

%%latex
$(x_1, ..., x_n) \\
p^{\leftarrow}((x_1, ..., x_n)) = (p^{-1}(x_1), ..., p^{-1}(x_n)) \\
p^{\leftarrow}(S) = \{y~|~p(y) \in S\}
$
U on (3, 1, 2)

$(x_1, ..., x_n) \\ p^{\leftarrow}((x_1, ..., x_n)) = (p^{-1}(x_1), ..., p^{-1}(x_n)) \\ p^{\leftarrow}(S) = \{y~|~p(y) \in S\} $ U on (3, 1, 2)

Circuits are equivalent when they are the same except for a top section which is equivalent as long as there are no multi-gate that cross the top and bottom sections and there is no control or swap across the sections. There could be a control in the top section with a target in the bottom section as long as circuit equivalence accounts for control on external targets as part of the output that must all be consistent for each possible input.

circuit_equiv_top_sub= Forall(
    (k, l, m),
    Forall((A11_to_Akm, B11_to_Bkm, C11_to_Clm),
           Forall((R11_to_Rkm, S11_to_Skm, T11_to_Tlm),
                  Implies(QcircuitEquiv(circuit_Akm, circuit_Bkm),
                          QcircuitEquiv(circuit_AkClm, circuit_BkClm))
                  .with_wrap_after_operator(),
                  conditions=no_1tok_in_Ts)
           .with_wrap_before_condition().with_wrapping())
    .with_wrapping(),
    domain=NaturalPos)

circuit_equiv_top_sub (conjecture without proof):

Circuit inputs and outputs in different forms

input_as_tensor_prod = Forall(
    m, Forall(
        (A, B_1_to_m),
        Iff(QcircuitEquiv(circuit_compressed_inputAm, circuit_expanded_inputBm),
            Equals(A, TensorProd(B_1_to_m)))),
    domain=NaturalPos)

input_as_tensor_prod (conjecture without proof):

output_as_tensor_prod = Forall(
    m, Forall(
        (A, B_1_to_m),
        Iff(QcircuitEquiv(circuit_compressed_outputAm, circuit_expanded_outputBm),
            Equals(A, TensorProd(B_1_to_m)))),
    domain=NaturalPos)

output_as_tensor_prod (conjecture without proof):

consolidated_input_A_1_to_m

input_consolidation = Forall(
    m, Forall(
        n_1_to_m, Forall(
            A_1_to_m,
                Forall(N_0_to_m,
                       QcircuitEquiv(
                           Qcircuit(VertExprArray(
                               [ExprRange(k, input_Ak_nk, one, m)])),
                           Qcircuit(VertExprArray(
                               [ExprRange(k, consolidated_input_A_1_to_m, one, m)]))),
                       domain=Natural, condition=each_Nk_is_partial_sum).with_wrapping(),
            domains=[ExprRange(k, nk_ket_domain, one, m)]).with_wrapping(),
        domain=NaturalPos).with_wrapping(),
    domain=NaturalPos)

input_consolidation (conjecture without proof):

output_consolidation = Forall(
    m, Forall(
        n_1_to_m, Forall(
            A_1_to_m,
                Forall(N_0_to_m,
                       QcircuitEquiv(
                           Qcircuit(VertExprArray(
                               [ExprRange(k, output_Ak_nk, one, m)])),
                           Qcircuit(VertExprArray(
                               [ExprRange(k, consolidated_output_A_1_to_m,
                                          one, m)]))),
                       domain=Natural, condition=each_Nk_is_partial_sum).with_wrapping(),
            domains=[ExprRange(k, nk_ket_domain, one, m)]).with_wrapping(),
        domain=NaturalPos).with_wrapping(),
    domain=NaturalPos)

output_consolidation (conjecture without proof):

Quantum circuit experiment extensions

The probability for a particular experiment outcome is the product of the outcome probabilities for a first part of the experiment and a second part of the experiment given that the state at the end of the first part matches the state at the beginning of the second part so they can happen in succession. If one of these is ideal (probability 1), there is no need to retain intermediate labels.

concat_onto_ideal_expt = Forall(
    (i, j, m), Forall(
        var_ket_psi, 
        Forall(
            (U_1_to_i, V_1_to_j),
            Implies(Equals(Prob(circuit_Ui_psi_m), one),
                    Equals(Prob(circuit_Ui_Vj),
                           Prob(circuit_psi_m_Vj))
                    .with_wrap_after_operator())
            .with_wrap_after_operator()).with_wrapping(),
        domain=m_ket_domain).with_wrapping(),
    domain=NaturalPos).with_wrapping()

concat_onto_ideal_expt (conjecture without proof):

concat_ideal_expt = Forall(
    (i, j, m), Forall(
        var_ket_psi, 
        Forall(
            (U_1_to_i, V_1_to_j),
            Implies(Equals(Prob(circuit_psi_m_Vj), one),
                    Equals(Prob(circuit_Ui_Vj),
                           Prob(circuit_Ui_psi_m))
                    .with_wrap_after_operator())
            .with_wrap_after_operator()).with_wrapping(),
        domain=m_ket_domain).with_wrapping(),
    domain=NaturalPos).with_wrapping()

concat_ideal_expt (conjecture without proof):

If neither experiment is ideal (both have probability less than one), it may not be right to remove the intermediate input/output labels. Let's revisit this later.

# concatenation_prob = Forall(
#     (i, j, m), Forall(
#         n_1_to_m,
#         Forall(
#             A_1_to_m, 
#             Forall(
#                 N_0_to_m, Forall(
#                     (U_1_to_i, V_1_to_j),
#                     Equals(Prob(circuit_Ui_Vj),
#                            Mult(Prob(circuit_Ui_outAm), Prob(circuit_inAm_Vj)))
#                     .with_wrap_after_operator()).with_wrapping(),
#                 domain=Natural, condition=each_Nk_is_partial_sum).with_wrapping(),
#             domains=[ExprRange(k, nk_ket_domain, one, m)]).with_wrapping(),
#         domain=NaturalPos).with_wrapping(),
#     domain=NaturalPos).with_wrapping()

Adding idle qubits is a trivial way to expand a quantum circuit and doesn't affect outcome probabilities.

trivial_expansion_above = Forall(
    (k, l, m), Forall(
        (var_ket_u, var_ket_v), Forall(
            var_ket_psi, Forall(
                A11_to_Akl, 
                Equals(Prob(circuit__u_Akl_v),
                       Prob(circuit__psi_m__u_Akl_v))
                .with_wrap_after_operator()).with_wrapping(),
            domain=m_ket_domain),
        domain=l_ket_domain),
    domain=NaturalPos)

trivial_expansion_above (conjecture without proof):

trivial_expansion_below = Forall(
    (k, l, m), Forall(
        (var_ket_u, var_ket_v), Forall(
            var_ket_psi, Forall(
                A11_to_Akl, 
                Equals(Prob(circuit__u_Akl_v),
                       Prob(circuit__u_Akl_v__psi_m))
                .with_wrap_after_operator()).with_wrapping(),
            domain=m_ket_domain),
        domain=l_ket_domain),
    domain=NaturalPos)

trivial_expansion_below (conjecture without proof):

# Whether this is valid depends upon what we regard as being in Q.C.
# It might not be safe.
# equate_outputs = Forall(
#     (k, m), Forall(
#         (a, b, U_1_to_m),
#         Implies(And(InSet(circuit_Ua, QC), 
#                     InSet(circuit_Ub, QC))
#                 .with_wrap_after_operator(),
#                 Equals(a, b))),
#     domain=NaturalPos)

Useful circuit truths

phase_kickback = Forall(
    m, Forall(
        U, Forall(
            var_ket_u, Forall(
                varphi, Equals(Prob(phase_kickback_circuit), one),
                condition=Equals(Qmult(U, var_ket_u,),
                                 ScalarMult(exp2pi_i(varphi), var_ket_u))),
            domain=m_ket_domain, condition=normalized_var_ket_u),
        domain=Unitary(Exp(two, m))),
    domain=NaturalPos)

phase_kickback (conjecture without proof):

phase_kickbacks_on_register = Forall(
    (m, t), Forall(
        var_range(U, one, t), Forall(
            var_ket_u, Forall(
                var_range(varphi, one, t), 
                Equals(Prob(phase_kickback_on_register_circuit), one),
                conditions=ExprRange(i, Equals(MatrixMult(IndexedVar(U, i), var_ket_u),
                                               ScalarMult(exp2pi_i(IndexedVar(varphi, i)), 
                                                          var_ket_u)),
                                     one, t)).with_wrapping(),
            domain=m_ket_domain, condition=normalized_var_ket_u).with_wrapping(),
        domain=Unitary(Exp(two, m))).with_wrapping(),
    domain=NaturalPos).with_wrapping()

phase_kickbacks_on_register (conjecture without proof):

%end theorems

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

# sub_circuit_inputs = Forall(
#     (k, m, n),
#     Forall(
#         (a_1_to_k, b_1_to_k, c_1_to_k, U11_to_Ukm, V11_to_Vkm, R11_to_Rkm, S11_to_Skm),
#         Implies(And(circuit_aUVc, circuit_aUb),
#                circuit_bVc).with_wrap_after_operator()),
#     domain=NaturalPos)

# sub_circuit_inputs.instance_expr.instance_expr

# qubit_permutation = Forall(
#     (P, Q), Forall(
#         (k, m, n),
#         Forall(
#             (A11_to_Akm, R11_to_Rkm, B11_to_Bkn, S11_to_Skn),
#             Implies(CircuitEquiv(circuit_A_detailed, circuit_B_detailed),
#                     CircuitEquiv(permuted_circuit_A, permuted_circuit_B)).with_wrap_after_operator()),
#         domain=NaturalPos))

# qubit_permutation.instance_expr.instance_expr.instance_expr

# qubit_range_circuit_substitution = Forall(
#     (k, l, m, n), Forall(
#         (A11_to_Akl, B11_to_Bkm, C11_to_Ckn, D11_to_Dkm),
#         Implies(CircuitEquiv(circuit_B, circuit_D),
#                 CircuitEquiv(circuit_ABCvert, circuit_ADCvert)).with_wrap_after_operator()),
#     domain=NaturalPos)

# qubit_range_circuit_substitution.instance_expr.instance_expr

# %end theorems