The algebraic adaptive update

The supporting linear algebra is stated over a field and is specialized to qubits (ZMod 2) in Round.lean. These are statements about unsigned Pauli labels. The qudit extension is outside this formalization. The identification with unitary conjugation is proved in the physical gate modules.

@[reducible, inline]

abbrev LeanPool.SingleCopyStabilizer.Vec (𝕜 : Type u_3) (ι : Type u_4) : Type (max u_3 u_4)

Coordinate vectors indexed by the register sites.

Equations

• LeanPool.SingleCopyStabilizer.Vec 𝕜 ι = (ι → 𝕜)

@[reducible, inline]

abbrev LeanPool.SingleCopyStabilizer.Label (𝕜 : Type u_3) (ι : Type u_4) : Type (max u_4 u_3)

Pauli labels paired into X and Z coordinate vectors.

Equations

• LeanPool.SingleCopyStabilizer.Label 𝕜 ι = (LeanPool.SingleCopyStabilizer.Vec 𝕜 ι × LeanPool.SingleCopyStabilizer.Vec 𝕜 ι)

def LeanPool.SingleCopyStabilizer.symplectic {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] (a b : Label 𝕜 ι) : 𝕜

The alternating X-Z pairing controlling Pauli commutation.

Equations

• LeanPool.SingleCopyStabilizer.symplectic a b = a.1 ⬝ᵥ b.2 - a.2 ⬝ᵥ b.1

def LeanPool.SingleCopyStabilizer.IsIsotropic {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] (L : Submodule 𝕜 (Label 𝕜 ι)) : Prop

Pairwise vanishing of the symplectic pairing on a label space.

Equations

• LeanPool.SingleCopyStabilizer.IsIsotropic L = ∀ a ∈ L, ∀ b ∈ L, LeanPool.SingleCopyStabilizer.symplectic a b = 0

def LeanPool.SingleCopyStabilizer.diagonalSpace {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} (L : Submodule 𝕜 (Label 𝕜 ι)) : Submodule 𝕜 (Vec 𝕜 ι)

Z labels whose paired X coordinate is zero in the label space.

Equations

• LeanPool.SingleCopyStabilizer.diagonalSpace L = { carrier := {s : LeanPool.SingleCopyStabilizer.Vec 𝕜 ι | (0, s) ∈ L}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem LeanPool.SingleCopyStabilizer.mem_diagonalSpace {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} (L : Submodule 𝕜 (Label 𝕜 ι)) (s : Vec 𝕜 ι) : s ∈ diagonalSpace L ↔ (0, s) ∈ L

theorem LeanPool.SingleCopyStabilizer.x_orthogonal_diagonal {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] {L : Submodule 𝕜 (Label 𝕜 ι)} (hL : IsIsotropic L) {x z s : Vec 𝕜 ι} (hxz : (x, z) ∈ L) (hs : s ∈ diagonalSpace L) : x ⬝ᵥ s = 0

Commuting with a diagonal stabilizer forces orthogonality of the X label.

def LeanPool.SingleCopyStabilizer.shearX {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} (i : ι) (w x : Vec 𝕜 ι) : Vec 𝕜 ι

X-coordinate action of a simultaneous controlled-SUM shear.

Equations

• LeanPool.SingleCopyStabilizer.shearX i w x = x - x i • w

def LeanPool.SingleCopyStabilizer.shearZ {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (i : ι) (w z : Vec 𝕜 ι) : Vec 𝕜 ι

Contragradient action on Z coordinates.

Equations

• LeanPool.SingleCopyStabilizer.shearZ i w z = z + (w ⬝ᵥ z) • Pi.single i 1

@[simp]

theorem LeanPool.SingleCopyStabilizer.shearX_pivot {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} (i : ι) {w : Vec 𝕜 ι} (hw : w i = 0) (x : Vec 𝕜 ι) : shearX i w x i = x i

@[simp]

theorem LeanPool.SingleCopyStabilizer.shearZ_pivot {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (i : ι) (w z : Vec 𝕜 ι) : shearZ i w z i = z i + w ⬝ᵥ z

theorem LeanPool.SingleCopyStabilizer.shear_pairing {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (i : ι) {w : Vec 𝕜 ι} (hw : w i = 0) (x z : Vec 𝕜 ι) : shearX i w x ⬝ᵥ shearZ i w z = x ⬝ᵥ z

The two shear actions preserve the X-Z pairing.

def LeanPool.SingleCopyStabilizer.shearZEquiv {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (i : ι) (w : Vec 𝕜 ι) (hw : w i = 0) : Vec 𝕜 ι ≃ₗ[𝕜] Vec 𝕜 ι

The invertible dual shear when the target mask vanishes at the pivot.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.SingleCopyStabilizer.pivot_concentrates {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [DecidableEq ι] {u : Vec 𝕜 ι} {i : ι} (hu : u i = 1) : shearX i (u - Pi.single i 1) u = Pi.single i 1

A normalized sample is concentrated on the chosen pivot.

theorem LeanPool.SingleCopyStabilizer.pivot_diagonal_zero {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {u s : Vec 𝕜 ι} {i : ι} (horth : u ⬝ᵥ s = 0) : shearZ i (u - Pi.single i 1) s i = 0

Orthogonality is exactly what makes the transformed old Z label vanish at the pivot.

def LeanPool.SingleCopyStabilizer.localCorrection {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [DecidableEq ι] (i : ι) (b : 𝕜) (a : Label 𝕜 ι) : Label 𝕜 ι

A local Fourier/phase correction, with determinant one over any field.

Equations

• LeanPool.SingleCopyStabilizer.localCorrection i b a = (Function.update a.1 i (a.2 i + b * a.1 i), Function.update a.2 i (-a.1 i))

theorem LeanPool.SingleCopyStabilizer.localCorrection_old_diagonal {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [DecidableEq ι] {s : Vec 𝕜 ι} {i : ι} (hs : s i = 0) (b : 𝕜) : localCorrection i b (0, s) = (0, s)

theorem LeanPool.SingleCopyStabilizer.localCorrection_new_diagonal {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [DecidableEq ι] (i : ι) (z : Vec 𝕜 ι) : localCorrection i (-z i) (Pi.single i 1, z) = (0, Function.update z i (-1))

def LeanPool.SingleCopyStabilizer.adaptiveUpdate {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (i : ι) (u : Vec 𝕜 ι) (b : 𝕜) (a : Label 𝕜 ι) : Label 𝕜 ι

Compose the pivot shear with its local Fourier and phase correction.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.SingleCopyStabilizer.adaptiveUpdate_preserves_diagonal {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {u s : Vec 𝕜 ι} {i : ι} (horth : u ⬝ᵥ s = 0) (b : 𝕜) : adaptiveUpdate i u b (0, s) = (0, shearZ i (u - Pi.single i 1) s)

theorem LeanPool.SingleCopyStabilizer.adaptiveUpdate_creates_diagonal {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {u v : Vec 𝕜 ι} {i : ι} (hu : u i = 1) : adaptiveUpdate i u (-shearZ i (u - Pi.single i 1) v i) (u, v) = (0, Function.update (shearZ i (u - Pi.single i 1) v) i (-1))

def LeanPool.SingleCopyStabilizer.adaptiveUpdateMap {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (i : ι) (u : Vec 𝕜 ι) (b : 𝕜) : Label 𝕜 ι →ₗ[𝕜] Label 𝕜 ι

The linear map implementing the observed symplectic update.

Equations

• LeanPool.SingleCopyStabilizer.adaptiveUpdateMap i u b = { toFun := LeanPool.SingleCopyStabilizer.adaptiveUpdate i u b, map_add' := ⋯, map_smul' := ⋯ }

theorem LeanPool.SingleCopyStabilizer.symplectic_eq_sum {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] (a c : Label 𝕜 ι) : symplectic a c = ∑ j : ι, (a.1 j * c.2 j - a.2 j * c.1 j)

theorem LeanPool.SingleCopyStabilizer.localCorrection_symplectic {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (i : ι) (b : 𝕜) (a c : Label 𝕜 ι) : symplectic (localCorrection i b a) (localCorrection i b c) = symplectic a c

theorem LeanPool.SingleCopyStabilizer.adaptiveUpdate_symplectic {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (i : ι) (u : Vec 𝕜 ι) (b : 𝕜) (hu : u i = 1) (a c : Label 𝕜 ι) : symplectic (adaptiveUpdate i u b a) (adaptiveUpdate i u b c) = symplectic a c

theorem LeanPool.SingleCopyStabilizer.symplectic_nondegenerate {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] (a : Label 𝕜 ι) (h : ∀ (c : Label 𝕜 ι), symplectic a c = 0) : a = 0

theorem LeanPool.SingleCopyStabilizer.adaptiveUpdate_injective {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (i : ι) (u : Vec 𝕜 ι) (b : 𝕜) (hu : u i = 1) : Function.Injective ⇑(adaptiveUpdateMap i u b)

def LeanPool.SingleCopyStabilizer.updatedSpace {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (L : Submodule 𝕜 (Label 𝕜 ι)) (i : ι) (u : Vec 𝕜 ι) (b : 𝕜) : Submodule 𝕜 (Label 𝕜 ι)

The image label space after the observed adaptive update.

Equations

• LeanPool.SingleCopyStabilizer.updatedSpace L i u b = Submodule.map (LeanPool.SingleCopyStabilizer.adaptiveUpdateMap i u b) L

theorem LeanPool.SingleCopyStabilizer.updatedSpace_isotropic {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (L : Submodule 𝕜 (Label 𝕜 ι)) (hL : IsIsotropic L) (i : ι) (u : Vec 𝕜 ι) (b : 𝕜) (hu : u i = 1) : IsIsotropic (updatedSpace L i u b)

theorem LeanPool.SingleCopyStabilizer.updatedSpace_finrank {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (L : Submodule 𝕜 (Label 𝕜 ι)) (i : ι) (u : Vec 𝕜 ι) (b : 𝕜) (hu : u i = 1) : Module.finrank 𝕜 ↥(updatedSpace L i u b) = Module.finrank 𝕜 ↥L

theorem LeanPool.SingleCopyStabilizer.diagonal_finrank_monotone {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (L : Submodule 𝕜 (Label 𝕜 ι)) (u : Vec 𝕜 ι) (i : ι) (b : 𝕜) (hu : u i = 1) (horth : ∀ s ∈ diagonalSpace L, u ⬝ᵥ s = 0) : Module.finrank 𝕜 ↥(diagonalSpace L) ≤ Module.finrank 𝕜 ↥(diagonalSpace (updatedSpace L i u b))

Every choice of the local correction does not decrease diagonal dimension. Only orthogonality is needed, not membership of the sample in the X projection; this distinction is essential to the low-nullity proof.

theorem LeanPool.SingleCopyStabilizer.new_diagonal_independent {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [DecidableEq ι] {D : Submodule 𝕜 (Vec 𝕜 ι)} {i : ι} (hD : ∀ s ∈ D, s i = 0) (z : Vec 𝕜 ι) : Function.update z i (-1) ∉ D

The newly created diagonal label is outside the span of all old labels, because the entire old subspace vanishes at the pivot.

theorem LeanPool.SingleCopyStabilizer.diagonal_finrank_strict_progress {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (L L' : Submodule 𝕜 (Label 𝕜 ι)) (u v : Vec 𝕜 ι) (i : ι) (hu : u i = 1) (huv : (u, v) ∈ L) (horth : ∀ s ∈ diagonalSpace L, u ⬝ᵥ s = 0) (hupdate : ∀ a ∈ L, adaptiveUpdate i u (-shearZ i (u - Pi.single i 1) v i) a ∈ L') : Module.finrank 𝕜 ↥(diagonalSpace L) < Module.finrank 𝕜 ↥(diagonalSpace L')

Exact algebraic content of the increase in diagonal-stabilizer dimension. L' can be any submodule containing the updated labels; no dimension increase is assumed. The result is deduced from the explicit fresh pivot coordinate.

theorem LeanPool.SingleCopyStabilizer.exists_diagonal_finrank_progress {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (L : Submodule 𝕜 (Label 𝕜 ι)) (hL : IsIsotropic L) (u v : Vec 𝕜 ι) (i : ι) (hu : u i = 1) (huv : (u, v) ∈ L) : ∃ (b : 𝕜), Module.finrank 𝕜 ↥(diagonalSpace L) < Module.finrank 𝕜 ↥(diagonalSpace (updatedSpace L i u b))

For an isotropic space and a genuine nonzero stabilizer X label, there exists a local slope which strictly increases diagonal dimension.