A repeated Trotter block with truncation at step boundaries

In LPD the Heisenberg-evolved observable is truncated at the end of each Trotter step, not after every rotation (apd:thm:triangle). Here a step is a fixed block of period rotations: the first period entries of Gs and θ specify the block, and the rotation-indexed trajectory repeats them modulo period. The schedule cuts after the rotations with index period - 1, 2 * period - 1, ….

Main definitions

• trotterSchedule period wstar: the retained set after rotation g, namely the Paulis of weight at most wstar if g + 1 is a multiple of period, and all Paulis otherwise.
• trotterTraj: the rotation-indexed truncated trajectory trajTrunc with this schedule.
• trotterStepTraj: the step-indexed recurrence: apply the whole untruncated block, then cut.
• discardedStep d: the discarded operator X_{d+1} of apd:eq:step_component.

Main results

• trotterTraj_at_boundary: the two executions agree at every step boundary.
• discardedStep_eq_truncOp: X_{d+1} is the projection onto weights above wstar of the operator before truncation.
• pauliNorm_discardedStep: the Pauli norm of X_{d+1} is the high-weight norm before truncation. By contrast the kept operator has no high-weight mass (highNorm_trotterStepTraj_succ).
• pauliNorm_discardedStep_le: the single-rotation flow bound apd:thm:local_flow_k_local applied to the last rotation of a step.

Implementation notes

trotterStepTraj is defined independently of trotterTraj, so their agreement at step boundaries is a theorem and not a definition. The hypothesis 0 < period is needed only for this identification. The operator identities of this file assume neither locality of the generators nor any bound on the angles. The telescoping error estimate is in TruncationError.lean, and the layer-level version with its quantitative bound is in LayerError.lean.

def Lean4LPD.PauliString.trotterSchedule {n : ℕ} (period wstar g : ℕ) : Finset (PauliIndex n)

The end-of-step schedule of apd:thm:triangle: rotation g is followed by a cut exactly when g+1 is a multiple of the block length.

Equations

• Lean4LPD.PauliString.trotterSchedule period wstar g = if (g + 1) % period = 0 then (Lean4LPD.PauliString.highSet n wstar)ᶜ else Finset.univ

theorem Lean4LPD.PauliString.trotterSchedule_interior {n : ℕ} (period wstar d i : ℕ) (hi : i + 1 < period) : trotterSchedule period wstar (d * period + i) = Finset.univ

No cutoff inside a block, as required by apd:thm:triangle.

theorem Lean4LPD.PauliString.trotterSchedule_boundary {n : ℕ} (period wstar d : ℕ) (hp : 0 < period) : trotterSchedule period wstar (d * period + (period - 1)) = (highSet n wstar)ᶜ

The last rotation of each nonempty block is followed by the weight cut (apd:thm:triangle).

noncomputable def Lean4LPD.PauliString.trotterTraj {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (period wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) : ℕ → Matrix (Bits n) (Bits n) ℂ

Rotation-indexed execution of a fixed repeated block with end-of-step truncation (apd:thm:triangle; apd:eq:step_component).

Equations

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

@[simp]

theorem Lean4LPD.PauliString.trotterTraj_zero {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (period wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) : trotterTraj Gs θ period wstar O 0 = O

The trajectory starts at the input observable: no truncation is applied before the first rotation (apd:eq:step_component).

theorem Lean4LPD.PauliString.trotterTraj_succ {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (period wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (g : ℕ) : trotterTraj Gs θ period wstar O (g + 1) = truncOp (trotterSchedule period wstar g) (rot (Gs (g % period)).toMatrix (θ (g % period)) * trotterTraj Gs θ period wstar O g * rot (Gs (g % period)).toMatrix (-θ (g % period)))

One rotation of the boundary-scheduled execution (apd:thm:triangle).

noncomputable def Lean4LPD.PauliString.trotterStepTraj {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (period wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) : ℕ → Matrix (Bits n) (Bits n) ℂ

The step-indexed recurrence, defined independently of trotterTraj: evolve through a whole block, then cut (apd:eq:step_component; apd:thm:triangle).

Equations

• One or more equations did not get rendered due to their size.
• Lean4LPD.PauliString.trotterStepTraj Gs θ period wstar O 0 = O

@[simp]

theorem Lean4LPD.PauliString.trotterStepTraj_zero {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (period wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) : trotterStepTraj Gs θ period wstar O 0 = O

The step-indexed recurrence starts at the input observable itself (apd:eq:step_component).

theorem Lean4LPD.PauliString.trotterStepTraj_succ {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (period wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (d : ℕ) : trotterStepTraj Gs θ period wstar O (d + 1) = truncOp (highSet n wstar)ᶜ (traj Gs θ (trotterStepTraj Gs θ period wstar O d) period)

The recurrence of the kept operator: evolve through the whole block, then cut (apd:eq:step_component).

theorem Lean4LPD.PauliString.trotterTraj_within_step {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (period wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (d i : ℕ) (hi : i < period) : trotterTraj Gs θ period wstar O (d * period + i) = traj Gs θ (trotterTraj Gs θ period wstar O (d * period)) i

Before the boundary, no truncation interrupts the block's ordinary traj (apd:thm:triangle).

theorem Lean4LPD.PauliString.trotterTraj_next_boundary {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (period wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (d : ℕ) (hp : 0 < period) : trotterTraj Gs θ period wstar O ((d + 1) * period) = truncOp (highSet n wstar)ᶜ (traj Gs θ (trotterTraj Gs θ period wstar O (d * period)) period)

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

theorem Lean4LPD.PauliString.trotterTraj_at_boundary {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (period wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (d : ℕ) (hp : 0 < period) : trotterTraj Gs θ period wstar O (d * period) = trotterStepTraj Gs θ period wstar O d

The rotation-indexed execution agrees with the independently defined step recurrence at every boundary (apd:eq:step_component).

noncomputable def Lean4LPD.PauliString.discardedStep {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (period 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 the block before truncation, minus the kept operator. The zero-based index d is the number of steps completed before.

Equations

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

theorem Lean4LPD.PauliString.discardedStep_eq_truncOp {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (period wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (d : ℕ) : discardedStep Gs θ period wstar O d = truncOp (highSet n wstar) (traj Gs θ (trotterStepTraj Gs θ period wstar O d) period)

The discarded operator is the projection of the pre-truncation operator onto the Paulis of weight above wstar (apd:eq:step_component).

theorem Lean4LPD.PauliString.pauliNorm_discardedStep {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (period wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (d : ℕ) : pauliNorm (discardedStep Gs θ period wstar O d) = highNorm wstar (traj Gs θ (trotterStepTraj Gs θ period wstar O d) period)

The discarded operator's Pauli norm is the pre-truncation high-weight mass (apd:thm:triangle; apd:eq:step_component).

theorem Lean4LPD.PauliString.highNorm_trotterStepTraj_succ {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (period wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (d : ℕ) : highNorm wstar (trotterStepTraj Gs θ period wstar O (d + 1)) = 0

The retained operator has zero high-weight mass after each completed step. This is a support theorem, not an error bound (apd:eq:step_component).

theorem Lean4LPD.PauliString.trotterBlock_eq_boundary_pre {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (period wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (d : ℕ) (hp : 0 < period) : traj Gs θ (trotterStepTraj Gs θ period wstar O d) period = rot (Gs (period - 1)).toMatrix (θ (period - 1)) * trotterTraj Gs θ period wstar O (d * period + (period - 1)) * rot (Gs (period - 1)).toMatrix (-θ (period - 1))

The pre-truncation operator of a block is the last rotation of the block applied to the scheduled trajectory just before the boundary (apd:eq:step_component). This connects the step-indexed recurrence to the rotation-indexed local flow of Truncate.lean.

theorem Lean4LPD.PauliString.discardedStep_eq_boundary_sub {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (period wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (d : ℕ) (hp : 0 < period) : discardedStep Gs θ period wstar O d = rot (Gs (period - 1)).toMatrix (θ (period - 1)) * trotterTraj Gs θ period wstar O (d * period + (period - 1)) * rot (Gs (period - 1)).toMatrix (-θ (period - 1)) - trotterTraj Gs θ period wstar O ((d + 1) * period)

X_{d+1} is the operator after the last rotation of the block and before the cut, minus the scheduled trajectory at the boundary (apd:eq:step_component).

theorem Lean4LPD.PauliString.pauliNorm_discardedStep_eq_boundary_highNorm {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (period wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (d : ℕ) (hp : 0 < period) : pauliNorm (discardedStep Gs θ period wstar O d) = highNorm wstar (rot (Gs (period - 1)).toMatrix (θ (period - 1)) * trotterTraj Gs θ period wstar O (d * period + (period - 1)) * rot (Gs (period - 1)).toMatrix (-θ (period - 1)))

At a Trotter boundary, the Pauli norm of the discarded operator is the high-weight norm of the last rotation applied to the scheduled trajectory, which is the quantity that the local-flow bound controls (apd:thm:triangle). No such identification is made at interior rotations, where nothing is discarded.

theorem Lean4LPD.PauliString.pauliNorm_discardedStep_le {n : ℕ} {Gs : ℕ → PauliString n} {θ : ℕ → ℝ} {period wstar ko kh m : ℕ} {O : Matrix (Bits n) (Bits n) ℂ} (hG : ∀ (g : ℕ), IsSelfAdjoint (Gs g)) (hk : ∀ (g : ℕ), (Gs g).weight ≤ kh) (hp : 0 < period) (hm : 1 ≤ m) (hcut : wstar = rungWeight ko kh m) (d : ℕ) : have g := d * period + (period - 1); pauliNorm (discardedStep Gs θ period wstar O d) ≤ ladderNTrunc (fun (j : ℕ) => Gs (j % period)) (fun (j : ℕ) => θ (j % period)) (trotterSchedule period wstar) O ko kh m g + |Real.sin (θ (period - 1))| * ladderNTrunc (fun (j : ℕ) => Gs (j % period)) (fun (j : ℕ) => θ (j % period)) (trotterSchedule period wstar) O ko kh (m - 1) g

The single-rotation flow bound highNorm_conj_trajTrunc_le, applied to the last rotation of a step, bounds the discarded operator X_{d+1} (apd:eq:step_component; apd:thm:local_flow_k_local). This is a one-rotation estimate: its right-hand side still contains the two ladder rungs of the trajectory just before the boundary. The multi-layer bound on the sum of the discarded norms is in LayerError.lean.