The entrywise Pauli model as a genuine tensor product

def:pauli_basis builds the Pauli basis from tensor products of the one-qubit matrices I, X, Y, Z, whereas this library computes with an entrywise model toMatrix. This file proves that the two agree: toMatrix s is a power of i times the Kronecker product of the single-qubit Pauli matrices of s.

The one-qubit matrices are specified independently, by their entries, and tensorPauli is built recursively from Mathlib's Kronecker product. The comparison with toMatrix keeps the phase: the positive tensor has phase exponent equal to the number of Y sites modulo four (yPhase), whereas herm uses only the parity of that number. In particular, for two Y sites the two representatives differ by a minus sign.

The algebra equivalence bitsMatrixEquiv at the end is noncomputable. It identifies the algebra of matrices indexed by bit strings with the 2^n by 2^n matrices, without singling out a binary or lexicographic ordering of the bit strings.

Main definitions

• qubitX, qubitY, qubitZ, qubitPauli: the one-qubit Pauli matrices, by their entries.
• tensorPauli n x z: the iterated Kronecker product of the one-qubit Paulis with bits x, z.
• yPhase x z: the number of Y sites, modulo four.
• tensorRepresentative p: the Pauli string of class p whose matrix is tensorPauli.
• bitsMatrixEquiv n: matrices indexed by Bits n as matrices indexed by Fin (2 ^ n).

Main results

• toMatrix_eq_phase_tensor: toMatrix s = iPow (s.phase - yPhase s.x s.z) • tensorPauli n s.x s.z.
• toMatrix_tensorRepresentative: toMatrix (tensorRepresentative p) = tensorPauli n p.1 p.2.
• isSelfAdjoint_tensorRepresentative, isSelfAdjoint_tensorPauli: the positive tensors are Hermitian.
• trace_star_tensorPauli_mul, trace_tensorPauli_mul: they are orthogonal for the trace pairing, with Tr (P Q) = 2 ^ n if P = Q and 0 otherwise.
• bitsMatrixEquiv_star: the change of index type preserves the adjoint.

def Lean4LPD.PauliString.qubitX : Matrix (ZMod 2) (ZMod 2) ℂ

The one-qubit X matrix in def:pauli_basis.

Equations

• Lean4LPD.PauliString.qubitX = ![![0, 1], ![1, 0]]

def Lean4LPD.PauliString.qubitY : Matrix (ZMod 2) (ZMod 2) ℂ

The one-qubit Y matrix in def:pauli_basis.

Equations

• Lean4LPD.PauliString.qubitY = ![![0, -Complex.I], ![Complex.I, 0]]

def Lean4LPD.PauliString.qubitZ : Matrix (ZMod 2) (ZMod 2) ℂ

The one-qubit Z matrix in def:pauli_basis.

Equations

• Lean4LPD.PauliString.qubitZ = ![![1, 0], ![0, -1]]

def Lean4LPD.PauliString.qubitPauli (x z : ZMod 2) : Matrix (ZMod 2) (ZMod 2) ℂ

The positive I/X/Z/Y representative of the local binary class, as in def:pauli_basis.

Equations

• Lean4LPD.PauliString.qubitPauli x z = if x = 0 then if z = 0 then 1 else Lean4LPD.PauliString.qubitZ else if z = 0 then Lean4LPD.PauliString.qubitX else Lean4LPD.PauliString.qubitY

noncomputable def Lean4LPD.PauliString.qubitXZ (x z : ZMod 2) : Matrix (ZMod 2) (ZMod 2) ℂ

The phase-free one-qubit factor X^x Z^z, by its entries. This is the local factor of the entrywise model toMatrix; at x = z = 1 it equals -iY, not the Y of def:pauli_basis.

Equations

• Lean4LPD.PauliString.qubitXZ x z a b = if a = b + x then Lean4LPD.negOnePow (z * b) else 0

theorem Lean4LPD.PauliString.qubitXZ_eq_phase_qubitPauli (x z : ZMod 2) : qubitXZ x z = iPow (-↑(x * z).val) • qubitPauli x z

The one-qubit phase correction: X^x Z^z is i ^ (-(x z)) times the positive Pauli matrix of def:pauli_basis. Only the Y site x = z = 1 carries a nontrivial phase.

def Lean4LPD.PauliString.yPhase {n : ℕ} (x z : Bits n) : ZMod 4

The exact Y-site phase modulo four, finer than the parity used by herm. This is the positive tensor-product convention in def:pauli_basis.

Equations

• Lean4LPD.PauliString.yPhase x z = ∑ i : Fin n, ↑(x i * z i).val

theorem Lean4LPD.PauliString.yPhase_succ {n : ℕ} (x z : Bits (n + 1)) : yPhase x z = ↑(x 0 * z 0).val + yPhase (Fin.tail x) (Fin.tail z)

Head/tail decomposition of the Y-site phase, supporting def:pauli_basis.

noncomputable def Lean4LPD.PauliString.tensorPauli (n : ℕ) : Bits n → Bits n → Matrix (Bits n) (Bits n) ℂ

Iterated, genuine Kronecker product of the independently specified one-qubit Paulis. The empty tensor is the one-by-one identity (def:pauli_basis).

Equations

• One or more equations did not get rendered due to their size.
• Lean4LPD.PauliString.tensorPauli 0 x_3 x_4 = 1

theorem Lean4LPD.PauliString.tensorPauli_succ_apply {n : ℕ} (x z a b : Bits (n + 1)) : tensorPauli (n + 1) x z a b = qubitPauli (x 0) (z 0) (a 0) (b 0) * tensorPauli n (Fin.tail x) (Fin.tail z) (Fin.tail a) (Fin.tail b)

The bit-indexed tensor product acts by the local matrix entry times its tail entry, as required by def:pauli_basis.

def Lean4LPD.PauliString.dropFirst {n : ℕ} (s : PauliString (n + 1)) : PauliString n

Drop the first tensor factor, retaining the global phase in the remaining string; an auxiliary definition for def:pauli_basis.

Equations

• s.dropFirst = { x := Fin.tail s.x, z := Fin.tail s.z, phase := s.phase }

theorem Lean4LPD.PauliString.toMatrix_split {n : ℕ} (s : PauliString (n + 1)) (a b : Bits (n + 1)) : s.toMatrix a b = qubitXZ (s.x 0) (s.z 0) (a 0) (b 0) * s.dropFirst.toMatrix (Fin.tail a) (Fin.tail b)

The entrywise model factors into a one-qubit X^x Z^z entry and its tail. This is the algebraic step relating toMatrix to def:pauli_basis.

theorem Lean4LPD.PauliString.toMatrix_eq_phase_tensor {n : ℕ} (s : PauliString n) : s.toMatrix = iPow (s.phase - yPhase s.x s.z) • tensorPauli n s.x s.z

The matrix model is the phase-corrected tensor product of Pauli matrices. For every Pauli string s, toMatrix s is i ^ (s.phase - yPhase s.x s.z) times the Kronecker product of the one-qubit Pauli matrices of def:pauli_basis. The identification of the entrywise model with a tensor product is thus a theorem, not an assumption.

def Lean4LPD.PauliString.tensorRepresentative {n : ℕ} (p : PauliIndex n) : PauliString n

The positive tensor representative of a signless class, as in def:pauli_basis. Unlike herm, its phase is the full count of Y sites modulo four, not only the parity.

Equations

• Lean4LPD.PauliString.tensorRepresentative p = { x := p.1, z := p.2, phase := Lean4LPD.PauliString.yPhase p.1 p.2 }

theorem Lean4LPD.PauliString.toMatrix_tensorRepresentative {n : ℕ} (p : PauliIndex n) : (tensorRepresentative p).toMatrix = tensorPauli n p.1 p.2

The matrix of the positive tensor representative is exactly the tensor product of Pauli matrices of def:pauli_basis, with no residual sign or phase.

theorem Lean4LPD.PauliString.two_mul_yPhase {n : ℕ} (x z : Bits n) : 2 * yPhase x z = signPhase (z ⬝ᵥ x)

Doubling the full Y-count phase gives the symplectic sign. This verifies the Hermiticity convention for the positive tensor basis of def:pauli_basis.

theorem Lean4LPD.PauliString.isSelfAdjoint_tensorRepresentative {n : ℕ} (p : PauliIndex n) : IsSelfAdjoint (tensorRepresentative p)

Positive tensor representatives are genuine Hermitian Pauli strings, not just tensors identified up to a freely chosen phase (def:pauli_basis).

@[simp]

theorem Lean4LPD.PauliString.cls_tensorRepresentative {n : ℕ} (p : PauliIndex n) : (tensorRepresentative p).cls = p

The positive tensor representative has the intended signless class (def:pauli_basis).

theorem Lean4LPD.PauliString.isSelfAdjoint_tensorPauli {n : ℕ} (p : PauliIndex n) : IsSelfAdjoint (tensorPauli n p.1 p.2)

The literal tensor Pauli is self-adjoint, as required by def:pauli_basis.

theorem Lean4LPD.PauliString.trace_star_tensorPauli_mul {n : ℕ} (p q : PauliIndex n) : (star (tensorPauli n p.1 p.2) * tensorPauli n q.1 q.2).trace = if p = q then 2 ^ n else 0

Orthogonality of the positive tensor Pauli family, in the unnormalized convention of def:pauli_basis. The normalized statement divides this pairing by 2^n.

theorem Lean4LPD.PauliString.trace_tensorPauli_mul {n : ℕ} (p q : PauliIndex n) : (tensorPauli n p.1 p.2 * tensorPauli n q.1 q.2).trace = if p = q then 2 ^ n else 0

The Hermitian form of the positive tensor Pauli trace pairing in def:pauli_basis.

noncomputable def Lean4LPD.PauliString.bitsEquivFin (n : ℕ) : Bits n ≃ Fin (2 ^ n)

A noncomputable numbering of the bit strings by Fin (2^n), matching the matrix dimension 2^n of def:pauli_basis. The bijection is unspecified: no particular order, such as the lexicographic one, is asserted.

Equations

• Lean4LPD.PauliString.bitsEquivFin n = Fintype.equivFinOfCardEq ⋯

noncomputable def Lean4LPD.PauliString.bitsMatrixEquiv (n : ℕ) : Matrix (Bits n) (Bits n) ℂ ≃ₐ[ℂ] Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ

The bit-indexed and dimension-indexed matrix algebras are isomorphic, the type-level bridge needed by def:pauli_basis.

Equations

• Lean4LPD.PauliString.bitsMatrixEquiv n = Matrix.reindexAlgEquiv ℂ ℂ (Lean4LPD.PauliString.bitsEquivFin n)

theorem Lean4LPD.PauliString.bitsMatrixEquiv_star (n : ℕ) (A : Matrix (Bits n) (Bits n) ℂ) : (bitsMatrixEquiv n) (star A) = star ((bitsMatrixEquiv n) A)

The change of computational-basis indexing preserves the adjoint as well as the algebra operations (def:pauli_basis).