Pauli propagation: truncation error

Pauli propagation evolves an observable in the Heisenberg picture as a sum over Pauli paths and, to stay efficient, truncates low-coefficient / high-weight terms. Rudolph et al. (2025) bound the total simulation error by the sum of the per-layer discarded ℓ¹-norms (a triangle-inequality bound). This module records that bound abstractly (the discarded norms are the hypotheses) and derives that exact propagation (no truncation) incurs no error, and that the error bound is nonnegative.

Source: Rudolph, Jones, Teng, Angrisani, Holmes (2025), Pauli Propagation (arXiv:2505.21606), Theory Box 3.

structure QuantumAlg.PauliPropagationTruncation : Type

Per-layer truncation data for a Pauli-propagation simulation: the discarded ℓ¹-norm at each layer and the total error, bounded by their sum (Rudolph et al. 2025).

• layers : ℕ

  Number of circuit layers.

• discarded : ℕ → ℝ

  ℓ¹-norm of the Pauli terms discarded at each layer.

• discarded_nonneg (i : ℕ) : 0 ≤ self.discarded i

  Discarded norms are nonnegative.

• totalError : ℝ

  Total simulation error.

• error_le : self.totalError ≤ ∑ i ∈ Finset.range self.layers, self.discarded i

  Triangle-inequality bound: the error is at most the sum of discarded norms.

theorem QuantumAlg.PauliPropagationTruncation.sum_discarded_nonneg (M : PauliPropagationTruncation) : 0 ≤ ∑ i ∈ Finset.range M.layers, M.discarded i

The error bound (sum of discarded norms) is nonnegative.

theorem QuantumAlg.PauliPropagationTruncation.exact (M : PauliPropagationTruncation) (h : ∀ (i : ℕ), M.discarded i = 0) : M.totalError ≤ 0

Exact propagation: if nothing is discarded, the simulation error is ≤ 0.