How many Paulis LPD stores: O(n^{w*})

The number of Pauli classes on n qubits of weight at most w is at most C(n,w) · 4^w, hence at most 4^w · n^w. This is the counting step of apd:thm:lightcone and apd:thm:runtime: an observable truncated at weight w* contains O(n^{w*}) Pauli operators, and the time O((r+1) · n^{w*}) and memory O(n^{w*}) of apd:thm:runtime are built on that count.

Scope. apd:thm:runtime itself is not formalized in this library; only this count is. The rest of that theorem combines the truncation-error analysis (the entanglement hypothesis of apd:thm:triangle, the short-time condition t < t₀, and the formula for w*, of which this library proves the existence form exists_uniform_weight_cutoff) with a computational cost model: a data structure indexed by supports, with O(1) access to a coefficient. A cost model is not something this library formalizes; it could only enter as a declared assumption. The counting step is the opposite: pure combinatorics, independent of all of those, and it is what makes n^{w*} polynomial rather than exponential in n at fixed w*.

The bound is C(n,w) · 4^w, and it is loose in two stated ways. It double-counts classes of weight < w, which lie in several w-element supersets, and it allows a site inside the chosen support to be the identity, giving 4 where an exact count gives 3. Both are the price of avoiding a fiberwise exact count, and neither affects the O(n^w) conclusion. card_lowSet_le is an explicit inequality where the paper writes O(·), and an upper bound is the direction that matters: an upper bound on the number of stored Paulis is what bounds the runtime.

Main definitions

• lowSet n w: the Pauli classes of weight at most w, the complement of highSet n w. These are the classes a weight-w truncation retains.
• psupp p: the sites at which the class p is not the identity.
• vanishOff S: the classes that are the identity outside the set of sites S.

Main results

• card_vanishOff: exactly 4 ^ S.card classes are the identity outside S.
• card_lowSet_le: (lowSet n w).card ≤ n.choose w * 4 ^ w for w ≤ n.
• card_lowSet_le_pow: (lowSet n w).card ≤ 4 ^ w * n ^ w for w ≤ n.

def Lean4LPD.PauliString.lowSet (n w : ℕ) : Finset (PauliIndex n)

The low-weight region: the Pauli classes of weight at most w, defined as the complement of highSet n w. These are the classes a weight-w truncation retains.

Equations

• Lean4LPD.PauliString.lowSet n w = (Lean4LPD.PauliString.highSet n w)ᶜ

@[simp]

theorem Lean4LPD.PauliString.mem_lowSet {n w : ℕ} {p : PauliIndex n} : p ∈ lowSet n w ↔ wt p ≤ w

def Lean4LPD.PauliString.siteFun {n : ℕ} (p : PauliIndex n) : Fin n → ZMod 2 × ZMod 2

A Pauli class read site by site: the pair of x and z bits at each qubit. The pair is 0 exactly when the class is the identity at that site.

Equations

• Lean4LPD.PauliString.siteFun p i = (p.1 i, p.2 i)

def Lean4LPD.PauliString.siteEquiv {n : ℕ} : PauliIndex n ≃ (Fin n → ZMod 2 × ZMod 2)

siteFun as an equivalence between Pauli classes and functions from sites to bit pairs.

Equations

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

def Lean4LPD.PauliString.psupp {n : ℕ} (p : PauliIndex n) : Finset (Fin n)

The sites at which the class is not the identity. wt counts exactly these.

Equations

• Lean4LPD.PauliString.psupp p = {i : Fin n | Lean4LPD.PauliString.siteFun p i ≠ 0}

theorem Lean4LPD.PauliString.wt_eq_card_psupp {n : ℕ} (p : PauliIndex n) : wt p = (psupp p).card

@[simp]

theorem Lean4LPD.PauliString.mem_psupp {n : ℕ} {p : PauliIndex n} {i : Fin n} : i ∈ psupp p ↔ siteFun p i ≠ 0

def Lean4LPD.PauliString.vanishOff {n : ℕ} (S : Finset (Fin n)) : Finset (PauliIndex n)

Classes whose site function vanishes outside S.

Equations

• Lean4LPD.PauliString.vanishOff S = {p : Lean4LPD.PauliIndex n | ∀ i ∉ S, Lean4LPD.PauliString.siteFun p i = 0}

theorem Lean4LPD.PauliString.card_vanishOff {n : ℕ} (S : Finset (Fin n)) : (vanishOff S).card = 4 ^ S.card

Exactly 4 ^ S.card classes are the identity outside S: each site of S carries one of the four bit pairs, and every other site carries 0.

theorem Lean4LPD.PauliString.card_lowSet_le (n w : ℕ) (hw : w ≤ n) : (lowSet n w).card ≤ n.choose w * 4 ^ w

The stored set is polynomial in n for fixed w.

apd:thm:runtime uses that an observable truncated at weight w* contains O(n^{w*}) Pauli operators. This is that count, with the constant explicit rather than inside an O(·).

Every class of weight ≤ w has its support inside some w-element set, and the classes supported in a fixed S number exactly 4^{|S|} (card_vanishOff) — so the union over all C(n,w) choices of S bounds the whole stored set. The bound is not tight: it double-counts classes of weight < w, which lie in several S. 4 rather than 3 for the same reason — a site inside S is allowed to be the identity. Both are the price of avoiding a fiberwise exact count, and neither affects the O(n^w) conclusion this is here to supply.

theorem Lean4LPD.PauliString.card_lowSet_le_pow (n w : ℕ) (hw : w ≤ n) : (lowSet n w).card ≤ 4 ^ w * n ^ w

The same bound as a polynomial in n: C(n,w) ≤ n^w. This is the form apd:thm:runtime's O(n^{w*}) names.

Sanity checks: the bound holds and is not vacuous