Quantum code from two binary linear codes

“Good Quantum error-correcting codes exist.” – Shor

Two Binary linear codes: One code corrects bit flips in the Z basis. The other the X basis.

• “Instance of Stabilizer codes

  • “Simple stabilizers.” generated by the Clifford group;

  • “CSS codes are precisely those for which a CNOT applied between every pair of corresponding qubits in two blocks performs a valid fault-tolerant operation.”

• “Codes that encode k qubits into n qubits and correct t errors; have asymptotic rate 1 − 2 * binary_entropy(2t/n) as n → ∞.”

• If t or fewer qubits are measured, no information about the quantum state of the encoded bits is revealed and the state can be perfectly recovered from the remaining n − t qubits.”

• by applying a unitary transformation R (independent of D) to ℋ₂ⁿ ⊗ ℋ_anc.”

import Binary_linear_code

variables
[n k d : ℕ]

variables
[binary_linear_code C₁]
[C₁.n = n]
[dim C₁ = n-k]
[code_dist C₁ = d]

variables
[complex_hilbert_space ℋC₁] [subspace ℋC₁ ℋ₂ⁿ]
[generator_matrix M C₁] -- C₁.words is the row space of M:
[C₁.words = {v M | v : F₂^dim(C₁)}]

/-- Construct quantum states |cw⟩ from C₁.words: -/
def encode_quantum (w : F₂ⁿ) := 
λ w, 2^{−dim(C₁)/2} * ∑ c ∈ C₁.words, (−1)^{c w} |c⟩

/-
For a code with message length 4 like Hamming (7,4,3).
λ w, 1/4 * ∑ c ∈ C₁.words, (−1)^{c w} |c⟩
-/

/--
The vectors {encode_quantum w | w : F₂ⁿ / C₁⊥}
form a basis for ℋC₁.

[{encode_quantum c | c ∈ C₁.words} generates ℋC₁]

Here F₂ⁿ / C₁⊥ := { {c + w | w : F₂ⁿ} | c ∈ C₁⊥.words}
There are 2^dim(C₁) of these cosets.
They form the natural index set for states |cw⟩.
-/
lemma encoded_quantum_words_form_basis :
  is_basis {encode_quantum w | w : F₂ⁿ / C₁⊥} ℋC₁ :=
begin
  /- If w₁ + w₂ ∈ C₁⊥.words then〈cw₁|cw₂⟩ = 1 -/
  have quantum_encoded_states_equal_of_sum_codewords_in_dual : 
    w₁ + w₂ ∈ C₁⊥.words → encode_quantum w₁ = encode_quantum w₂, 
  {
    /- ∀ c ∈ C₁.words, c w₁ = c w₂ -/
  }

  /- If w₁ + w₂ ∉ C₁⊥ then〈cw₁|cw₂⟩ = 0 -/
  have quantum_encoded_states_orthogonal_of_sum_codewords_not_in_dual :
    w₁ + w₂ ∉ C₁⊥ → (encode_quantum w₁)† * (encode_quantum w₂) = 0,
  {
    -- This follows since ∑ c ∈ C₁.words, (−1)^{c w} = 0.
    -- unless ∀ c ∈ C₁.words, c w = 0.
  }
  sorry,
end

The condition C₀⊥ ⊂ C₁ is equivalent to H₀H₁ᵀ = 0.

The condition H₀H₁ᵀ = 0 means that each row in H₀ is orthogonal to each row in H₁.

Or in other words: an even number of checks overlap in H₀ and H₁.

XX and ZZ

import Quantum_error_correction

variables
(C₂⊥ : binary_linear_code)
[C₂⊥.n = C₁.n]
[dim C₂⊥ = dim C₁]
[code_dist C₂⊥ = code_dist C₁]
[{0} ⊂ C₂.words ⊂ C₁.words]

variables
[quantum_code ℰC₁C₂]

/-
"Let the quantum code ℰC₁C₂ be such that
its codewords are {encode_quantum w | w ∈ C₂⊥.words}."
-/

/-
"The natural index set for the codewords is thus over C₂⊥ / C₁⊥,
the cosets of C₁⊥ in C₂⊥.

This code thus contains 2^{dim(C₁)−dim(C₂)} orthogonal vectors.

Since its length is n qubits, it has rate (dim(C₁) − dim(C₂))/n"
-/
lemma quantum_code_rate_CSS_code :
quantum_code_rate ℰC₁C₂ = (dim(C₁) − dim(C₂)) / C₁.n := sorry

def t : ℕ := ⌊(d−1)/2⌋

theorem Theorem1 :
  corrects_t_errors ℰC₁C₂ :=
begin
  /-
  "Let E be the binary vector such that supp(E)
  is the set of qubits that have decohered."

  So hamming_weight(E) = t
  -/

  /-
  "the most general decoherence D is a unitary process
  operating on a binary vector u
  and the initial state of the environment |a0〉as follows:
  
  D |u⟩|a0〉= ∑ e ≤ E, |u + e⟩|a_u|E,e⟩"
  -/

  /-
  If the decoherence acts on |cw⟩|a0⟩ we get

  D |cw⟩|a0⟩ = 2^{-(n-k)/2} * ∑ v, (-1)^{v M w} * ∑ e ≤ E, |v M + e⟩|a_{v M|E,e}⟩
  -/

  Have H1 : code_dist C₁ > 2*hamming_weight(e), {
    -- code_dist C₁ = d
    sorry
  }.

  /-
  Intuitively: If code_dist is large and hamming_weight(e)
  then we might be able to correct the error e.

  So we can restore v M + e to a unique codeword v M ∈ C₁.words.
  
  We can do this using a unitary operator Rf
  provided we make the operation reversible;
  
  to do this we record the error e
  in a set of ancilla qubits A.

  Rf D |cw⟩ = 2^{-(n-k)/2} * ∑ v, (-1)^{v M w} * ∑ e ≤ E, |v M⟩ |a_{vM|E,e}⟩ |Aₑ⟩ 
  
  Since v M ∈ C₁.words,
  we have now corrected our state to some state in the Hilbert space ℋC₁.
  "
  -/

  /-
  "encode_quantum w can only decohere to encode_quantum u if
   there is c ∈ C₁⊥.words such that hamming_weight(u + w + c) ≤ t."
  -/

  /-
  "So for each encode_quantum u there is a unique encode_quantum w 
  with w ∈ C₂⊥.words / C₁⊥.words
  which it could have arisen from"
  -/
  have H2 : ..., {
    by_contradiction,
    /-
    "Suppose that we have two such w’s, w₁ and w₂ 
    with w₁ + u + c₁ = e₁ and w₂ + u + c₂ = e₂."
    -/

    /- Then e₁ + e₂ = w₁ + w₂ + c₁ + c₂ ∈ C₂⊥. -/

    /-
    However hamming_weight(e₁ + e₂) ≤ hamming_weight e₁ + hamming_weight e₂
                                    ≤ 2*t
    -/

    /-
    But code_dist C₂⊥ > 2*t.
    So w₁ + w₂ ∈ C₁⊥.
    And encode_quantum u = encode_quantum w
    -/
  }

  /-
  "So there is a unitary from encode_quantum u
  to Rf D encode_quantum w where u : F₂ⁿ / C₁⊥,
  since there is at most one w with hamming_dist(w, u) < t.
  
  So the correction is unitary: Use a second ancilla A′ to record
  which bits we needed to flip to get from u to w
  to ensure the transformation
  
  These flipped bits correspond to phase errors in the original basis."
  -/

  /-
  "Denoting this correction operator by Rp, we get
  
  Rp Rf D encode_quantum w = ...
  
  This is just the state encode_quantum w tensored
  with a state of the ancillae and the environment
  that does not depend on w." We trace them out.
  -/
  sorry,
end

• If avg behaviour of channel corrupts less than t qubits the quantum transmissions is still ok.

• Holevo information upper bounds classical capacity of any quantum channel;

• Decoherence Quantum channel;

  • “by first applying an arbitrary unitary transformation D to the space consisting of the tensor product Ht ⊗ Henv of any t of the qubits and some arbitrary Hilbert space Henv designating the environment, and then tracing over the environment Henv to obtain the output of the channel, which will thus in general be an ensemble of states in H₂ᵏ.”

---

• CSS codes do not have optimal Code efficiency.”

  • Quantum code from two Hamming 7-4-3 codes

  • The five-qubit code;

  • Shor’s nine-qubit code;

  • Repetition code;

  • Quantum code from two binary linear codes on expander graphs;

---

distance of a quantum code


dX = min { |w| | w ∈ 𝒞₀\𝒞₁⊥ }


dZ = min { |w| | w ∈ 𝒞₁\𝒞₀⊥ }

                                             
                    X   ⇅   X   ⇅   X   ⇅             
                                                      
                    ⇅   Z   ⇅   Z   ⇅   Z             
                                                      
                    X   ⇅   X   ⇅   X   ⇅             
          ඌ                                          
⇅        /|\        ⇅   Z   ⇅   Z   ⇅   Z             
                                                      
                    X   ⇅   X   ⇅   X   ⇅             
                                                      
                    ⇅   Z   ⇅   Z   ⇅   Z             
                                             

                                             
                    X   ⇅   X   ⇅   X   ⇅             
                                                      
                    ⇅   Z   ⇅.  Z   ⇅   Z             
                                                      
                    X   ⇅   X   ⇅   X   ⇅             
          ඌ                                          
⇅        /|\        ⇅   Z   ⇅.  Z   ⇅   Z             
                                                      
                    X   ⇅   X   ⇅   X   ⇅             
                                                      
                    ⇅   Z   ⇅.  Z   ⇅   Z             
                                             

an error that commutes with the stabilizers
                                             
                    X   ⇅   X   ⇅   X   ⇅             
                                                      
                    ⇅   Z   ⇅   Z   ⇅   Z             
                                                      
                    X   ⇅   X   ⇅.  X   ⇅             
          ඌ                                          
⇅        /|\        ⇅   Z   ⇅.  Z   ⇅.  Z             
                                                      
                    X   ⇅   X   ⇅.  X   ⇅             
                                                      
                    ⇅   Z   ⇅   Z   ⇅   Z             
                                             

returns a word that corresponds to the same logical state

---

CSS codes as ZX diagrams;

References

• Shor1996;

• Gottesman1997;

• Leverrier2022;