Documentation

LeanPool.SingleCopyStabilizer.Circuit

Recorded binary Clifford circuits and exact decoding #

Each recorded outcome specifies precisely the CNOTs and correction used by one learning round. Lists are chronological: the head is performed first. The inverse acts on the final computational basis vector to reconstruct the original amplitude, with its physically irrelevant global phase explicit.

source
def LeanPool.SingleCopyStabilizer.Circuit.cnotEquiv {ι : Type u_1} (i : ι) (w : Measurement.Bits ι) (hw : w i = 0) :
Measurement.Amplitude ι ≃ₗ[ℂ] Measurement.Amplitude ι

The simultaneous CNOT operation, with its explicit inverse permutation.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem LeanPool.SingleCopyStabilizer.Circuit.cnotEquiv_apply {ι : Type u_1} (i : ι) (w : Measurement.Bits ι) (hw : w i = 0) (ψ : Measurement.Amplitude ι) :
    (cnotEquiv i w hw) ψ = CNOTAction.applyCNOTs i w hw ψ
    source
    @[simp]
    theorem LeanPool.SingleCopyStabilizer.Circuit.cnotEquiv_symm_apply {ι : Type u_1} (i : ι) (w : Measurement.Bits ι) (hw : w i = 0) (ψ : Measurement.Amplitude ι) :
    (cnotEquiv i w hw).symm ψ = fun (x : Measurement.Bits ι) => ψ ((CNOTAction.basisShear i w hw) x)
    source
    noncomputable def LeanPool.SingleCopyStabilizer.Circuit.correctionEquiv {ι : Type u_1} [DecidableEq ι] (i : ι) (b : ZMod 2) :
    Measurement.Amplitude ι ≃ₗ[ℂ] Measurement.Amplitude ι

    The correction is H for bit zero and HS for bit one.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem LeanPool.SingleCopyStabilizer.Circuit.correctionEquiv_apply {ι : Type u_1} [DecidableEq ι] (i : ι) (b : ZMod 2) (ψ : Measurement.Amplitude ι) :
      (correctionEquiv i b) ψ = CliffordAction.localHadamard i (if b = 0 then ψ else CliffordAction.localPhase i ψ)
      source
      theorem LeanPool.SingleCopyStabilizer.Circuit.correctionEquiv_normalized {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) (b : ZMod 2) (ψ : Measurement.Amplitude ι) (hψ : Measurement.IsNormalized ψ) :
      Measurement.IsNormalized ((correctionEquiv i b) ψ)
      source
      theorem LeanPool.SingleCopyStabilizer.Circuit.correctionEquiv_norm_preserving {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) (b : ZMod 2) (ψ : Measurement.Amplitude ι) :
      ∑ x : Measurement.Bits ι, Measurement.bornWeight ((correctionEquiv i b) ψ) x = ∑ x : Measurement.Bits ι, Measurement.bornWeight ψ x
      source
      theorem LeanPool.SingleCopyStabilizer.Circuit.pivot_target_zero {ι : Type u_1} [DecidableEq ι] (u : Measurement.Bits ι) (hu : u ≠ 0) :
      (u - Pi.single (binaryPivot u hu) 1) (binaryPivot u hu) = 0

      The pivot-coordinate vanishes in the CNOT target vector.

      source
      noncomputable def LeanPool.SingleCopyStabilizer.Circuit.roundEquiv {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u : Measurement.Bits ι) (b : ZMod 2) :
      Measurement.Amplitude ι ≃ₗ[ℂ] Measurement.Amplitude ι

      The physical Clifford operation determined by the sampled difference and the correction coin. A zero difference records the identity operation.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem LeanPool.SingleCopyStabilizer.Circuit.roundEquiv_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (b : ZMod 2) :
        roundEquiv 0 b = LinearEquiv.refl ℂ (Measurement.Amplitude ι)
        source
        theorem LeanPool.SingleCopyStabilizer.Circuit.roundEquiv_apply_of_ne {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u : Measurement.Bits ι) (b : ZMod 2) (hu : u ≠ 0) (ψ : Measurement.Amplitude ι) :
        (roundEquiv u b) ψ = (correctionEquiv (binaryPivot u hu) b) (CNOTAction.applyCNOTs (binaryPivot u hu) (u - Pi.single (binaryPivot u hu) 1) ⋯ ψ)
        source
        theorem LeanPool.SingleCopyStabilizer.Circuit.roundEquiv_normalized {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u : Measurement.Bits ι) (b : ZMod 2) (ψ : Measurement.Amplitude ι) (hψ : Measurement.IsNormalized ψ) :
        Measurement.IsNormalized ((roundEquiv u b) ψ)
        source
        theorem LeanPool.SingleCopyStabilizer.Circuit.roundEquiv_norm_preserving {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u : Measurement.Bits ι) (b : ZMod 2) (ψ : Measurement.Amplitude ι) :
        ∑ x : Measurement.Bits ι, Measurement.bornWeight ((roundEquiv u b) ψ) x = ∑ x : Measurement.Bits ι, Measurement.bornWeight ψ x
        source
        @[reducible, inline]
        abbrev LeanPool.SingleCopyStabilizer.Circuit.Outcome (ι : Type u_2) :
        Type u_2

        A recorded outcome is sufficient to specify all gates in a round.

        Equations
        Instances For
          source
          def LeanPool.SingleCopyStabilizer.Circuit.circuitEquiv {ι : Type u_1} [Fintype ι] [DecidableEq ι] :
          List (Outcome ι) → Measurement.Amplitude ι ≃ₗ[ℂ] Measurement.Amplitude ι

          Circuit composition in chronological order.

          Equations
          Instances For
            source
            @[simp]
            theorem LeanPool.SingleCopyStabilizer.Circuit.circuitEquiv_nil {ι : Type u_1} [Fintype ι] [DecidableEq ι] :
            circuitEquiv [] = LinearEquiv.refl ℂ (Measurement.Amplitude ι)
            source
            @[simp]
            theorem LeanPool.SingleCopyStabilizer.Circuit.circuitEquiv_cons {ι : Type u_1} [Fintype ι] [DecidableEq ι] (op : Outcome ι) (ops : List (Outcome ι)) :
            circuitEquiv (op :: ops) = roundEquiv op.1 op.2 ≪≫ₗ circuitEquiv ops
            source
            @[simp]
            theorem LeanPool.SingleCopyStabilizer.Circuit.circuitEquiv_cons_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] (op : Outcome ι) (ops : List (Outcome ι)) (ψ : Measurement.Amplitude ι) :
            (circuitEquiv (op :: ops)) ψ = (circuitEquiv ops) ((roundEquiv op.1 op.2) ψ)
            source
            theorem LeanPool.SingleCopyStabilizer.Circuit.circuitEquiv_append {ι : Type u_1} [Fintype ι] [DecidableEq ι] (xs ys : List (Outcome ι)) :
            circuitEquiv (xs ++ ys) = circuitEquiv xs ≪≫ₗ circuitEquiv ys
            source
            theorem LeanPool.SingleCopyStabilizer.Circuit.circuitEquiv_normalized {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ops : List (Outcome ι)) (ψ : Measurement.Amplitude ι) (hψ : Measurement.IsNormalized ψ) :
            Measurement.IsNormalized ((circuitEquiv ops) ψ)
            source
            theorem LeanPool.SingleCopyStabilizer.Circuit.circuitEquiv_norm_preserving {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ops : List (Outcome ι)) (ψ : Measurement.Amplitude ι) :
            ∑ x : Measurement.Bits ι, Measurement.bornWeight ((circuitEquiv ops) ψ) x = ∑ x : Measurement.Bits ι, Measurement.bornWeight ψ x
            source
            theorem LeanPool.SingleCopyStabilizer.Circuit.circuitEquiv_symm_normalized {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ops : List (Outcome ι)) (ψ : Measurement.Amplitude ι) (hψ : Measurement.IsNormalized ψ) :
            Measurement.IsNormalized ((circuitEquiv ops).symm ψ)
            source
            def LeanPool.SingleCopyStabilizer.Circuit.basis {ι : Type u_1} [Fintype ι] (z : Measurement.Bits ι) :
            Measurement.Amplitude ι

            Computational basis amplitudes, with value one at the chosen string.

            Equations
            Instances For
              source
              @[simp]
              theorem LeanPool.SingleCopyStabilizer.Circuit.basis_apply {ι : Type u_1} [Fintype ι] (z x : Measurement.Bits ι) :
              basis z x = if x = z then 1 else 0
              source
              theorem LeanPool.SingleCopyStabilizer.Circuit.basis_normalized {ι : Type u_1} [Fintype ι] [DecidableEq ι] (z : Measurement.Bits ι) :
              Measurement.IsNormalized (basis z)
              source
              noncomputable def LeanPool.SingleCopyStabilizer.Circuit.decode {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ops : List (Outcome ι)) (z : Measurement.Bits ι) :
              Measurement.Amplitude ι

              Classical description of the learned state: undo the recorded circuit on the final measured basis string.

              Equations
              Instances For
                source
                @[simp]
                theorem LeanPool.SingleCopyStabilizer.Circuit.decode_nil {ι : Type u_1} [Fintype ι] [DecidableEq ι] (z : Measurement.Bits ι) :
                decode [] z = basis z
                source
                @[simp]
                theorem LeanPool.SingleCopyStabilizer.Circuit.decode_cons {ι : Type u_1} [Fintype ι] [DecidableEq ι] (op : Outcome ι) (ops : List (Outcome ι)) (z : Measurement.Bits ι) :
                decode (op :: ops) z = (roundEquiv op.1 op.2).symm (decode ops z)
                source
                theorem LeanPool.SingleCopyStabilizer.Circuit.decode_append {ι : Type u_1} [Fintype ι] [DecidableEq ι] (xs ys : List (Outcome ι)) (z : Measurement.Bits ι) :
                decode (xs ++ ys) z = (circuitEquiv xs).symm (decode ys z)
                source
                @[simp]
                theorem LeanPool.SingleCopyStabilizer.Circuit.circuitEquiv_decode {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ops : List (Outcome ι)) (z : Measurement.Bits ι) :
                (circuitEquiv ops) (decode ops z) = basis z
                source
                theorem LeanPool.SingleCopyStabilizer.Circuit.decode_normalized {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ops : List (Outcome ι)) (z : Measurement.Bits ι) :
                Measurement.IsNormalized (decode ops z)
                source
                theorem LeanPool.SingleCopyStabilizer.Circuit.reconstruction_eq_smul_decode {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ops : List (Outcome ι)) (ψ : Measurement.Amplitude ι) (z : Measurement.Bits ι) (c : ℂ) (h : (circuitEquiv ops) ψ = c • basis z) :
                ψ = c • decode ops z

                Inverting the recorded circuit recovers the original amplitude with the same global phase as its final computational basis amplitude.

                source
                theorem LeanPool.SingleCopyStabilizer.Circuit.smul_basis {ι : Type u_1} [Fintype ι] (z : Measurement.Bits ι) (c : ℂ) :
                c • basis z = fun (x : Measurement.Bits ι) => if x = z then c else 0
                source
                theorem LeanPool.SingleCopyStabilizer.Circuit.reconstruction_of_basis_amplitude {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ops : List (Outcome ι)) (ψ : Measurement.Amplitude ι) (z : Measurement.Bits ι) (c : ℂ) (h : (circuitEquiv ops) ψ = fun (x : Measurement.Bits ι) => if x = z then c else 0) :
                ψ = c • decode ops z

                Version matching StabilizerState.full_diagonal_basis_amplitude.

                source
                theorem LeanPool.SingleCopyStabilizer.Circuit.reconstruction_phase_normSq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ops : List (Outcome ι)) (ψ : Measurement.Amplitude ι) (hψ : Measurement.IsNormalized ψ) (z : Measurement.Bits ι) (c : ℂ) (h : (circuitEquiv ops) ψ = c • basis z) :
                Complex.normSq c = 1

                If the input is normalized, the scalar occurring at a basis-vector endpoint must have unit modulus.

                source
                theorem LeanPool.SingleCopyStabilizer.Circuit.reconstruction_iff {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ops : List (Outcome ι)) (ψ : Measurement.Amplitude ι) (z : Measurement.Bits ι) (c : ℂ) :
                (circuitEquiv ops) ψ = c • basis z ↔ ψ = c • decode ops z

                The circuit endpoint condition and exact recovery up to a specified global phase are equivalent.