Pauli weight, and the k_h - 1 bound on how far a rotation can move it

This file defines the support and the weight of a Pauli string (def:pauli_weight) and proves the weight estimate the damped ladder is built on: if a Pauli string G anticommutes with s, then the product G s satisfies | |G s| - |s| | ≤ |G| - 1, hence ≤ k_h - 1 for a k_h-local G.

Main definitions

• PauliString.site: the single-qubit Pauli type carried at a site, as a pair of bits.
• PauliString.support, PauliString.weight: the qubits on which a string acts non-trivially, and their number (def:pauli_weight).
• PauliString.cancelSites, PauliString.antiSites, PauliString.createSites: the three kinds of site of supp G, relative to a second string s.

Main results

• PauliString.card_cancelSites_add_card_antiSites_add_card_createSites, PauliString.weight_mul_add_card_cancelSites: the exact site bookkeeping.
• PauliString.sympForm_eq_card_antiSites: the symplectic form is #antiSites modulo two.
• PauliString.weight_mul_le, PauliString.weight_le_weight_mul_add_weight: the bounds with the full weight |G|, which need no hypothesis.
• PauliString.abs_weight_mul_sub_weight_le: the two-sided bound with |G| - 1 for an anticommuting pair.
• PauliString.weight_sub_le_weight_mul, PauliString.weight_le_weight_mul_add_kh, PauliString.weight_mul_le_weight_add_kh: the k_h forms the ladder consumes.
• PauliString.exists_commuting_weight_increase_by_full_weight: the anticommutation hypothesis cannot be dropped.

The estimate, and why it is k_h - 1 rather than k_h

The proof of apd:thm:local_flow_k_local needs: when G anticommutes with s, the partner Pauli G s satisfies

|G s| ≥ |s| - (k_h - 1) for |G| ≤ k_h,

which places the partner one rung down rather than k_h rungs down, and so supports the rung spacing w_m = k_o + (m-1)(k_h-1). In the other direction, |G s| ≤ |s| + (k_h - 1) is the one-step bound behind reading w_m as the largest weight reachable from weight k_o by m-1 anticommuting k_h-local rotations. The recursion needs only these inequalities; that the weight w_m is actually attained is not formalized. The two-sided statement, that the weight changes by at most k - 1 when G has weight at most k, is one of the consequences of apd:eq:pauli_rotation_branch on which the paper's analysis rests.

The arithmetic is exact rather than estimated. Split the support of G by what it does to s:

• cancelSites G s — G and s carry the same non-identity Pauli, so the site drops out;
• antiSites G s — both non-identity and different, so the site survives in G s;
• createSites G s — G acts where s does not, so the site is new.

These three partition supp G (card_cancelSites_add_card_antiSites_add_card_createSites), and separately |G s| + #cancel = |s| + #create (weight_mul_add_card_cancelSites). So the weight moves by #create - #cancel, and each of those is at most |G| - #anti.

The whole of the -1 is then one observation: sympForm counts antiSites mod 2 (sympForm_eq_card_antiSites), so anticommuting forces #anti odd, hence non-zero. A pair that merely commutes gets #anti even, which may be 0, and then only the weaker |G| is available — which is why the bound is a statement about the anticommuting branch and not a general fact about Pauli products.

Naming

weight is def:pauli_weight's |P|. k_h appears in the corollaries as a variable kh : ℕ, implicit and inferred from the hypothesis weight G ≤ kh, so the statements read as they do in the paper. Bounds of the form |s| - (k_h - 1) ≤ … use natural-number subtraction; this is harmless, because the additive forms (weight_le_weight_mul_add, weight_le_weight_mul_add_kh) are proved first and the subtractive ones are derived from them.

Sites

def Lean4LPD.PauliString.site {n : ℕ} (s : PauliString n) (i : Fin n) : ZMod 2 × ZMod 2

The single-qubit Pauli type that s carries at site i, as a pair of bits: (0,0) is identity, (1,0) is X-type, (0,1) is Z-type, (1,1) is Y-type.

These are labels up to phase, which is all the weight needs. At phase zero the (1,1) factor is literally X Z = −i Y, not Y; which of Y, −Y or a non-Hermitian multiple it is depends on the string's global phase, and the weight cannot see that (weight_phaseMul).

Equations

• s.site i = (s.x i, s.z i)

@[simp]

theorem Lean4LPD.PauliString.site_mul {n : ℕ} (s t : PauliString n) (i : Fin n) : (s * t).site i = s.site i + t.site i

@[simp]

theorem Lean4LPD.PauliString.site_one {n : ℕ} (i : Fin n) : site 1 i = 0

@[simp]

theorem Lean4LPD.PauliString.site_phaseMul {n : ℕ} (k : ZMod 4) (s : PauliString n) (i : Fin n) : (phaseMul k s).site i = s.site i

def Lean4LPD.PauliString.support {n : ℕ} (s : PauliString n) : Finset (Fin n)

The support of a Pauli string: the qubits it acts on non-trivially. Defined here as a Finset, since def:pauli_weight takes its cardinality.

This is the support of a single Pauli string. def:support builds the support of a general operator from it, as the union of the supports of the Pauli strings that carry a non-zero coefficient.

Equations

• s.support = {i : Fin n | s.site i ≠ 0}

@[simp]

theorem Lean4LPD.PauliString.mem_support {n : ℕ} {s : PauliString n} {i : Fin n} : i ∈ s.support ↔ s.site i ≠ 0

def Lean4LPD.PauliString.weight {n : ℕ} (s : PauliString n) : ℕ

The weight |s| of a Pauli string, def:pauli_weight: the number of qubits on which it acts non-trivially.

Equations

• s.weight = s.support.card

@[simp]

theorem Lean4LPD.PauliString.weight_one {n : ℕ} : weight 1 = 0

@[simp]

theorem Lean4LPD.PauliString.weight_phaseMul {n : ℕ} (k : ZMod 4) (s : PauliString n) : (phaseMul k s).weight = s.weight

The weight does not see the phase: it is a function of the bit vectors alone. The partner Pauli in the proof of apd:thm:local_flow_k_local is ±i G s rather than the bare product G s, and this is why bounding |G s| bounds it too.

The three kinds of site

def Lean4LPD.PauliString.cancelSites {n : ℕ} (G s : PauliString n) : Finset (Fin n)

Sites of s that the product G * s cancels: G and s carry the same non-identity Pauli there, so it drops out.

Equations

• G.cancelSites s = s.support \ (G * s).support

def Lean4LPD.PauliString.createSites {n : ℕ} (G s : PauliString n) : Finset (Fin n)

Sites that G * s creates: G acts there and s does not.

Equations

• G.createSites s = (G * s).support \ s.support

def Lean4LPD.PauliString.antiSites {n : ℕ} (G s : PauliString n) : Finset (Fin n)

Sites at which G and s locally anticommute: both act, with different Paulis.

Equations

• G.antiSites s = {i : Fin n | G.site i ≠ 0 ∧ s.site i ≠ 0 ∧ G.site i ≠ s.site i}

theorem Lean4LPD.PauliString.mem_cancelSites {n : ℕ} {G s : PauliString n} {i : Fin n} : i ∈ G.cancelSites s ↔ s.site i ≠ 0 ∧ G.site i = s.site i

theorem Lean4LPD.PauliString.mem_createSites {n : ℕ} {G s : PauliString n} {i : Fin n} : i ∈ G.createSites s ↔ G.site i ≠ 0 ∧ s.site i = 0

@[simp]

theorem Lean4LPD.PauliString.mem_antiSites {n : ℕ} {G s : PauliString n} {i : Fin n} : i ∈ G.antiSites s ↔ G.site i ≠ 0 ∧ s.site i ≠ 0 ∧ G.site i ≠ s.site i

The partition of supp G

theorem Lean4LPD.PauliString.support_eq_union {n : ℕ} (G s : PauliString n) : G.support = G.cancelSites s ∪ G.antiSites s ∪ G.createSites s

The three kinds of site exhaust supp G.

theorem Lean4LPD.PauliString.card_cancelSites_add_card_antiSites_add_card_createSites {n : ℕ} (G s : PauliString n) : (G.cancelSites s).card + (G.antiSites s).card + (G.createSites s).card = G.weight

The site count of G. Every site G acts on either cancels a site of s, survives as a locally anticommuting site, or is new.

theorem Lean4LPD.PauliString.weight_mul_add_card_cancelSites {n : ℕ} (G s : PauliString n) : (G * s).weight + (G.cancelSites s).card = s.weight + (G.createSites s).card

The weight bookkeeping. Cancelled sites are exactly what s loses and created sites exactly what it gains, so the weight moves by #create - #cancel.

The symplectic form counts locally anticommuting sites

theorem Lean4LPD.PauliString.sympForm_eq_card_antiSites {n : ℕ} (G s : PauliString n) : G.sympForm s = ↑(G.antiSites s).card

⟪G,s⟫ is #antiSites modulo two. This is what turns a parity statement into a counting statement, and it is the whole source of the -1 in |G s| ≥ |s| - (k_h - 1).

theorem Lean4LPD.PauliString.one_le_card_antiSites {n : ℕ} {G s : PauliString n} (h : G.sympForm s = 1) : 1 ≤ (G.antiSites s).card

Anticommuting Pauli strings share at least one site at which they locally anticommute.

theorem Lean4LPD.PauliString.one_le_weight_of_sympForm_eq_one {n : ℕ} {G s : PauliString n} (h : G.sympForm s = 1) : 1 ≤ G.weight

A Pauli string that anticommutes with something is not a phase: it acts on at least one qubit.

The general bound, and why the sharp one needs anticommutation

theorem Lean4LPD.PauliString.weight_mul_le {n : ℕ} (G s : PauliString n) : (G * s).weight ≤ s.weight + G.weight

Without any hypothesis only |G| is available: the weight can move by up to the full weight of G in either direction.

theorem Lean4LPD.PauliString.weight_le_weight_mul_add_weight {n : ℕ} (G s : PauliString n) : s.weight ≤ (G * s).weight + G.weight

The companion lower bound, again with no hypothesis.

theorem Lean4LPD.PauliString.exists_commuting_weight_increase_by_full_weight : ∃ (G : PauliString 3) (s : PauliString 3), G.sympForm s = 0 ∧ G.weight = 2 ∧ s.weight = 1 ∧ (G * s).weight = 3

The anticommutation hypothesis cannot be dropped. For the commuting pair G = X₁X₂, s = Z₃ on three qubits, the supports are disjoint, so |G s| = 3 = |s| + |G| and the sharp bound |G s| ≤ |s| + (|G| - 1) = 2 fails.

This is why weight_mul_le_weight_add carries sympForm G s = 1 and why the general statement weight_mul_le is the best available without it. It is also why "a k_h-local rotation increases the weight by at most k_h - 1" is a statement about anticommuting rotations. A commuting rotation leaves the Pauli operator unchanged (pauli_rotation_branch_commute in Pauli/Branch.lean), so the bare product G s never arises in that branch and its weight is irrelevant there.

The weight bound

theorem Lean4LPD.PauliString.card_cancelSites_le {n : ℕ} {G s : PauliString n} (h : G.sympForm s = 1) : (G.cancelSites s).card ≤ G.weight - 1

At most |G| - 1 sites of s can be cancelled by an anticommuting G.

theorem Lean4LPD.PauliString.card_createSites_le {n : ℕ} {G s : PauliString n} (h : G.sympForm s = 1) : (G.createSites s).card ≤ G.weight - 1

At most |G| - 1 new sites can be created by an anticommuting G.

theorem Lean4LPD.PauliString.weight_le_weight_mul_add {n : ℕ} {G s : PauliString n} (h : G.sympForm s = 1) : s.weight ≤ (G * s).weight + (G.weight - 1)

The lower half, |G s| ≥ |s| - (|G| - 1) in the form that avoids truncated subtraction. This is the direction the proof of apd:thm:local_flow_k_local uses.

theorem Lean4LPD.PauliString.weight_mul_le_weight_add {n : ℕ} {G s : PauliString n} (h : G.sympForm s = 1) : (G * s).weight ≤ s.weight + (G.weight - 1)

The upper half, |G s| ≤ |s| + (|G| - 1). This is the direction behind the rung spacing w_m = k_o + (m-1)(k_h-1): applied m - 1 times, it bounds by w_m the weight reachable from weight k_o by anticommuting k_h-local rotations. That w_m is attained is not formalized.

theorem Lean4LPD.PauliString.abs_weight_mul_sub_weight_le {n : ℕ} {G s : PauliString n} (h : G.sympForm s = 1) : |↑(G * s).weight - ↑s.weight| ≤ ↑G.weight - 1

The two-sided weight bound: an anticommuting generator of weight |G| changes the weight of s by at most |G| - 1. Stated over ℤ so that no truncated subtraction is hiding in it.

The bound is in terms of the actual weight |G|, which is slightly stronger than the paper's statement in terms of a locality parameter k ≥ |G| (the weight changes by at most k - 1, one of the consequences drawn from apd:eq:pauli_rotation_branch). The parameterized forms are the k_h corollaries weight_sub_le_weight_mul and weight_mul_le_weight_add_kh below, which follow from the two halves above.

The k_h form the ladder consumes

theorem Lean4LPD.PauliString.weight_le_weight_mul_add_kh {n : ℕ} {G s : PauliString n} {kh : ℕ} (hk : G.weight ≤ kh) (h : G.sympForm s = 1) : s.weight ≤ (G * s).weight + (kh - 1)

|s| ≤ |G s| + (k_h - 1) for |G| ≤ k_h: the lower bound on the partner's weight used in the proof of apd:thm:local_flow_k_local, in additive form.

theorem Lean4LPD.PauliString.weight_sub_le_weight_mul {n : ℕ} {G s : PauliString n} {kh : ℕ} (hk : G.weight ≤ kh) (h : G.sympForm s = 1) : s.weight - (kh - 1) ≤ (G * s).weight

|G s| ≥ |s| - (k_h - 1) — the same bound in subtractive form, which is where the proof of apd:thm:local_flow_k_local places the partner Pauli one rung down rather than k_h rungs down. The natural-number subtraction is harmless: when |s| < k_h - 1 the left-hand side is 0 and the bound is trivially true, and otherwise it is the additive form rearranged.

theorem Lean4LPD.PauliString.weight_sub_le_weight_phaseMul_one_mul {n : ℕ} {G s : PauliString n} {kh : ℕ} (hk : G.weight ≤ kh) (h : G.sympForm s = 1) : s.weight - (kh - 1) ≤ (phaseMul 1 (G * s)).weight

The same bound for the Hermitian partner i G s. In the proof of apd:thm:local_flow_k_local a high-weight Pauli s is connected to its partner i G s, not to the bare product G s. The two have the same weight, because the weight cannot see a phase (weight_phaseMul), so this is weight_sub_le_weight_mul restated for the object the proof actually uses.

theorem Lean4LPD.PauliString.weight_mul_le_weight_add_kh {n : ℕ} {G s : PauliString n} {kh : ℕ} (hk : G.weight ≤ kh) (h : G.sympForm s = 1) : (G * s).weight ≤ s.weight + (kh - 1)

|G s| ≤ |s| + (k_h - 1) for |G| ≤ k_h — the direction that fixes the rung spacing w_m = k_o + (m-1)(k_h-1) of apd:thm:local_flow_k_local.