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.

Higher-order product-formula error with explicit term counts

Statement

Let $k, m, r \geq 1$ , let $H_{1}, \dots, H_{m}$ be self-adjoint endomorphisms of a finite-dimensional complex inner-product space, and put $H = \sum_{j} H_{j}$ , $M = \sum_{j} ∥ H_{j} ∥$ , and $q = 2 k + 1$ . Expand one recursive segment as $S_{2 k} (h) = \prod_{ν = 1}^{L} e^{- i h c_{ν} H_{j_{ν}}}$ in its declared order and set $B_{k} = \sum_{ν = 1}^{L} ∣ c_{ν} ∣ ∥ H_{j_{ν}} ∥$ . For every real $t$ , $∥ S_{2 k} (t / r)^{r} - U_{H} (t) ∥ \leq \frac{(B_{k}^{q} + M^{q}) ∣ t ∣^{q}}{q! r^{q - 1}} .$ The expanded term count is $L = (2 m - 1) 5^{k - 1}$ per segment. If $t$ is rational with an exact finite code, a rational tolerance $ϵ > 0$ and rational upper bounds $\overline{B} \geq B_{k}$ , $\overline{M} \geq M$ are supplied, a finite integer search for the least $r \geq 1$ satisfying $r^{q - 1} q! ϵ \geq ({\overline{B}}^{q} + {\overline{M}}^{q}) ∣ t ∣^{q}$ makes the displayed exact-call error at most $ϵ$ . For the resource claims when $t \neq 0$ , require the term-list input to support every actual signed call code $c_{ν} t / r$ for its term $H_{j_{ν}}$ in the fully expanded segment, including half-time base calls and negative central calls, and to declare an implementation and per-call cost at each such code. An inverse or time-reversed implementation must be separately declared with its own cost and error record; forward access alone does not supply it. When $t \neq 0$ and term circuits are approximate, add the sum of all per-call operator-norm errors separately; to keep total error at most $ϵ$ , use $ϵ / 2$ in the integer search and require the sum of call errors over all $r L$ calls to be at most $ϵ / 2$ . When $t \neq 0$ , the term-call contributions to query and gate costs are the sums of the declared costs at the actual signed times in one expanded word, multiplied by $r$ ; when $t = 0$ , the recursive algorithm returns the identity with no term calls. The separately declared product-composition overheads $Q_{w r a p}$ and $G_{w r a p}$ are added to those totals; coefficient, description-bit, ancilla, and classical-generation resources remain separate coordinates.

Facts & Assumptions

Given: The finite term list $H_{1}, \dots, H_{m}$ , integer $k, r \geq 1$ , and real time $t$ .

[F1]

Suzuki recursive cancellation of error terms proves that $S_{2 k}$ and $U_{H}$ have matching Taylor coefficients through degree $2 k$ .

[F2]

Finite higher-order Suzuki product formula expands each segment into five copies per recursion level, starting from the $2 m - 1$ factors of $S_{2}$ .

[F3]

Unitary and differential identities for finite matrix dynamics gives unitarity and $U_{H}^{'} (h) = - i H U_{H} (h)$ .

[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 (and as zero on the zero domain).

[F5]

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

[F6]

Term-list Hamiltonian access charges each supported signed term call and separately records query, gate, coefficient, and generation costs.

[A1]

For the resource claims when $t \neq 0$ , each actual call in the expanded word is supported at its signed time code and has a declared implementation and per-call cost; any inverse or time-reversed route is separately declared.

Proof

1.1givenF3F4F5algebra

The claim is immediate on the zero-dimensional space, so assume $V \neq {0}$ . Write the expanded segment as $P (h) = F_{1} (h) \dots F_{L} (h)$ , where $F_{ν} (h) = e^{- i h c_{ν} H_{j_{ν}}}$ . Repeated differentiation gives $F_{ν}^{(a)} (h) = (- i c_{ν} H_{j_{ν}})^{a} F_{ν} (h)$ , so [F3]–[F5] imply $∥ F_{ν}^{(a)} (h) ∥ \leq ∣ c_{ν} ∣^{a} ∥ H_{j_{ν}} ∥^{a}$ . The full multinomial sum is $\sum_{a_{1} + \dots + a_{L} = q} \frac{q!}{a_{1}! \dots a_{L}!} \prod_{ν} (∣ c_{ν} ∣ ∥ H_{j_{ν}} ∥)^{a_{ν}} = (\sum_{ν} ∣ c_{ν} ∣ ∥ H_{j_{ν}} ∥)^{q} = B_{k}^{q}$ , proving $∥ P^{(q)} (h) ∥ \leq B_{k}^{q}$ . Repeatedly differentiating [F3] gives $U_{H}^{(q)} (h) = (- i H)^{q} U_{H} (h)$ . The triangle inequality from [F4] gives $∥ H ∥ \leq \sum_{j} ∥ H_{j} ∥ = M$ , hence $∥ U_{H}^{(q)} (h) ∥ \leq M^{q}$ .

2.1step 1.1F1algebra

By [F1], $P - U_{H}$ has zero Taylor coefficients through degree $q - 1$ . The integral Taylor remainder of order $q$ gives $∥ P (h) - U_{H} (h) ∥ \leq \int_{0}^{∣ h ∣} \frac{(∣ h ∣ - s)^{q - 1}}{(q - 1)!} (B_{k}^{q} + M^{q}) d s = \frac{(B_{k}^{q} + M^{q}) ∣ h ∣^{q}}{q!}$ , using a change of variable when $h < 0$ .

3.1step 2.1F3F4F5algebra

Both $P (h)$ and $U_{H} (h)$ are unitary. Their operator norms and those of their inverses are one by the unit-vector definition [F4]; submultiplicativity [F5] then shows that each unitary factor preserves the norm in a telescoping expansion. Thus their $r$ th-power difference is at most $r$ times the local bound in step 2.1. Substituting $h = t / r$ yields the displayed global error.

4.1step 3.1F2F3F5F6algebra∎

The base segment has $2 m - 1$ term calls by [F2]; every recursive level replaces one formula by five copies, so induction gives $L = (2 m - 1) 5^{k - 1}$ . When $t \neq 0$ , [A1] supplies each call at signed time $c_{ν} t / r$ with its query and gate costs, so $r$ identical segments multiply their term-call contributions by $r$ ; when $t = 0$ , the procedure returns the identity and makes no term calls. Add the separately declared product-composition charges $Q_{w r a p}$ and $G_{w r a p}$ to obtain total query and gate costs; coefficient, description-bit, ancilla, and classical-generation costs stay separate as required by [F6]. If the $ν$ th exact call is replaced by a unitary call with error $η_{ν}$ , expanding the difference of the two products one factor at a time and applying the norm invariance in step 3.1 bounds the total change by $\sum_{ν} η_{ν}$ over all $r L$ calls. Finally, the integer search terminates because its left side grows without bound; its inequality and the certified upper bounds make the exact-call error at most $ϵ$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

32 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)