LeanPool.SingleCopyStabilizer.Round

A complete unsigned-label update for one binary round, including the zero-difference branch and a deterministic pivot choice.

source

@[reducible, inline]

abbrev LeanPool.SingleCopyStabilizer.BinaryVec (ι : Type u_2) :

Type u_2

Unsigned X or Z labels of a binary qubit register.

Equations

LeanPool.SingleCopyStabilizer.BinaryVec ι = LeanPool.SingleCopyStabilizer.Vec (ZMod 2) ι

Instances For

source

@[reducible, inline]

abbrev LeanPool.SingleCopyStabilizer.BinarySpace (ι : Type u_2) :

Type u_2

Binary linear spaces of paired Pauli labels.

Equations

LeanPool.SingleCopyStabilizer.BinarySpace ι = Submodule (ZMod 2) (LeanPool.SingleCopyStabilizer.Label (ZMod 2) ι)

Instances For

source

theorem LeanPool.SingleCopyStabilizer.bit_eq_one_of_ne_zero (a : ZMod 2) (ha : a ≠ 0) :

a = 1

source

theorem LeanPool.SingleCopyStabilizer.exists_binary_pivot {ι : Type u_1} (u : BinaryVec ι) (hu : u ≠ 0) :

∃ (i : ι), u i = 1

source

noncomputable def LeanPool.SingleCopyStabilizer.binaryPivot {ι : Type u_1} (u : BinaryVec ι) (hu : u ≠ 0) :

Select a coordinate equal to one in a nonzero binary vector.

Equations

LeanPool.SingleCopyStabilizer.binaryPivot u hu = Classical.choose ⋯

Instances For

source

theorem LeanPool.SingleCopyStabilizer.binaryPivot_spec {ι : Type u_1} (u : BinaryVec ι) (hu : u ≠ 0) :

u (binaryPivot u hu) = 1

source

noncomputable def LeanPool.SingleCopyStabilizer.binaryRound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (L : BinarySpace ι) (u : BinaryVec ι) (b : ZMod 2) :

BinarySpace ι

The observed shear and local correction acting on a binary label space.

Equations

LeanPool.SingleCopyStabilizer.binaryRound L u b = if hu : u = 0 then L else LeanPool.SingleCopyStabilizer.updatedSpace L (LeanPool.SingleCopyStabilizer.binaryPivot u hu) u b

Instances For

source

@[simp]

theorem LeanPool.SingleCopyStabilizer.binaryRound_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (L : BinarySpace ι) (b : ZMod 2) :

binaryRound L 0 b = L

source

theorem LeanPool.SingleCopyStabilizer.binaryRound_of_ne {ι : Type u_1} [Fintype ι] [DecidableEq ι] (L : BinarySpace ι) (u : BinaryVec ι) (b : ZMod 2) (hu : u ≠ 0) :

binaryRound L u b = updatedSpace L (binaryPivot u hu) u b

source

theorem LeanPool.SingleCopyStabilizer.binaryRound_isotropic {ι : Type u_1} [Fintype ι] [DecidableEq ι] (L : BinarySpace ι) (hL : IsIsotropic L) (u : BinaryVec ι) (b : ZMod 2) :

IsIsotropic (binaryRound L u b)

source

theorem LeanPool.SingleCopyStabilizer.binaryRound_finrank {ι : Type u_1} [Fintype ι] [DecidableEq ι] (L : BinarySpace ι) (u : BinaryVec ι) (b : ZMod 2) :

Module.finrank (ZMod 2) ↥(binaryRound L u b) = Module.finrank (ZMod 2) ↥L

source

theorem LeanPool.SingleCopyStabilizer.binaryRound_diagonal_mono {ι : Type u_1} [Fintype ι] [DecidableEq ι] (L : BinarySpace ι) (u : BinaryVec ι) (b : ZMod 2) (hu : u ∈ dotOrthogonal (diagonalSpace L)) :

Module.finrank (ZMod 2) ↥(diagonalSpace L) ≤ Module.finrank (ZMod 2) ↥(diagonalSpace (binaryRound L u b))

All computationally allowed differences preserve the diagonal dimension, including those which are not stabilizer X labels in the low-nullity setting.

source

theorem LeanPool.SingleCopyStabilizer.binaryRound_exists_progress {ι : Type u_1} [Fintype ι] [DecidableEq ι] (L : BinarySpace ι) (hL : IsIsotropic L) (u : BinaryVec ι) (hu : u ∈ xProjection L) (hzero : u ≠ 0) :

∃ (b : ZMod 2), Module.finrank (ZMod 2) ↥(diagonalSpace L) < Module.finrank (ZMod 2) ↥(diagonalSpace (binaryRound L u b))

Every nonzero stabilizer X label has at least one successful correction.

source

noncomputable def LeanPool.SingleCopyStabilizer.safeBinaryRound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (L : BinarySpace ι) (u : BinaryVec ι) (b : ZMod 2) :

BinarySpace ι

Totalize sampling from the X projection by leaving the label space unchanged on labels outside that projection. This is used for exact learning; those labels can have positive probability for states of positive nullity.

Equations

LeanPool.SingleCopyStabilizer.safeBinaryRound L u b = if u ∈ LeanPool.SingleCopyStabilizer.xProjection L then LeanPool.SingleCopyStabilizer.binaryRound L u b else L

Instances For

source

theorem LeanPool.SingleCopyStabilizer.safeBinaryRound_of_mem {ι : Type u_1} [Fintype ι] [DecidableEq ι] (L : BinarySpace ι) (u : BinaryVec ι) (b : ZMod 2) (hu : u ∈ xProjection L) :

safeBinaryRound L u b = binaryRound L u b

source

theorem LeanPool.SingleCopyStabilizer.safeBinaryRound_of_not_mem {ι : Type u_1} [Fintype ι] [DecidableEq ι] (L : BinarySpace ι) (u : BinaryVec ι) (b : ZMod 2) (hu : u ∉ xProjection L) :

safeBinaryRound L u b = L

source

theorem LeanPool.SingleCopyStabilizer.safeBinaryRound_isotropic {ι : Type u_1} [Fintype ι] [DecidableEq ι] (L : BinarySpace ι) (hL : IsIsotropic L) (u : BinaryVec ι) (b : ZMod 2) :

IsIsotropic (safeBinaryRound L u b)

source

theorem LeanPool.SingleCopyStabilizer.safeBinaryRound_finrank {ι : Type u_1} [Fintype ι] [DecidableEq ι] (L : BinarySpace ι) (u : BinaryVec ι) (b : ZMod 2) :

Module.finrank (ZMod 2) ↥(safeBinaryRound L u b) = Module.finrank (ZMod 2) ↥L

source

theorem LeanPool.SingleCopyStabilizer.safeBinaryRound_diagonal_mono {ι : Type u_1} [Fintype ι] [DecidableEq ι] (L : BinarySpace ι) (hL : IsIsotropic L) (u : BinaryVec ι) (b : ZMod 2) :

Module.finrank (ZMod 2) ↥(diagonalSpace L) ≤ Module.finrank (ZMod 2) ↥(diagonalSpace (safeBinaryRound L u b))