The matrix model of the Pauli group

Pauli/Basic.lean builds PauliString n as a group of symbols. This file supplies the operators those symbols denote, toMatrix s : Matrix (Bits n) (Bits n) ℂ, proves that toMatrix is a faithful *-monoid homomorphism, and so turns every statement there into a statement about matrices — which is the form Rotation.lean consumes.

The index type, and why there are no Kronecker products here

The Hilbert space is indexed by bit strings, Bits n := Fin n → ZMod 2, of cardinality 2^n (card_bits). So Matrix (Bits n) (Bits n) ℂ is a 2^n × 2^n matrix algebra — the operator algebra of n qubits, up to the reindexing provided by PauliString.bitsMatrixEquiv in Pauli/Tensor.lean — and

toMatrix s a b = i^{phase} · (-1)^{z ⬝ᵥ b} when a = b + x, and 0 otherwise

is i^{phase} X^x Z^z written out: Z^z is diagonal with entries (-1)^{z·b}, and X^x shifts the basis label by x. Every Pauli string is a monomial matrix — one non-zero entry per row and per column — and that is what this form buys: the matrix-product sum ∑_k A_{ik} B_{kj} has exactly one surviving term, so toMatrix_mul is Finset.sum_eq_single plus bookkeeping in ZMod 4, and no induction on n appears anywhere in the file.

The definition does factorize over sites — toMatrix ⟨x,z,0⟩ a b = ∏ᵢ ([aᵢ = bᵢ + xᵢ]·(−1)^{zᵢbᵢ}), an n-fold tensor product of X^{xᵢ} Z^{zᵢ} — but those factors range over {I, X, Z, XZ}, and XZ = −i Y is not in the set {I,X,Y,Z} of def:pauli_basis. Reaching that set needs the further phase normalization phase = #{Y-sites} mod 4. Pauli/Tensor.lean proves the phase-correct tensor identity and provides that positive representative; neither fact is assumed by the matrix model.

Main definitions

• Bits n: the computational basis labels Fin n → ZMod 2.
• iPow, negOnePow: the characters k ↦ i^k on ZMod 4 and a ↦ (-1)^a on ZMod 2.
• PauliString.toMatrix: the matrix of a Pauli string.

Main results

• toMatrix_one, toMatrix_mul, toMatrix_star: toMatrix is a *-monoid homomorphism on the nose, not projectively. This is what carrying phase : ZMod 4 in PauliString was for.
• toMatrix_injective: the representation is faithful — distinct group elements, phase variants included, are distinct operators — so nothing below is a statement about a collapsed model. It does not say the image is linearly independent, and cannot: toMatrix (phaseMul 1 s) is i · toMatrix s. Linear independence is a statement about a basis; the one instance of it needed in this file is toMatrix_mul_ne_smul, and the orthogonality of the signless classes is in Pauli/Trace.lean.
• toMatrix_commute_or_anticommute: the commute-or-anticommute dichotomy as a statement about operators. This is the exhaustiveness of the two cases of apd:eq:pauli_rotation_branch, which Lean4LPD.rot_conj_of_commute and Lean4LPD.rot_conj_of_anticommute cannot see over an abstract algebra. toMatrix_commute_iff and toMatrix_anticommute_iff identify the two cases with sympForm s t = 0 and sympForm s t = 1.
• star_toMatrix_of_isSelfAdjoint and toMatrix_mul_self_of_isSelfAdjoint discharge, from the single hypothesis IsSelfAdjoint s, both hypotheses rot_conj_of_commute, rot_conj_of_anticommute and rot_mem_unitary carry between them.
• toMatrix_mul_ne_smul and linearIndependent_toMatrix_mul_pair: for anticommuting G, s the partner G s is not a scalar multiple of s, and the two are genuinely linearly independent — which needs toMatrix_ne_zero on top of non-collinearity. Rotation.lean records that reading i sin(dt) as the amplitude of a new transition needs exactly this and that distinctness does not give it, exhibiting G = Z, P = E₁₀ in Matrix (Fin 2) (Fin 2) ℂ where both rotation hypotheses hold and G * P = -P. Inside the Pauli group that cannot happen, and this is the theorem that says so.

Pauli/Branch.lean assembles these into the paper's branching rule.

Fourth and second roots of unity

iPow and negOnePow are the two characters the representation needs. Everything about them reduces to I ^ 4 = 1 and a finite case check.

noncomputable def Lean4LPD.iPow (k : ZMod 4) : ℂ

i^k for an exponent in ZMod 4. Well defined because I ^ 4 = 1.

Equations

• Lean4LPD.iPow k = Complex.I ^ k.val

noncomputable def Lean4LPD.negOnePow (a : ZMod 2) : ℂ

(-1)^a for an exponent in ZMod 2.

Equations

• Lean4LPD.negOnePow a = (-1) ^ a.val

@[simp]

theorem Lean4LPD.iPow_zero : iPow 0 = 1

theorem Lean4LPD.iPow_one : iPow 1 = Complex.I

@[simp]

theorem Lean4LPD.iPow_two : iPow 2 = -1

theorem Lean4LPD.iPow_three : iPow 3 = -Complex.I

theorem Lean4LPD.iPow_add (k l : ZMod 4) : iPow (k + l) = iPow k * iPow l

@[simp]

theorem Lean4LPD.negOnePow_zero : negOnePow 0 = 1

@[simp]

theorem Lean4LPD.negOnePow_one : negOnePow 1 = -1

theorem Lean4LPD.negOnePow_add (a b : ZMod 2) : negOnePow (a + b) = negOnePow a * negOnePow b

@[simp]

theorem Lean4LPD.iPow_signPhase (a : ZMod 2) : iPow (signPhase a) = negOnePow a

The two characters agree where they must: (-1)^a = i^{2a}.

@[simp]

theorem Lean4LPD.negOnePow_mul_self (a : ZMod 2) : negOnePow a * negOnePow a = 1

theorem Lean4LPD.iPow_ne_zero (k : ZMod 4) : iPow k ≠ 0

theorem Lean4LPD.negOnePow_ne_zero (a : ZMod 2) : negOnePow a ≠ 0

theorem Lean4LPD.negOnePow_injective : Function.Injective negOnePow

theorem Lean4LPD.negOnePow_eq_one_iff {a : ZMod 2} : negOnePow a = 1 ↔ a = 0

theorem Lean4LPD.iPow_eq_one_iff {k : ZMod 4} : iPow k = 1 ↔ k = 0

theorem Lean4LPD.iPow_injective : Function.Injective iPow

@[simp]

theorem Lean4LPD.conj_negOnePow (a : ZMod 2) : (starRingEnd ℂ) (negOnePow a) = negOnePow a

theorem Lean4LPD.conj_iPow (k : ZMod 4) : (starRingEnd ℂ) (iPow k) = iPow (-k)

@[simp]

theorem Lean4LPD.star_negOnePow (a : ZMod 2) : star (negOnePow a) = negOnePow a

theorem Lean4LPD.star_iPow (k : ZMod 4) : star (iPow k) = iPow (-k)

The Hilbert space

@[reducible, inline]

abbrev Lean4LPD.Bits (n : ℕ) : Type

The computational basis of n qubits, indexed by bit strings.

Equations

• Lean4LPD.Bits n = (Fin n → ZMod 2)

theorem Lean4LPD.card_bits (n : ℕ) : Fintype.card (Bits n) = 2 ^ n

There are 2^n basis states, so Matrix (Bits n) (Bits n) ℂ is a 2^n × 2^n matrix algebra. Rotation.lean's closing example names the same algebra as Matrix (Fin (2^n)) (Fin (2^n)) ℂ, which is a different Lean type; the reindexing along Bits n ≃ Fin (2^n) is supplied by PauliString.bitsEquivFin in Pauli/Tensor.lean, together with the induced equivalence of matrix algebras PauliString.bitsMatrixEquiv.

The representation

noncomputable def Lean4LPD.PauliString.toMatrix {n : ℕ} (s : PauliString n) : Matrix (Bits n) (Bits n) ℂ

The matrix representation i^{phase} X^{x} Z^{z} of a Pauli string, as a monomial matrix on bit strings: the entry in row a, column b is non-zero only when a = b + x, where it is i^{phase} (-1)^{z ⬝ᵥ b}.

This is a definition. That it deserves the name is toMatrix_one, toMatrix_mul, toMatrix_star (it is a *-monoid homomorphism) and toMatrix_injective (it is faithful).

Equations

• s.toMatrix = Matrix.of fun (a b : Lean4LPD.Bits n) => if a = b + s.x then Lean4LPD.iPow s.phase * Lean4LPD.negOnePow (s.z ⬝ᵥ b) else 0

theorem Lean4LPD.PauliString.toMatrix_apply {n : ℕ} (s : PauliString n) (a b : Bits n) : s.toMatrix a b = if a = b + s.x then iPow s.phase * negOnePow (s.z ⬝ᵥ b) else 0

theorem Lean4LPD.PauliString.toMatrix_apply_add {n : ℕ} (s : PauliString n) (b : Bits n) : s.toMatrix (b + s.x) b = iPow s.phase * negOnePow (s.z ⬝ᵥ b)

The one non-zero entry of each column.

theorem Lean4LPD.PauliString.toMatrix_apply_ne {n : ℕ} (s : PauliString n) {a b : Bits n} (h : a ≠ b + s.x) : s.toMatrix a b = 0

@[simp]

theorem Lean4LPD.PauliString.toMatrix_one {n : ℕ} : toMatrix 1 = 1

@[simp]

theorem Lean4LPD.PauliString.toMatrix_phaseMul {n : ℕ} (k : ZMod 4) (s : PauliString n) : (phaseMul k s).toMatrix = iPow k • s.toMatrix

theorem Lean4LPD.PauliString.toMatrix_mul {n : ℕ} (s t : PauliString n) : s.toMatrix * t.toMatrix = (s * t).toMatrix

The representation is multiplicative. Exactly, with no phase ambiguity: this is what phase : ZMod 4 was carried for.

theorem Lean4LPD.PauliString.toMatrix_star {n : ℕ} (s : PauliString n) : star s.toMatrix = (star s).toMatrix

The representation respects the adjoint. This is the theorem that justifies calling PauliString's star an adjoint at all — in Pauli/Basic.lean it is only defined, as the group inverse.

Faithfulness

theorem Lean4LPD.PauliString.toMatrix_injective {n : ℕ} : Function.Injective toMatrix

The representation is faithful. Distinct Pauli strings — including strings differing only in their phase — are distinct operators, so nothing proved through toMatrix is a statement about a collapsed model.

The dichotomy, at the level of operators

theorem Lean4LPD.PauliString.toMatrix_commute_or_anticommute {n : ℕ} (s t : PauliString n) : Commute s.toMatrix t.toMatrix ∨ s.toMatrix * t.toMatrix = -(t.toMatrix * s.toMatrix)

Any two Pauli operators either commute or anticommute. The operator form of PauliString.commute_or_anticommute, and the exhaustiveness that Lean4LPD.rot_conj_of_commute / Lean4LPD.rot_conj_of_anticommute presuppose: those two cover a commuting and an anticommuting generator, and over an abstract algebra nothing rules out a third case. For Pauli operators it shows that the two cases of apd:eq:pauli_rotation_branch are the only ones.

theorem Lean4LPD.PauliString.toMatrix_commute {n : ℕ} {s t : PauliString n} (h : s.sympForm t = 0) : Commute s.toMatrix t.toMatrix

Commuting Pauli strings give commuting operators.

theorem Lean4LPD.PauliString.toMatrix_anticommute {n : ℕ} {s t : PauliString n} (h : s.sympForm t = 1) : s.toMatrix * t.toMatrix = -(t.toMatrix * s.toMatrix)

Anticommuting Pauli strings give anticommuting operators — the hypothesis Lean4LPD.rot_conj_of_anticommute takes, spelled the way that file spells it.

theorem Lean4LPD.PauliString.toMatrix_commute_iff {n : ℕ} (s t : PauliString n) : Commute s.toMatrix t.toMatrix ↔ s.sympForm t = 0

The commuting branch condition is an iff at the level of operators, not just an implication: toMatrix is injective, so operators commuting forces the symbols to. Without this the if in pauli_rotation_branch would be a sufficient condition for the paper's [G,P] = 0 rather than a rendering of it.

theorem Lean4LPD.PauliString.toMatrix_anticommute_iff {n : ℕ} (s t : PauliString n) : s.toMatrix * t.toMatrix = -(t.toMatrix * s.toMatrix) ↔ s.sympForm t = 1

The anticommuting branch condition, likewise an iff.

Discharging Rotation.lean's hypotheses

theorem Lean4LPD.PauliString.star_toMatrix_of_isSelfAdjoint {n : ℕ} {s : PauliString n} (h : IsSelfAdjoint s) : star s.toMatrix = s.toMatrix

A Hermitian Pauli string is a self-adjoint operator: discharges star G = G in Lean4LPD.rot_mem_unitary.

theorem Lean4LPD.PauliString.toMatrix_mul_self_of_isSelfAdjoint {n : ℕ} {s : PauliString n} (h : IsSelfAdjoint s) : s.toMatrix * s.toMatrix = 1

A Hermitian Pauli string is an involution: discharges hG : G * G = 1, the hypothesis the two branch lemmas and rot_mem_unitary carry (rot_zero, commute_rot, rot_mul_eq_mul_rot_neg and star_rot do not). Note this comes from the same hypothesis as self-adjointness — Pauli/Basic.lean's isSelfAdjoint_iff_mul_self_eq_one.

theorem Lean4LPD.PauliString.toMatrix_mul_toMatrix_inv {n : ℕ} (s : PauliString n) : s.toMatrix * s⁻¹.toMatrix = 1

Every Pauli operator is invertible, with toMatrix s⁻¹ as inverse.

theorem Lean4LPD.PauliString.toMatrix_ne_zero {n : ℕ} (s : PauliString n) : s.toMatrix ≠ 0

No Pauli operator is zero: the entry at (b + x, b) is i^{phase}, a fourth root of unity.

theorem Lean4LPD.PauliString.isSelfAdjoint_toMatrix_iff {n : ℕ} {s : PauliString n} : IsSelfAdjoint s.toMatrix ↔ IsSelfAdjoint s

Hermiticity transfers in both directions. toMatrix_star alone gives only symbol-to-operator; faithfulness supplies the converse, so a Pauli handed over as a self-adjoint operator — which is how the generators G_g enter apd:thm:local_flow_k_local — is a self-adjoint Pauli string, and isSelfAdjoint_iff_mul_self_eq_one applies to it.

Independence of the two branch terms

theorem Lean4LPD.PauliString.toMatrix_mul_ne_smul_aux {n : ℕ} {G s : PauliString n} (h : G.sympForm s = 1) (c : ℂ) : (G * s).toMatrix ≠ c • s.toMatrix

The two branch terms are independent. When G anticommutes with s, the partner G s is not a scalar multiple of s, so the i sin(dt) coefficient in apd:eq:pauli_rotation_branch really is the amplitude of a new transition rather than a rescaling of the old one.

Rotation.lean states that the damping consequence of the branching rule needs exactly this and that mere distinctness is not enough, exhibiting G = Z, P = E₁₀ in Matrix (Fin 2) (Fin 2) ℂ — both rotation hypotheses hold there and G * P = -P. That example is not a Pauli string, and this theorem is why no Pauli string can play its role.

theorem Lean4LPD.PauliString.toMatrix_mul_ne_smul {n : ℕ} {G s : PauliString n} (h : G.sympForm s = 1) (c : ℂ) : (G * s).toMatrix ≠ c • s.toMatrix

The same statement, named for what it is used for.

theorem Lean4LPD.PauliString.linearIndependent_toMatrix_mul_pair {n : ℕ} {G s : PauliString n} (h : G.sympForm s = 1) : LinearIndependent ℂ ![s.toMatrix, (G * s).toMatrix]

The two branch terms are linearly independent. Non-collinearity (toMatrix_mul_ne_smul) is not by itself linear independence — it leaves open a • A = 0 with a ≠ 0 — and what closes the gap is toMatrix_ne_zero. This is the property Rotation.lean names as what the damping consequence of apd:eq:pauli_rotation_branch needs.

One qubit, entry by entry

The check that the definition really is the operator it is named for. Everything above is a statement about toMatrix, so a sign or transpose slip here would be invisible to the kernel and fatal to the correspondence with the paper's operators. Bits 1 has the two labels 0 and 1; entries are listed in that order, so the three displays below read

X = ((0,1),(1,0)), Z = ((1,0),(0,−1)), Y = ((0,−i),(i,0)),

which are the standard Pauli matrices with the standard signs.

X1 and Z1 are the one-qubit case of the phase-zero factorization toMatrix ⟨x,z,0⟩ = ⨂ᵢ X^{xᵢ} Z^{zᵢ}. Y1 is deliberately not: at (x,z) = (1,1) the phase-zero string is X Z = −i Y, and the +Y displayed below is the phase-one representative — exactly the #{Y-sites} normalization that reaching the set {I,X,Y,Z}^{⊗n} of def:pauli_basis requires. phase = 3 would give −Y, and isSelfAdjoint_iff_phase admits both. The general tensor and phase identities are proved in Pauli/Tensor.lean; these are finite sanity checks.