Documentation

CsdLean4.Mathlib.QuantumInfo.Stabilizer

Stabiliser families, the group projector, and the stabilised state (GK-3) #

Category: 1-Mathlib (CSD-free).

The stabiliser layer over the Pauli algebra (plan specs/gottesman-knill-plan.md, GK-3), in the corpus's hypothesis-driven concrete style: a stabiliser family is indexed by ๐”ฝโ‚‚^m directly โ€” ๐”ฝโ‚‚-linear label maps A B : ๐”ฝโ‚‚^m โ†’ ๐”ฝโ‚‚โฟ and a sign function ฯƒ : ๐”ฝโ‚‚^m โ†’ ๐”ฝโ‚‚ subject to the one coherence law

ฯƒ(x+y) = ฯƒ(x) + ฯƒ(y) + B(x)ยทA(y),

which is exactly the condition that the signed Paulis ฯ‡(ฯƒx)ยทX^{Ax}Z^{Bx} form a genuine group (the ๐”ฝโ‚‚ pairing on the right is the phase of pauliOp_mul) โ€” the "โˆ’I โˆ‰ S" condition of the stabiliser formalism. Commutativity of the family is implied: coherence at (x,y) and at (y,x) forces the symplectic form of any two members to vanish (stab_symp_zero).

Both residues named at the first landing are now discharged in this file:

Honest scope. Measurement is Born-weight bookkeeping on the corpus's coordinate operators; no measurement dynamics is claimed (that is the CSD layer's business elsewhere). The IsProj.trace route uses Mathlib's linear algebra, not a spectral theorem.

source
noncomputable def QuantumInfo.stabProjector {n m : โ„•} (A B : (Fin m โ†’ Fin 2) โ†’ Fin n โ†’ Fin 2) (ฯƒ : (Fin m โ†’ Fin 2) โ†’ Fin 2) (ฯˆ : QReg n) :
QReg n

The stabiliser-group average P = 2^{โˆ’m} โˆ‘_{x โˆˆ ๐”ฝโ‚‚^m} ฯ‡(ฯƒx) ยท X^{Ax} Z^{Bx}, applied to a state.

Equations
Instances For
    source
    theorem QuantumInfo.stab_label_zero {n m : โ„•} {A : (Fin m โ†’ Fin 2) โ†’ Fin n โ†’ Fin 2} (hA : โˆ€ (x y : Fin m โ†’ Fin 2), A (x + y) = A x + A y) :
    A 0 = 0

    Linearity forces the zero label at 0.

    source
    theorem QuantumInfo.stab_sigma_zero {n m : โ„•} {A B : (Fin m โ†’ Fin 2) โ†’ Fin n โ†’ Fin 2} {ฯƒ : (Fin m โ†’ Fin 2) โ†’ Fin 2} (hB : โˆ€ (x y : Fin m โ†’ Fin 2), B (x + y) = B x + B y) (hฯƒ : โˆ€ (x y : Fin m โ†’ Fin 2), ฯƒ (x + y) = ฯƒ x + ฯƒ y + bdot (B x) (A y)) :
    ฯƒ 0 = 0

    Coherence forces the trivial sign at 0 โ€” the group contains +I, not โˆ’I.

    source
    theorem QuantumInfo.stab_symp_zero {n m : โ„•} {A B : (Fin m โ†’ Fin 2) โ†’ Fin n โ†’ Fin 2} {ฯƒ : (Fin m โ†’ Fin 2) โ†’ Fin 2} (hฯƒ : โˆ€ (x y : Fin m โ†’ Fin 2), ฯƒ (x + y) = ฯƒ x + ฯƒ y + bdot (B x) (A y)) (x y : Fin m โ†’ Fin 2) :
    bdot (A x) (B y) + bdot (B x) (A y) = 0

    Coherence at (x,y) and (y,x) forces the symplectic form of any two members to vanish: the family is automatically abelian.

    source
    theorem QuantumInfo.stabProjector_absorb {n m : โ„•} {A B : (Fin m โ†’ Fin 2) โ†’ Fin n โ†’ Fin 2} {ฯƒ : (Fin m โ†’ Fin 2) โ†’ Fin 2} (hA : โˆ€ (x y : Fin m โ†’ Fin 2), A (x + y) = A x + A y) (hB : โˆ€ (x y : Fin m โ†’ Fin 2), B (x + y) = B x + B y) (hฯƒ : โˆ€ (x y : Fin m โ†’ Fin 2), ฯƒ (x + y) = ฯƒ x + ฯƒ y + bdot (B x) (A y)) (x : Fin m โ†’ Fin 2) (ฯˆ : QReg n) :
    signChar (ฯƒ x) โ€ข pauliOp (A x) (B x) (stabProjector A B ฯƒ ฯˆ) = stabProjector A B ฯƒ ฯˆ

    โ˜… Absorption: every signed element of the family fixes the group average.

    source
    theorem QuantumInfo.stabProjector_idem {n m : โ„•} {A B : (Fin m โ†’ Fin 2) โ†’ Fin n โ†’ Fin 2} {ฯƒ : (Fin m โ†’ Fin 2) โ†’ Fin 2} (hA : โˆ€ (x y : Fin m โ†’ Fin 2), A (x + y) = A x + A y) (hB : โˆ€ (x y : Fin m โ†’ Fin 2), B (x + y) = B x + B y) (hฯƒ : โˆ€ (x y : Fin m โ†’ Fin 2), ฯƒ (x + y) = ฯƒ x + ฯƒ y + bdot (B x) (A y)) (ฯˆ : QReg n) :
    stabProjector A B ฯƒ (stabProjector A B ฯƒ ฯˆ) = stabProjector A B ฯƒ ฯˆ

    โ˜… Idempotence, three lines from absorption.

    source
    theorem QuantumInfo.stabProjector_trace {n m : โ„•} {A B : (Fin m โ†’ Fin 2) โ†’ Fin n โ†’ Fin 2} {ฯƒ : (Fin m โ†’ Fin 2) โ†’ Fin 2} (hA : โˆ€ (x y : Fin m โ†’ Fin 2), A (x + y) = A x + A y) (hB : โˆ€ (x y : Fin m โ†’ Fin 2), B (x + y) = B x + B y) (hฯƒ : โˆ€ (x y : Fin m โ†’ Fin 2), ฯƒ (x + y) = ฯƒ x + ฯƒ y + bdot (B x) (A y)) (hinj : โˆ€ (x : Fin m โ†’ Fin 2), A x = 0 โ†’ B x = 0 โ†’ x = 0) :
    โˆ‘ z : Fin n โ†’ Fin 2, (stabProjector A B ฯƒ (basisState z)).ofLp z = 2 ^ n / 2 ^ m

    โ˜… The trace of the group average is the code-space dimension count 2โฟ/2^m (= 1 for a full stabiliser, m = n): only the identity label survives the Pauli trace, and independence pins it to x = 0, where coherence forces the + sign.

    source
    theorem QuantumInfo.stabState_exists {n m : โ„•} {A B : (Fin m โ†’ Fin 2) โ†’ Fin n โ†’ Fin 2} {ฯƒ : (Fin m โ†’ Fin 2) โ†’ Fin 2} (hA : โˆ€ (x y : Fin m โ†’ Fin 2), A (x + y) = A x + A y) (hB : โˆ€ (x y : Fin m โ†’ Fin 2), B (x + y) = B x + B y) (hฯƒ : โˆ€ (x y : Fin m โ†’ Fin 2), ฯƒ (x + y) = ฯƒ x + ฯƒ y + bdot (B x) (A y)) (hinj : โˆ€ (x : Fin m โ†’ Fin 2), A x = 0 โ†’ B x = 0 โ†’ x = 0) :
    โˆƒ (ฯˆ : QReg n), ฯˆ โ‰  0 โˆง stabProjector A B ฯƒ ฯˆ = ฯˆ โˆง โˆ€ (x : Fin m โ†’ Fin 2), signChar (ฯƒ x) โ€ข pauliOp (A x) (B x) ฯˆ = ฯˆ

    โ˜…โ˜… The stabilised state exists: a nonzero ฯˆ fixed by the group average and by every signed element of the family โ€” the defining property of a stabiliser state. Extracted from tr P โ‰  0 and idempotence; no spectral machinery. (That the fixed space has dimension exactly 2^{nโˆ’m} is the named uniqueness residue in the plan.)

    The group average as a linear projection, and rank = trace #

    source
    theorem QuantumInfo.stabProjector_map_add {n m : โ„•} (A B : (Fin m โ†’ Fin 2) โ†’ Fin n โ†’ Fin 2) (ฯƒ : (Fin m โ†’ Fin 2) โ†’ Fin 2) (ฯˆ ฯ‡ : QReg n) :
    stabProjector A B ฯƒ (ฯˆ + ฯ‡) = stabProjector A B ฯƒ ฯˆ + stabProjector A B ฯƒ ฯ‡
    source
    theorem QuantumInfo.stabProjector_map_smul {n m : โ„•} (A B : (Fin m โ†’ Fin 2) โ†’ Fin n โ†’ Fin 2) (ฯƒ : (Fin m โ†’ Fin 2) โ†’ Fin 2) (c : โ„‚) (ฯˆ : QReg n) :
    stabProjector A B ฯƒ (c โ€ข ฯˆ) = c โ€ข stabProjector A B ฯƒ ฯˆ
    source
    noncomputable def QuantumInfo.stabProjectorL {n m : โ„•} (A B : (Fin m โ†’ Fin 2) โ†’ Fin n โ†’ Fin 2) (ฯƒ : (Fin m โ†’ Fin 2) โ†’ Fin 2) :
    QReg n โ†’โ‚—[โ„‚] QReg n

    The group average as a linear map.

    Equations
    Instances For
      source
      @[simp]
      theorem QuantumInfo.stabProjectorL_apply {n m : โ„•} (A B : (Fin m โ†’ Fin 2) โ†’ Fin n โ†’ Fin 2) (ฯƒ : (Fin m โ†’ Fin 2) โ†’ Fin 2) (ฯˆ : QReg n) :
      (stabProjectorL A B ฯƒ) ฯˆ = stabProjector A B ฯƒ ฯˆ
      source
      theorem QuantumInfo.stabProjectorL_trace {n m : โ„•} (A B : (Fin m โ†’ Fin 2) โ†’ Fin n โ†’ Fin 2) (ฯƒ : (Fin m โ†’ Fin 2) โ†’ Fin 2) :
      (LinearMap.trace โ„‚ (QReg n)) (stabProjectorL A B ฯƒ) = โˆ‘ z : Fin n โ†’ Fin 2, (stabProjector A B ฯƒ (basisState z)).ofLp z

      The linear-map trace is the coordinate diagonal sum this file computes.

      source
      theorem QuantumInfo.stabProjectorL_isProj {n m : โ„•} {A B : (Fin m โ†’ Fin 2) โ†’ Fin n โ†’ Fin 2} {ฯƒ : (Fin m โ†’ Fin 2) โ†’ Fin 2} (hA : โˆ€ (x y : Fin m โ†’ Fin 2), A (x + y) = A x + A y) (hB : โˆ€ (x y : Fin m โ†’ Fin 2), B (x + y) = B x + B y) (hฯƒ : โˆ€ (x y : Fin m โ†’ Fin 2), ฯƒ (x + y) = ฯƒ x + ฯƒ y + bdot (B x) (A y)) :
      LinearMap.IsProj (stabProjectorL A B ฯƒ).range (stabProjectorL A B ฯƒ)

      The group average is a genuine linear projection onto its range.

      source
      theorem QuantumInfo.mem_range_stabProjectorL_iff {n m : โ„•} {A B : (Fin m โ†’ Fin 2) โ†’ Fin n โ†’ Fin 2} {ฯƒ : (Fin m โ†’ Fin 2) โ†’ Fin 2} (hA : โˆ€ (x y : Fin m โ†’ Fin 2), A (x + y) = A x + A y) (hB : โˆ€ (x y : Fin m โ†’ Fin 2), B (x + y) = B x + B y) (hฯƒ : โˆ€ (x y : Fin m โ†’ Fin 2), ฯƒ (x + y) = ฯƒ x + ฯƒ y + bdot (B x) (A y)) (ฯ† : QReg n) :
      ฯ† โˆˆ (stabProjectorL A B ฯƒ).range โ†” stabProjector A B ฯƒ ฯ† = ฯ†

      The range of the group average is exactly the fixed space.

      source
      theorem QuantumInfo.stabProjector_rank {n m : โ„•} {A B : (Fin m โ†’ Fin 2) โ†’ Fin n โ†’ Fin 2} {ฯƒ : (Fin m โ†’ Fin 2) โ†’ Fin 2} (hA : โˆ€ (x y : Fin m โ†’ Fin 2), A (x + y) = A x + A y) (hB : โˆ€ (x y : Fin m โ†’ Fin 2), B (x + y) = B x + B y) (hฯƒ : โˆ€ (x y : Fin m โ†’ Fin 2), ฯƒ (x + y) = ฯƒ x + ฯƒ y + bdot (B x) (A y)) (hinj : โˆ€ (x : Fin m โ†’ Fin 2), A x = 0 โ†’ B x = 0 โ†’ x = 0) (hmn : m โ‰ค n) :
      Module.finrank โ„‚ โ†ฅ(stabProjectorL A B ฯƒ).range = 2 ^ (n - m)

      โ˜…โ˜… Rank equals trace โ€” the uniqueness residue discharged: the fixed space of a stabiliser family with m independent generators on n qubits has dimension exactly 2^{nโˆ’m}. Via Mathlib's LinearMap.IsProj.trace; no spectral theorem.

      source
      theorem QuantumInfo.stabState_unique {n : โ„•} {A' B' : (Fin n โ†’ Fin 2) โ†’ Fin n โ†’ Fin 2} {ฯƒ' : (Fin n โ†’ Fin 2) โ†’ Fin 2} (hA' : โˆ€ (x y : Fin n โ†’ Fin 2), A' (x + y) = A' x + A' y) (hB' : โˆ€ (x y : Fin n โ†’ Fin 2), B' (x + y) = B' x + B' y) (hฯƒ' : โˆ€ (x y : Fin n โ†’ Fin 2), ฯƒ' (x + y) = ฯƒ' x + ฯƒ' y + bdot (B' x) (A' y)) (hinj : โˆ€ (x : Fin n โ†’ Fin 2), A' x = 0 โ†’ B' x = 0 โ†’ x = 0) (ฯˆ ฯ† : QReg n) (hฯˆfix : stabProjector A' B' ฯƒ' ฯˆ = ฯˆ) (hฯ†fix : stabProjector A' B' ฯƒ' ฯ† = ฯ†) (hฯˆ0 : ฯˆ โ‰  0) :
      โˆƒ (c : โ„‚), ฯ† = c โ€ข ฯˆ

      โ˜…โ˜… The full-stabiliser state is unique up to scalar (m = n): any two stabilised vectors are parallel.

      Measurement of an involutive Pauli observable #

      source
      noncomputable def QuantumInfo.measProj {n : โ„•} (a b : Fin n โ†’ Fin 2) (s : Fin 2) (ฯˆ : QReg n) :
      QReg n

      The outcome-s measurement branch of the Pauli observable X^a Z^b: ฮ _s ฯˆ = (ฯˆ + ฯ‡(s)ยทgฯˆ)/2, the ฯ‡(s)-eigenspace projection.

      Equations
      Instances For
        source
        theorem QuantumInfo.pauliOp_involutive {n : โ„•} {a b : Fin n โ†’ Fin 2} (hba : bdot b a = 0) (ฯˆ : QReg n) :
        pauliOp a b (pauliOp a b ฯˆ) = ฯˆ

        An X/Z-type Pauli (bยทa = 0) is an involution.

        source
        theorem QuantumInfo.measProj_add_compl {n : โ„•} {a b : Fin n โ†’ Fin 2} (ฯˆ : QReg n) :
        measProj a b 0 ฯˆ + measProj a b 1 ฯˆ = ฯˆ

        The two branches partition the state: ฮ โ‚€ฯˆ + ฮ โ‚ฯˆ = ฯˆ.

        source
        theorem QuantumInfo.pauliOp_measProj {n : โ„•} {a b : Fin n โ†’ Fin 2} (hba : bdot b a = 0) (s : Fin 2) (ฯˆ : QReg n) :
        pauliOp a b (measProj a b s ฯˆ) = signChar s โ€ข measProj a b s ฯˆ

        โ˜… The branch is stabilised by the signed observable: g(ฮ _sฯˆ) = ฯ‡(s)ยทฮ _sฯˆ โ€” half of the measurement-update rule.

        source
        theorem QuantumInfo.meas_deterministic {n : โ„•} {a b : Fin n โ†’ Fin 2} (t : Fin 2) (ฯˆ : QReg n) (hfix : signChar t โ€ข pauliOp a b ฯˆ = ฯˆ) :
        measProj a b t ฯˆ = ฯˆ โˆง measProj a b (t + 1) ฯˆ = 0

        โ˜… The deterministic case: if the signed observable already stabilises ฯˆ, the matching outcome is certain and the other branch is empty.

        source
        theorem QuantumInfo.inner_fixed_pauliOp {n : โ„•} {a' b' : Fin n โ†’ Fin 2} {u : Fin 2} (ฯˆ ฯ† : QReg n) (hs : signChar u โ€ข pauliOp a' b' ฯˆ = ฯˆ) :
        inner โ„‚ ฯˆ (pauliOp a' b' ฯ†) = signChar u * inner โ„‚ ฯˆ ฯ†

        Fixed states absorb their group elements inside an inner product.

        source
        theorem QuantumInfo.meas_expectation_zero {n : โ„•} {a b a' b' : Fin n โ†’ Fin 2} {u : Fin 2} (ฯˆ : QReg n) (hs : signChar u โ€ข pauliOp a' b' ฯˆ = ฯˆ) (hanti : bdot a b' + bdot b a' = 1) :
        inner โ„‚ ฯˆ (pauliOp a b ฯˆ) = 0

        โ˜… The random case, expectation: if some group element stabilising ฯˆ anticommutes with the observable, the expectation โŸจฯˆ, gฯˆโŸฉ vanishes.

        source
        theorem QuantumInfo.meas_prob_half {n : โ„•} {a b a' b' : Fin n โ†’ Fin 2} {u : Fin 2} (ฯˆ : QReg n) (hฯˆ : inner โ„‚ ฯˆ ฯˆ = 1) (hs : signChar u โ€ข pauliOp a' b' ฯˆ = ฯˆ) (hanti : bdot a b' + bdot b a' = 1) (s : Fin 2) :
        inner โ„‚ (measProj a b s ฯˆ) (measProj a b s ฯˆ) = 1 / 2

        โ˜… The random case, Born weights: both outcomes carry probability exactly 1/2.

        source
        theorem QuantumInfo.meas_update_fixes {n : โ„•} {a b a' b' : Fin n โ†’ Fin 2} {u : Fin 2} (ฯˆ : QReg n) (hs : signChar u โ€ข pauliOp a' b' ฯˆ = ฯˆ) (hcomm : bdot a' b + bdot b' a = 0) (s : Fin 2) :
        signChar u โ€ข pauliOp a' b' (measProj a b s ฯˆ) = measProj a b s ฯˆ

        โ˜… The update rule: every group element commuting with the observable still stabilises the post-measurement branch. Together with pauliOp_measProj this is the standard stabiliser update: the new group is generated by ฯ‡(s)ยทg and the commuting part of the old one.