TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

First-order commutator error

Statement

Let $V$ be a finite-dimensional complex inner-product space, let $H_{1}, \dots, H_{m}$ be self-adjoint endomorphisms of $V$ with $m \geq 1$ , and set $H = \sum_{j = 1}^{m} H_{j}$ . For every real $t$ and integer $r \geq 1$ , $∥ S_{1} (t / r)^{r} - U_{H} (t) ∥ \leq \frac{t^{2}}{2 r} \sum_{1 \leq j < k \leq m} ∥ [H_{j}, H_{k}] ∥,$ where $S_{1}$ has the fixed order of First-order Lie product formula and $U_{H} (t) = e^{- i t H}$ is the finite-matrix evolution of Finite Hermitian matrix dynamics.

Facts & Assumptions

Given: The finite-dimensional space $V$ , self-adjoint terms $H_{1}, \dots, H_{m}$ , $m \geq 1$ , $t \in R$ , and $r \geq 1$ .

[F1]

First-order Lie product formula defines $S_{1} (h) = e^{- i h H_{1}} \dots e^{- i h H_{m}}$ in the announced order.

[F2]

Unitary and differential identities for finite matrix dynamics states that $U_{K} (s)$ is unitary, $U_{K}^{'} (s) = - i K U_{K} (s)$ , and $U_{K} (s + u) = U_{K} (s) U_{K} (u)$ for every finite-dimensional self-adjoint $K$ and real $s, u$ .

[F3]

The operator norm is submultiplicative and satisfies ||T^*T|| = ||T||^2 gives submultiplicativity of the operator norm.

[F4]

The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv|| defines the operator norm by the maximum over unit vectors.

Proof

1.1givenF2construct

If $V = {0}$ , every endomorphism is the unique zero map and both sides of the theorem are zero. Otherwise, for self-adjoint $H_{1}, H_{2}$ , put $A = - i H_{1}$ and $B = - i H_{2}$ . For $h \geq 0$ define $F (s) = e^{(h - s) (A + B)} e^{s A} e^{s B}$ for $0 \leq s \leq h$ . Its endpoints are $F (0) = e^{h (A + B)}$ and $F (h) = e^{h A} e^{h B}$ . Differentiating the three finite-matrix evolutions using [F2] and the entrywise product rule gives $F^{'} (s) = e^{(h - s) (A + B)} (e^{s A} B - B e^{s A}) e^{s B}$ .

2.1step 1.1F2F3F4algebra

For fixed $s \geq 0$ , differentiating $e^{u A} B e^{(s - u) A}$ for $0 \leq u \leq s$ and integrating yields $e^{s A} B - B e^{s A} = \int_{0}^{s} e^{u A} [A, B] e^{(s - u) A} d u$ . For unitaries $R, S$ , [F2] and [F4] give $∥ R ∥ = ∥ S ∥ = ∥ R^{- 1} ∥ = ∥ S^{- 1} ∥ = 1$ ; [F3] applied to $R X S$ and then to $R^{- 1} (R X S) S^{- 1}$ gives $∥ R X S ∥ = ∥ X ∥$ . Thus the unitary factors in the integrands and in [step 1.1] give $∥ F^{'} (s) ∥ \leq s ∥ [A, B] ∥$ . Integrating from $0$ to $h$ gives $∥ e^{h (A + B)} - e^{h A} e^{h B} ∥ \leq h^{2} ∥ [A, B] ∥ / 2$ . For $h < 0$ apply the same result to $- A, - B$ and $∣ h ∣$ ; since $[A, B] = - [H_{1}, H_{2}]$ , the bound is $h^{2} ∥ [H_{1}, H_{2}] ∥ / 2$ for all real $h$ .

3.1step 2.1F1F2F3F4algebra

Put $A_{j} = - i H_{j}$ . For $k = 1, \dots, m$ , let $P_{k} = e^{h A_{1}} \dots e^{h A_{k}}$ and $T_{k} = e^{h \sum_{j = 1}^{k} A_{j}}$ . Adding and subtracting $e^{h \sum_{j < k} A_{j}} e^{h A_{k}}$ and applying the two-term estimate in [step 2.1] gives $∥ T_{k} - P_{k} ∥ \leq ∥ T_{k - 1} - P_{k - 1} ∥ + \frac{h^{2}}{2} ∥ [\sum_{j < k} A_{j}, A_{k}] ∥$ . Linearity gives $[\sum_{j < k} A_{j}, A_{k}] = \sum_{j < k} [A_{j}, A_{k}]$ , and $[A_{j}, A_{k}] = - [H_{j}, H_{k}]$ ; the triangle inequality from [F4] bounds this norm by $\sum_{j < k} ∥ [H_{j}, H_{k}] ∥$ . Right multiplication by $e^{h A_{k}}$ preserves the norm by the unitary norm argument in [step 2.1]. Starting with $T_{1} = P_{1}$ and iterating proves the local $m$ -term bound $∥ e^{- i h H} - S_{1} (h) ∥ \leq \frac{h^{2}}{2} \sum_{j < k} ∥ [H_{j}, H_{k}] ∥$ .

4.1step 2.1step 3.1F1F2F3F4algebra∎

Set $h = t / r$ . The identity $S^{r} - U^{r} = \sum_{ℓ = 0}^{r - 1} S^{r - 1 - ℓ} (S - U) U^{ℓ}$ writes the difference as $r$ terms. The unitary norm argument in [step 2.1] bounds each term by $∥ S_{1} (h) - U_{H} (h) ∥$ , so [step 3.1] gives $∥ S_{1} (h)^{r} - U_{H} (h)^{r} ∥ \leq \frac{t^{2}}{2 r} \sum_{j < k} ∥ [H_{j}, H_{k}] ∥$ . By [F2], $U_{H} (h)^{r} = U_{H} (t)$ .

Depends on

Used by

First-order error for two Pauli terms Example
Finite adiabatic path simulation from term access Theorem
First-order query and gate cost Theorem

Dependency tree · two levels

22 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Andrew M. Childs, Lecture Notes on Quantum Algorithms (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes (standard reference, not scraped)