The LPD truncation error of a layered Trotter circuit, in Pauli norm

This file assembles the norm-level truncation-error bound for a Trotter step made of Γ disjoint-support layers of Pauli rotations, with truncation to Pauli weight at most w* at the end of every step. The main result is pauliNorm_layerStep_error_le_model_of_source_regime: for a k_o-local observable O and r Trotter steps in the paper's parameter regime,

‖U^r(O) - O_r‖ ≤ (t / t₀)^(m+1) · (e (m+1))^(k_o / (k_h - 1)) · ‖O‖,

where ‖·‖ is the normalized Pauli 2-norm pauliNorm, U is the untruncated step (layerBlockEnd), O_r is the LPD output (layerStepTraj), the cutoff is w* = rungWeight ko kh (m + 1) = k_o + m (k_h - 1), and t₀ = 1 / (2 Γ (k_h - 1) α) is tZeroModel Γ k_h α. This is the Pauli-norm counterpart of apd:thm:one_step_truncation_error with the time condition apd:eq:time_condition.

Main definitions

• layerBlockTraj: the untruncated evolution through the first i layers of a block.
• layerStepTraj: the LPD recurrence: a whole block of Γ layers, then the weight cut.
• layerScheduledTraj: the same execution indexed by layers, as a layerTraj with the schedule trotterSchedule Γ wstar. Here the schedule counts layers, not individual rotations.
• discardedLayerStep: the discarded operator X_{d+1} of apd:eq:step_component.
• layerStepMass: the high-weight norm inside a step, before the cut.
• layerBlockEnd: one block as an additive endomorphism; its powers are the untruncated evolution.

Main results

• layerScheduledTraj_at_boundary: the layer-indexed and the step-indexed executions agree at step boundaries.
• pauliNorm_discardedLayerStep: ‖X_{d+1}‖ is the high-weight norm of the operator before the cut.
• layerStepMass_reset, layerStepMass_inflow: the two hypotheses of MultiLadder.sum_block_inflow_le, proved for the Pauli model.
• sum_pauliNorm_discardedLayerStep_le_chain: the shifted-chain bound on ∑_d ‖Õ^{(d)}_{≥w*+1}‖ of apd:eq:total_high_weight_norm.
• layerStep_telescoping, pauliNorm_layerStep_error_le: the telescoping identity and the norm-level triangle bound of apd:thm:triangle, for layered steps.
• sum_pauliNorm_discardedLayerStep_le_cZero, pauliNorm_layerStep_error_le_cZero: the bound with the constant c₀ of apd:eq:c0.
• source_entry_inflation_le_one, source_beta_le_half: the paper's step-count condition gives 4eβ ≤ 1 and β ≤ 1/2.
• pauliNorm_layerStep_error_le_model, pauliNorm_layerStep_error_le_model_of_source_regime: the final bound with the threshold tZeroModel.

Implementation notes

The discarded operator Õ^{(d)}_{≥w*+1} lives at a step boundary, and its norm is the high-weight norm of the operator before the cut. The kept trajectory, whose rung masses pauliMultiLadder controls, has no mass above the cutoff right after a boundary. The bridge is layerStepMass: within a step it starts from zero (layerStepMass_reset) and grows by the multi-jump inflow from the lower rungs of the kept trajectory (layerStepMass_inflow). With these two facts, MultiLadder.sum_block_inflow_le bounds ∑_d ‖Õ^{(d)}_{≥w*+1}‖ by the shifted-chain sum of apd:eq:total_high_weight_norm, and MultiLadder.sum_block_epsJump_le_cZero by the c₀ form.

layerStepTraj and layerScheduledTraj are defined independently, and their agreement at step boundaries is a theorem. Every hypothesis of the final theorems concerns the circuit (layer structure, Hermiticity, sine bound), the observable (locality) or the parameters (Admissible, 1 ≤ m, 5 ≤ r, the step-count condition); no recurrence, reset or intermediate bound is assumed.

All bounds are in the normalized Pauli 2-norm. Expectation values in a state, and the comparison of the Trotter circuit with the Hamiltonian evolution, are not treated here.

theorem Lean4LPD.source_entry_inflation_le_one {kh1 c a A r : ℝ} (hkh : 0 < kh1) (hc : 0 ≤ c) (hr : 0 < r) (haA : a ≤ A / r) (hsteps : 8 * Real.exp 1 ^ 2 * rungW kh1 c 2 * A ≤ r) : 4 * Real.exp 1 * betaOf kh1 c a ≤ 1

In the paper's parameter regime, the step-count condition r ≥ 8e² w₂ A together with a ≤ A / r gives B = 4eβ ≤ 1, where β = 2e w₂ a (apd:eq:multijump_factor; apd:eq:c0; apd:thm:one_step_truncation_error). This is the hypothesis B ≤ 1 of cZero_le_two. The proof multiplies through by r; no division by a occurs.

theorem Lean4LPD.source_beta_le_half {kh1 c a A r : ℝ} (hkh : 0 < kh1) (hc : 0 ≤ c) (ha : 0 ≤ a) (hr : 0 < r) (haA : a ≤ A / r) (hsteps : 8 * Real.exp 1 ^ 2 * rungW kh1 c 2 * A ≤ r) : betaOf kh1 c a ≤ 1 / 2

In the paper's parameter regime, the same step-count condition gives β ≤ 1/2, the regime of the entry-factor bound entryFactor_le (apd:eq:multijump_factor; apd:eq:entry_bound).

noncomputable def Lean4LPD.PauliString.layerBlockTraj {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (O : Matrix (Bits n) (Bits n) ℂ) : ℕ → Matrix (Bits n) (Bits n) ℂ

The untruncated evolution through the first i layers of a fixed block, as used to define Õ^{(d)}_{≥w*+1} in apd:eq:step_component.

Equations

• Lean4LPD.PauliString.layerBlockTraj layers O 0 = O
• Lean4LPD.PauliString.layerBlockTraj layers O i.succ = Lean4LPD.PauliString.layerConj (layers i) (Lean4LPD.PauliString.layerBlockTraj layers O i)

@[simp]

theorem Lean4LPD.PauliString.layerBlockTraj_zero {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (O : Matrix (Bits n) (Bits n) ℂ) : layerBlockTraj layers O 0 = O

The fixed block begins at the supplied operator (apd:eq:step_component).

theorem Lean4LPD.PauliString.layerBlockTraj_succ {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (O : Matrix (Bits n) (Bits n) ℂ) (i : ℕ) : layerBlockTraj layers O (i + 1) = layerConj (layers i) (layerBlockTraj layers O i)

One more untruncated layer of the fixed block (apd:eq:step_component).

noncomputable def Lean4LPD.PauliString.layerStepTraj {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (Γ wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) : ℕ → Matrix (Bits n) (Bits n) ℂ

The LPD recurrence: evolve through a whole block of Γ layers, then keep Pauli weights at most wstar. This is the recurrence of the kept operator in apd:eq:step_component. It is defined directly, not as a subsequence of layerScheduledTraj.

Equations

• One or more equations did not get rendered due to their size.
• Lean4LPD.PauliString.layerStepTraj layers Γ wstar O 0 = O

@[simp]

theorem Lean4LPD.PauliString.layerStepTraj_zero {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (Γ wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) : layerStepTraj layers Γ wstar O 0 = O

The recurrence starts at the input observable; no cut is applied at step 0 (apd:eq:step_component).

theorem Lean4LPD.PauliString.layerStepTraj_succ {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (Γ wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (d : ℕ) : layerStepTraj layers Γ wstar O (d + 1) = truncOp (highSet n wstar)ᶜ (layerBlockTraj layers (layerStepTraj layers Γ wstar O d) Γ)

One complete step: evolve through the block, then cut (apd:eq:step_component).

noncomputable def Lean4LPD.PauliString.layerScheduledTraj {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (Γ wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) : ℕ → Matrix (Bits n) (Bits n) ℂ

Execute the repeated fixed block with a cut after each multiple of Γ layers. This uses the boundary convention of apd:thm:triangle.

Equations

• Lean4LPD.PauliString.layerScheduledTraj layers Γ wstar O = Lean4LPD.PauliString.layerTraj (fun (T : ℕ) => layers (T % Γ)) (Lean4LPD.PauliString.trotterSchedule Γ wstar) O

@[simp]

theorem Lean4LPD.PauliString.layerScheduledTraj_zero {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (Γ wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) : layerScheduledTraj layers Γ wstar O 0 = O

The scheduled execution starts at the input observable (apd:eq:step_component).

theorem Lean4LPD.PauliString.layerScheduledTraj_succ {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (Γ wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (T : ℕ) : layerScheduledTraj layers Γ wstar O (T + 1) = truncOp (trotterSchedule Γ wstar T) (layerConj (layers (T % Γ)) (layerScheduledTraj layers Γ wstar O T))

A single scheduled layer: conjugation by the layer, then the scheduled projection (apd:thm:triangle).

theorem Lean4LPD.PauliString.layerScheduledTraj_within_step {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (Γ wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (d i : ℕ) (hi : i < Γ) : layerScheduledTraj layers Γ wstar O (d * Γ + i) = layerBlockTraj layers (layerScheduledTraj layers Γ wstar O (d * Γ)) i

Before a boundary, the scheduled execution is the untruncated prefix of the fixed block, started from the scheduled operator at the previous boundary (apd:eq:step_component).

theorem Lean4LPD.PauliString.layerScheduledTraj_next_boundary {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (Γ wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (d : ℕ) (hΓ : 0 < Γ) : layerScheduledTraj layers Γ wstar O ((d + 1) * Γ) = truncOp (highSet n wstar)ᶜ (layerBlockTraj layers (layerScheduledTraj layers Γ wstar O (d * Γ)) Γ)

Over one full block, the scheduled execution evolves without truncation and is then cut (apd:eq:step_component).

theorem Lean4LPD.PauliString.layerScheduledTraj_at_boundary {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (Γ wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (d : ℕ) (hΓ : 0 < Γ) : layerScheduledTraj layers Γ wstar O (d * Γ) = layerStepTraj layers Γ wstar O d

The layer-indexed and the step-indexed executions agree at step boundaries (apd:eq:step_component). Both sides are defined independently, so this is a theorem.

theorem Lean4LPD.PauliString.layerBlockTraj_eq_scheduled_prefix {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (Γ wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (d i : ℕ) (hi : i < Γ) : layerBlockTraj layers (layerStepTraj layers Γ wstar O d) i = layerScheduledTraj layers Γ wstar O (d * Γ + i)

Inside a step, the untruncated prefix of the block equals the scheduled trajectory at the corresponding layer. This identification lets the rung masses of pauliMultiLadder be used in apd:eq:total_high_weight_norm. The endpoint i = Γ is excluded: there the scheduled trajectory has already been cut.

noncomputable def Lean4LPD.PauliString.discardedLayerStep {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (Γ wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (d : ℕ) : Matrix (Bits n) (Bits n) ℂ

The discarded operator X_{d+1} of apd:eq:step_component: the operator at the end of step d + 1 before the cut, minus the kept operator. The index d is zero-based.

Equations

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

theorem Lean4LPD.PauliString.pauliNorm_discardedLayerStep {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (Γ wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (d : ℕ) : pauliNorm (discardedLayerStep layers Γ wstar O d) = highNorm wstar (layerBlockTraj layers (layerStepTraj layers Γ wstar O d) Γ)

The Pauli norm of the discarded operator is the high-weight norm of the operator before the cut (apd:thm:triangle; apd:eq:step_component).

theorem Lean4LPD.PauliString.highNorm_layerStepTraj_succ {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (Γ wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (d : ℕ) : highNorm wstar (layerStepTraj layers Γ wstar O (d + 1)) = 0

After every completed step the kept operator has no mass above the cutoff. This gives the reset condition in apd:eq:total_high_weight_norm. It is a statement about the kept operator, not about the discarded one.

noncomputable def Lean4LPD.PauliString.layerStepMass {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (Γ wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (d i : ℕ) : ℝ

The high-weight norm inside step d + 1, after i untruncated layers and before the cut, as used in apd:eq:total_high_weight_norm. It is defined from the matrix evolution; its recurrence is layerStepMass_inflow.

Equations

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

theorem Lean4LPD.PauliString.layerStepMass_reset {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) {Γ wstar ko : ℕ} {O : Matrix (Bits n) (Bits n) ℂ} (hcut : ko ≤ wstar) (hloc : ∀ (p : PauliIndex n), ko < wt p → coeff O p = 0) (d : ℕ) : layerStepMass layers Γ wstar O d 0 = 0

Reset at the start of every step, as required by apd:eq:total_high_weight_norm: the mass above the cutoff vanishes at layer 0 of each step. For the first step this follows from k_o-locality of the input and k_o ≤ wstar; for later steps from the preceding cut.

theorem Lean4LPD.PauliString.layerStepMass_inflow {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (Γ : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) {ko kh m : ℕ} (hkh : 2 ≤ kh) (hL : ∀ (T : ℕ), IsLayer kh (List.map Prod.fst (layers T))) (hherm : ∀ (T : ℕ), ∀ g ∈ layers T, IsSelfAdjoint g.1) {a : ℝ} (ha : 0 ≤ a) (hsin : ∀ (T : ℕ), ∀ g ∈ layers T, |Real.sin g.2| ≤ a) (hm : 1 ≤ m) (hb : betaOf (↑(kh - 1)) (↑ko / ↑(kh - 1)) a < 1) (d i : ℕ) (hi : i < Γ) : layerStepMass layers Γ (rungWeight ko kh m) O d (i + 1) ≤ layerStepMass layers Γ (rungWeight ko kh m) O d i + ∑ j ∈ Finset.Ico 1 m, epsJump (↑(kh - 1)) (↑ko / ↑(kh - 1)) a j m * layerN (fun (T : ℕ) => layers (T % Γ)) (trotterSchedule Γ (rungWeight ko kh m)) O ko kh (m - j) (d * Γ + i) + entryFactor (↑(kh - 1)) (↑ko / ↑(kh - 1)) a m * pauliNorm O

Inflow inside a step. One more layer increases the mass above the cutoff by at most the multi-jump inflow from the lower rungs of the kept trajectory layerN, plus the entry factor times the Pauli norm of the input. This is the inflow hypothesis of MultiLadder.sum_block_inflow_le for apd:eq:total_high_weight_norm, derived here from highNorm_layerConj_le_multi.

theorem Lean4LPD.PauliString.sum_pauliNorm_discardedLayerStep_le_chain {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (Γ : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) {ko kh m : ℕ} (hΓ : 0 < Γ) (hkh : 2 ≤ kh) (hL : ∀ (T : ℕ), IsLayer kh (List.map Prod.fst (layers T))) (hherm : ∀ (T : ℕ), ∀ g ∈ layers T, IsSelfAdjoint g.1) {a : ℝ} (ha : 0 ≤ a) (hsin : ∀ (T : ℕ), ∀ g ∈ layers T, |Real.sin g.2| ≤ a) (hm : 1 ≤ m) (hb : betaOf (↑(kh - 1)) (↑ko / ↑(kh - 1)) a < 1) (hloc : ∀ (p : PauliIndex n), ko < wt p → coeff O p = 0) (r : ℕ) : ∑ d ∈ Finset.range r, pauliNorm (discardedLayerStep layers Γ (rungWeight ko kh m) O d) ≤ pauliNorm O * ∑ k ∈ Finset.range m, ((↑r + 1) * ↑Γ) ^ (k + 1) / ↑(k + 1).factorial * chain (epsJump (↑(kh - 1)) (↑ko / ↑(kh - 1)) a) (entryFactor (↑(kh - 1)) (↑ko / ↑(kh - 1)) a) (k + 1) m

The sum of the discarded Pauli norms obeys the shifted-chain bound. This is the step of apd:eq:total_high_weight_norm that sums the per-step inflows over the layer slots, with X_{d+1} defined by apd:eq:step_component: a chain with k + 1 jumps carries the factor ((r + 1) Γ)^(k+1) / (k+1)!. The reset and the inflow recurrence required by MultiLadder.sum_block_inflow_le are supplied by layerStepMass_reset and layerStepMass_inflow, so they are not hypotheses.

theorem Lean4LPD.PauliString.layerConj_add {n : ℕ} (L : List (PauliString n × ℝ)) (A B : Matrix (Bits n) (Bits n) ℂ) : layerConj L (A + B) = layerConj L A + layerConj L B

Layer conjugation is additive, supporting the operator telescope of apd:thm:triangle.

@[simp]

theorem Lean4LPD.PauliString.layerConj_zero {n : ℕ} (L : List (PauliString n × ℝ)) : layerConj L 0 = 0

Layer conjugation preserves zero, the additive-map helper for apd:thm:triangle.

theorem Lean4LPD.PauliString.layerBlockTraj_add {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (A B : Matrix (Bits n) (Bits n) ℂ) (i : ℕ) : layerBlockTraj layers (A + B) i = layerBlockTraj layers A i + layerBlockTraj layers B i

The evolution through a block of layers is additive, as required by apd:thm:triangle.

@[simp]

theorem Lean4LPD.PauliString.layerBlockTraj_zero_input {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (i : ℕ) : layerBlockTraj layers 0 i = 0

A zero input stays zero through a block of layers (apd:thm:triangle).

noncomputable def Lean4LPD.PauliString.layerBlockEnd {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (Γ : ℕ) : AddMonoid.End (Matrix (Bits n) (Bits n) ℂ)

The untruncated evolution through a fixed block of Γ layers, as an additive endomorphism of matrices. Its powers are the untruncated whole-step evolutions in apd:thm:triangle.

Equations

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

@[simp]

theorem Lean4LPD.PauliString.layerBlockEnd_apply {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (Γ : ℕ) (A : Matrix (Bits n) (Bits n) ℂ) : (layerBlockEnd layers Γ) A = layerBlockTraj layers A Γ

layerBlockEnd applies the matrix evolution layerBlockTraj through Γ layers (apd:thm:triangle).

theorem Lean4LPD.PauliString.layerStep_telescoping {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (Γ wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (r : ℕ) : (layerBlockEnd layers Γ ^ r) O - layerStepTraj layers Γ wstar O r = ∑ d ∈ Finset.range r, (layerBlockEnd layers Γ ^ (r - 1 - d)) (discardedLayerStep layers Γ wstar O d)

The operator telescope for layered steps. This is the identity in apd:thm:triangle: the untruncated evolution minus the LPD output after r steps is the sum of the discarded operators discardedLayerStep, each evolved through the remaining whole blocks.

theorem Lean4LPD.PauliString.pauliNorm_layerBlockTraj {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (hherm : ∀ (T : ℕ), ∀ g ∈ layers T, IsSelfAdjoint g.1) (O : Matrix (Bits n) (Bits n) ℂ) (i : ℕ) : pauliNorm (layerBlockTraj layers O i) = pauliNorm O

A whole Hermitian layer block preserves the normalized Pauli norm, supporting the norm-level triangle counterpart of apd:thm:triangle.

theorem Lean4LPD.PauliString.pauliNorm_layerBlockEnd_pow {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (hherm : ∀ (T : ℕ), ∀ g ∈ layers T, IsSelfAdjoint g.1) (Γ : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (r : ℕ) : pauliNorm ((layerBlockEnd layers Γ ^ r) O) = pauliNorm O

Every power of the block evolution preserves the normalized Pauli norm, for Hermitian generators (apd:thm:triangle).

theorem Lean4LPD.PauliString.pauliNorm_layerStep_error_le {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (hherm : ∀ (T : ℕ), ∀ g ∈ layers T, IsSelfAdjoint g.1) (Γ wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (r : ℕ) : pauliNorm ((layerBlockEnd layers Γ ^ r) O - layerStepTraj layers Γ wstar O r) ≤ ∑ d ∈ Finset.range r, pauliNorm (discardedLayerStep layers Γ wstar O d)

The truncation error is at most the sum of the discarded Pauli norms. This is the norm-level part of apd:thm:triangle, in the normalized Pauli 2-norm. It is neither a bound on expectation values nor a bound in the matrix operator norm.

theorem Lean4LPD.PauliString.pauliNorm_layerStep_error_le_chain {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (Γ : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) {ko kh m : ℕ} (hΓ : 0 < Γ) (hkh : 2 ≤ kh) (hL : ∀ (T : ℕ), IsLayer kh (List.map Prod.fst (layers T))) (hherm : ∀ (T : ℕ), ∀ g ∈ layers T, IsSelfAdjoint g.1) {a : ℝ} (ha : 0 ≤ a) (hsin : ∀ (T : ℕ), ∀ g ∈ layers T, |Real.sin g.2| ≤ a) (hm : 1 ≤ m) (hb : betaOf (↑(kh - 1)) (↑ko / ↑(kh - 1)) a < 1) (hloc : ∀ (p : PauliIndex n), ko < wt p → coeff O p = 0) (r : ℕ) : pauliNorm ((layerBlockEnd layers Γ ^ r) O - layerStepTraj layers Γ (rungWeight ko kh m) O r) ≤ pauliNorm O * ∑ k ∈ Finset.range m, ((↑r + 1) * ↑Γ) ^ (k + 1) / ↑(k + 1).factorial * chain (epsJump (↑(kh - 1)) (↑ko / ↑(kh - 1)) a) (entryFactor (↑(kh - 1)) (↑ko / ↑(kh - 1)) a) (k + 1) m

The truncation error obeys the shifted-chain bound. This composes the norm-level triangle bound of apd:thm:triangle with the shifted-chain bound sum_pauliNorm_discardedLayerStep_le_chain of apd:eq:total_high_weight_norm. Besides 0 < Γ and 1 ≤ m, the hypotheses concern only the generators (layer structure, Hermiticity, sine bound, betaOf < 1) and the locality of the observable.

theorem Lean4LPD.PauliString.sum_pauliNorm_discardedLayerStep_le_cZero {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (Γ : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) {ko kh m r : ℕ} (hΓ : 0 < Γ) (hkh : 2 ≤ kh) (hL : ∀ (T : ℕ), IsLayer kh (List.map Prod.fst (layers T))) (hherm : ∀ (T : ℕ), ∀ g ∈ layers T, IsSelfAdjoint g.1) {a A : ℝ} (ha : 0 ≤ a) (hsin : ∀ (T : ℕ), ∀ g ∈ layers T, |Real.sin g.2| ≤ a) (hb : betaOf (↑(kh - 1)) (↑ko / ↑(kh - 1)) a ≤ 1 / 2) (hA : 0 ≤ A) (hr : 1 ≤ r) (haA : a ≤ A / ↑r) (hloc : ∀ (p : PauliIndex n), ko < wt p → coeff O p = 0) : ∑ d ∈ Finset.range r, pauliNorm (discardedLayerStep layers Γ (rungWeight ko kh (m + 1)) O d) ≤ ((cZero (↑r) (↑m) (↑Γ) (4 * Real.exp 1 * betaOf (↑(kh - 1)) (↑ko / ↑(kh - 1)) a) * ↑Γ * A) ^ (m + 1) * ∏ j ∈ Finset.range (m + 1), rungW (↑(kh - 1)) (↑ko / ↑(kh - 1)) (j + 2)) / ↑(m + 1).factorial * pauliNorm O

The sum of the discarded Pauli norms obeys the c₀ bound. MultiLadder.sum_block_epsJump_le_cZero (apd:eq:total_high_weight_norm; apd:eq:c0) applied to pauliMultiLadder, with reset and inflow supplied by layerStepMass_reset and layerStepMass_inflow. The conclusion has the form of the hypothesis hstep of total_truncation_error, which is therefore a theorem for the Pauli model. Here A stands for the product α t, the cutoff is rung m + 1, and B = 4eβ.

theorem Lean4LPD.PauliString.pauliNorm_layerStep_error_le_cZero {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (Γ : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) {ko kh m r : ℕ} (hΓ : 0 < Γ) (hkh : 2 ≤ kh) (hL : ∀ (T : ℕ), IsLayer kh (List.map Prod.fst (layers T))) (hherm : ∀ (T : ℕ), ∀ g ∈ layers T, IsSelfAdjoint g.1) {a A : ℝ} (ha : 0 ≤ a) (hsin : ∀ (T : ℕ), ∀ g ∈ layers T, |Real.sin g.2| ≤ a) (hb : betaOf (↑(kh - 1)) (↑ko / ↑(kh - 1)) a ≤ 1 / 2) (hA : 0 ≤ A) (hr : 1 ≤ r) (haA : a ≤ A / ↑r) (hloc : ∀ (p : PauliIndex n), ko < wt p → coeff O p = 0) : pauliNorm ((layerBlockEnd layers Γ ^ r) O - layerStepTraj layers Γ (rungWeight ko kh (m + 1)) O r) ≤ ((cZero (↑r) (↑m) (↑Γ) (4 * Real.exp 1 * betaOf (↑(kh - 1)) (↑ko / ↑(kh - 1)) a) * ↑Γ * A) ^ (m + 1) * ∏ j ∈ Finset.range (m + 1), rungW (↑(kh - 1)) (↑ko / ↑(kh - 1)) (j + 2)) / ↑(m + 1).factorial * pauliNorm O

The truncation error obeys the c₀ bound (apd:thm:triangle; apd:eq:total_high_weight_norm; apd:eq:c0). This is a statement in the normalized Pauli norm, not about expectation values.

theorem Lean4LPD.PauliString.pauliNorm_layerStep_error_le_model {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (Γ : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) {ko kh m r : ℕ} (hΓ : 0 < Γ) (hkh : 2 ≤ kh) (hL : ∀ (T : ℕ), IsLayer kh (List.map Prod.fst (layers T))) (hherm : ∀ (T : ℕ), ∀ g ∈ layers T, IsSelfAdjoint g.1) {a α t : ℝ} (ha : 0 ≤ a) (hsin : ∀ (T : ℕ), ∀ g ∈ layers T, |Real.sin g.2| ≤ a) (hα : 0 < α) (ht : 0 ≤ t) (haA : a ≤ α * t / ↑r) (hB : 4 * Real.exp 1 * betaOf (↑(kh - 1)) (↑ko / ↑(kh - 1)) a ≤ 1) (hadm : Admissible ↑r ↑m ↑Γ) (hm : 1 ≤ m) (hr : 5 ≤ r) (hloc : ∀ (p : PauliIndex n), ko < wt p → coeff O p = 0) : pauliNorm ((layerBlockEnd layers Γ ^ r) O - layerStepTraj layers Γ (rungWeight ko kh (m + 1)) O r) ≤ decayBase (↑Γ) (↑kh) α t ^ (m + 1) * (Real.exp 1 * (↑m + 1)) ^ (↑ko / ↑(kh - 1)) * pauliNorm O

The truncation error with the threshold tZeroModel. This is the Pauli-norm counterpart of apd:thm:one_step_truncation_error and apd:eq:time_condition: the error is at most q^(m+1) (e (m+1))^(k_o/(k_h-1)) ‖O‖ with q = decayBase Γ k_h α t = t / tZeroModel Γ k_h α, a threshold that depends only on Γ, k_h and α. The hypotheses 1 ≤ m and 5 ≤ r, under which c₀ ≤ 2 (cZero_le_two), are explicit, as is B = 4eβ ≤ 1, which also implies β ≤ 1/2. Since c₀ ≤ 2 under these hypotheses, tZeroModel is at most the threshold tZero with the constant c₀ (tZeroModel_le_tZero), so t < tZeroModel is the more restrictive time condition. The hypothesis hstep of the scalar theorem total_truncation_error_product_bound is supplied by pauliNorm_layerStep_error_le_cZero.

theorem Lean4LPD.PauliString.pauliNorm_layerStep_error_le_model_of_source_regime {n : ℕ} (layers : ℕ → List (PauliString n × ℝ)) (Γ : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) {ko kh m r : ℕ} (hΓ : 0 < Γ) (hkh : 2 ≤ kh) (hL : ∀ (T : ℕ), IsLayer kh (List.map Prod.fst (layers T))) (hherm : ∀ (T : ℕ), ∀ g ∈ layers T, IsSelfAdjoint g.1) {a α t : ℝ} (ha : 0 ≤ a) (hsin : ∀ (T : ℕ), ∀ g ∈ layers T, |Real.sin g.2| ≤ a) (hα : 0 < α) (ht : 0 ≤ t) (haA : a ≤ α * t / ↑r) (hsteps : 8 * Real.exp 1 ^ 2 * (↑ko + ↑kh - 1) * α * t ≤ ↑r) (hadm : Admissible ↑r ↑m ↑Γ) (hm : 1 ≤ m) (hr : 5 ≤ r) (hloc : ∀ (p : PauliIndex n), ko < wt p → coeff O p = 0) : pauliNorm ((layerBlockEnd layers Γ ^ r) O - layerStepTraj layers Γ (rungWeight ko kh (m + 1)) O r) ≤ decayBase (↑Γ) (↑kh) α t ^ (m + 1) * (Real.exp 1 * (↑m + 1)) ^ (↑ko / ↑(kh - 1)) * pauliNorm O

The norm-level truncation bound in the paper's parameter regime. This is apd:thm:one_step_truncation_error with apd:eq:time_condition at the level of the normalized Pauli norm. Let O be k_o-local, let each step consist of Γ disjoint-support layers of Hermitian rotations of weight at most k_h, 2 ≤ k_h, with |sin θ| ≤ a ≤ α t / r, and let the cutoff be w* = k_o + m (k_h - 1). If Admissible r m Γ (in particular m ≤ r and 8 (m + 1)² ≤ r Γ), 1 ≤ m, 5 ≤ r and r ≥ 8e² (k_o + k_h - 1) α t, then

‖U^r(O) - O_r‖ ≤ (t / t₀)^(m+1) · (e (m+1))^(k_o/(k_h-1)) · ‖O‖, t₀ = tZeroModel Γ k_h α.

The step-count condition gives B = 4eβ ≤ 1 (source_entry_inflation_le_one) and hence β ≤ 1/2, so neither is a separate hypothesis. The base t / t₀ is below one whenever t < tZeroModel Γ k_h α, by decayBase_lt_one. Nothing is asserted about expectation values in a state or about the Trotter approximation of the Hamiltonian evolution.