Documentation

CsdLean4.Empirical.QM.QEC.SteaneEncoder

The Steane encoder, and the logical action of a one- or two-qubit operator #

Category: 3-Local (Empirical, QM twin). BACKLOG #86, steps (c) and the crux of (d): what a concatenation of the Steane code needs from level one.

steaneEnc is the encoder, the 128 × 2 matrix whose two columns are |0̄⟩ and |1̄⟩. It is an isometry (steaneEnc_conjTranspose_mul, from the orthonormality of the logical states) whose columns are code states (steaneProj_mul_steaneEnc), so KnillLaflamme.lean's encoder form applies: the landed projector-form condition (steane_knillLaflamme) becomes ★ steaneEnc_pauli_pair, steaneEncᴴ Eᵢᴴ Eⱼ steaneEnc = δᵢⱼ • 1, with no rank statement relating steaneEnc steaneEncᴴ to steaneProj.

The crux for the concatenation is that the logical action of an operator touching at most two qubits is a scalar — distance three, read through the encoder:

Honest scope #

⚠️ Two qubits is the limit, and it is the code's: a product of three single-qubit Paulis is not Eᵢᴴ Eⱼ for the weight-one family, and indeed the logical action of a weight-three operator on the Steane code need not be a scalar (the logical X̄ has weight seven, logicalX_steaneZero). ⚠️ exists_steaneEnc_gateOf_mul_gateOf and exists_steaneEnc_blockKron give the scalar existentially. The value is a product of the one-qubit scalars, but nothing downstream needs it: the induction of #86 only needs that the logical action is a scalar.

Source #

A. Steane, Error correcting codes in quantum theory, PRL 77 (1996); E. Knill, R. Laflamme, Phys. Rev. A 55 (1997) 900; M. Nielsen, I. Chuang, §10.6.1; Mathlib/QuantumInfo/KnillLaflamme.lean (the encoder form), Mathlib/QuantumInfo/BlockKron.lean, Empirical/QM/QEC/SteaneArbitrary.lean (#61, the span step); specs/BACKLOG.md #86; specs/steane-plan.md; specs/future-work.md.

The encoder #

source
noncomputable def CSD.Empirical.QM.QEC.Steane.steaneEnc :
Matrix (Fin 7 → Fin 2) (Fin 2) ℂ

The Steane encoder: the isometry whose two columns are the logical states |0̄⟩ and |1̄⟩.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem CSD.Empirical.QM.QEC.Steane.steaneEnc_col_zero :
    (fun (z : Fin 7 → Fin 2) => steaneEnc z 0) = steaneZero.ofLp
    source
    theorem CSD.Empirical.QM.QEC.Steane.steaneEnc_col_one :
    (fun (z : Fin 7 → Fin 2) => steaneEnc z 1) = steaneOne.ofLp
    source
    theorem CSD.Empirical.QM.QEC.Steane.inner_eq_sum_star (ψ φ : QuantumInfo.QReg 7) :
    inner ℂ ψ φ = ∑ z : Fin 7 → Fin 2, star (ψ.ofLp z) * φ.ofLp z

    The coordinate form of the inner product on the register.

    source
    theorem CSD.Empirical.QM.QEC.Steane.steaneEnc_conjTranspose_mul :
    steaneEnc.conjTranspose * steaneEnc = 1

    ★ The encoder is an isometry: the logical states are orthonormal.

    source
    theorem CSD.Empirical.QM.QEC.Steane.steaneProj_mul_steaneEnc :
    steaneProj * steaneEnc = steaneEnc

    The columns of the encoder are code states.

    The error family through the encoder #

    source
    theorem CSD.Empirical.QM.QEC.Steane.steaneErr_none :
    QuantumInfo.pauliMat (errA none) (errB none) = 1
    source
    theorem CSD.Empirical.QM.QEC.Steane.steaneEnc_pauli_pair (i j : SingleErr) :
    steaneEnc.conjTranspose * (QuantumInfo.pauliMat (errA i) (errB i)).conjTranspose * QuantumInfo.pauliMat (errA j) (errB j) * steaneEnc = 1 i j • 1

    ★ Knill–Laflamme in encoder form for the single-qubit Paulis.

    source
    theorem CSD.Empirical.QM.QEC.Steane.steaneEnc_pauli_single (j : SingleErr) :
    steaneEnc.conjTranspose * QuantumInfo.pauliMat (errA j) (errB j) * steaneEnc = 1 none j • 1

    The logical action of a single error: the identity passes, every weight-one Pauli is detected.

    source
    theorem CSD.Empirical.QM.QEC.Steane.exists_steaneEnc_pauli_mul (i j : SingleErr) :
    ∃ (δ : ℂ), steaneEnc.conjTranspose * (QuantumInfo.pauliMat (errA i) (errB i) * QuantumInfo.pauliMat (errA j) (errB j)) * steaneEnc = δ • 1

    A product of two single-qubit Paulis acts on the encoded qubit as a scalar: it is ±Eᵢᴴ Eⱼ, and the family's Knill–Laflamme matrix is the identity.

    The logical action of an arbitrary operator on one or two qubits #

    source
    theorem CSD.Empirical.QM.QEC.Steane.exists_smul_one_of_forall {κ : Type u_1} [Fintype κ] {L : Type u_2} [DecidableEq L] (f : κ → Matrix L L ℂ) (h : ∀ (i : κ), ∃ (γ : ℂ), f i = γ • 1) :
    ∃ (γ : ℂ), ∑ i : κ, f i = γ • 1

    A finite sum of scalar multiples of the identity is one.

    source
    theorem CSD.Empirical.QM.QEC.Steane.steaneEnc_gateOf (b : Fin 7) (G : Matrix (Fin 2) (Fin 2) ℂ) :
    steaneEnc.conjTranspose * QuantumInfo.Controlled.gateOf b G * steaneEnc = ((G 0 0 + G 1 1) / 2) • 1

    ★★ The logical action of an arbitrary operator on one qubit is a scalar — the trace (G₀₀ + G₁₁)/2. The Paulis span the operators of a qubit (#61) and every weight-one Pauli is detected, so only the identity's coefficient survives.

    source
    theorem CSD.Empirical.QM.QEC.Steane.exists_steaneEnc_gateOf_mul_gateOf (b₀ b₁ : Fin 7) (G₀ G₁ : Matrix (Fin 2) (Fin 2) ℂ) :
    ∃ (δ : ℂ), steaneEnc.conjTranspose * (QuantumInfo.Controlled.gateOf b₀ G₀ * QuantumInfo.Controlled.gateOf b₁ G₁) * steaneEnc = δ • 1

    ★★ Two arbitrary operators on two qubits act as a scalar too — distance three, in the form the concatenation needs.

    source
    theorem CSD.Empirical.QM.QEC.Steane.exists_steaneEnc_blockKron (b₀ b₁ : Fin 7) (N : Fin 7 → Matrix (Fin 2) (Fin 2) ℂ) (h : ∀ (b : Fin 7), b ≠ b₀ → b ≠ b₁ → ∃ (γ : ℂ), N b = γ • 1) :
    ∃ (δ : ℂ), steaneEnc.conjTranspose * QuantumInfo.blockKron N * steaneEnc = δ • 1

    ★★ The logical action of a tensor over blocks with at most two arbitrary slots is a scalar. The two named blocks may coincide, so this covers no arbitrary slot and one as well; it is the shape the induction of #86 consumes, where the good blocks contribute scalars and at most two blocks — one per error of the Knill–Laflamme pair — do not.