TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge 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.

Product block-encoding error bound

Statement

Under the inputs and register order of Product block encoding with separate ancillas, let $C_{A}$ and $C_{B}$ be the two normalized compressed blocks, so $∥ C_{A} - A / α_{A} ∥_{o p} \leq ε_{A}$ and $∥ C_{B} - B / α_{B} ∥_{o p} \leq ε_{B}$ . The all-zero block of the constructed unitary is $C_{A} C_{B}$ . It obeys

${∥ C_{A} C_{B} - \frac{A B}{α_{A} α_{B}} ∥}_{o p} \leq ε_{A} \frac{∥ B ∥_{o p}}{α_{B}} + ε_{B} \frac{∥ A ∥_{o p}}{α_{A}} + ε_{A} ε_{B} \leq ε_{A} + ε_{B} + ε_{A} ε_{B} .$

Because each $C_{A}$ is itself a projected unitary block and hence a contraction, the sharper bound $∥ C_{A} C_{B} - A B / (α_{A} α_{B}) ∥_{o p} \leq ε_{B} + ε_{A} ∥ B ∥_{o p} / α_{B} \leq ε_{A} + ε_{B}$ also holds. In particular the product is an $(α_{A} α_{B}, a_{A} + a_{B}, ε_{A} + ε_{B} + ε_{A} ε_{B})$ block encoding of $A B$ .

Facts & Assumptions

Given: Square matrices and approximate block encodings satisfying the hypotheses of Product block encoding with separate ancillas and Finite block encoding.

[F1]

Finite block encoding: a normalized compressed block differs from its matrix divided by its positive normalization by at most the declared operator-norm error.

[F2]

Product block encoding with separate ancillas: the product circuit uses separate ancillas and the operator order $V_{A} V_{B}$ .

[F3]

The operator norm is submultiplicative and satisfies ||T^*T|| = ||T||^2: for compatible finite-dimensional maps, $∥ S T ∥_{o p} \leq ∥ S ∥_{o p} ∥ T ∥_{o p}$ .

[F4]

A projected unitary block is a contraction: every projected unitary block has operator norm at most one.

Proof

1.1F1F2givenconstructalgebra

Each lifted operation $V_{A}, V_{B}$ is a block-diagonal direct sum of copies of its supplied unitary on the untouched ancilla's computational basis; the inverse is the corresponding direct sum of the component inverse. Thus both lifts and $V_{A} V_{B}$ are unitary. Let $J$ inject the system into the all-zero state of both ancillas. The zero-subspace projections are $P_{A}$ and $P_{B}$ , with $P = P_{A} P_{B}$ , $P J = J$ , and $J^{†} P = J^{†}$ . In $J^{†} V_{A} V_{B} J$ , insert $P$ at both ends; commute $P_{B}$ through $V_{A}$ and use $P_{A} V_{B} = V_{B} P_{A}$ to obtain $J^{†} V_{A} P_{B} V_{B} J$ . The vector $P_{B} V_{B} J x$ has both ancillas zero and system component $C_{B} x$ , so $P_{B} V_{B} J = J C_{B}$ . The remaining compression is $J^{†} V_{A} J C_{B} = C_{A} C_{B}$ . Hence the all-zero block is exactly $C_{A} C_{B}$ in the stated order.

1.2F1F2F3algebra

Set $A^{'} : = A / α_{A}$ , $B^{'} : = B / α_{B}$ , $E_{A} : = C_{A} - A^{'}$ , and $E_{B} : = C_{B} - B^{'}$ . Then $C_{A} C_{B} - A^{'} B^{'} = E_{A} B^{'} + A^{'} E_{B} + E_{A} E_{B}$ . By [F1], $∥ E_{A} ∥ \leq ε_{A}$ and $∥ E_{B} ∥ \leq ε_{B}$ ; by the normalization promises, $∥ A^{'} ∥ \leq 1$ and $∥ B^{'} ∥ \leq 1$ . Applying [F3] to each summand yields the first displayed bound, and $∥ A ∥ / α_{A}, ∥ B ∥ / α_{B} \leq 1$ yields its conservative final bound.

2.1F1F3F4algebra∎

The same difference can be written $C_{A} E_{B} + E_{A} B^{'}$ . By [F4], $∥ C_{A} ∥ \leq 1$ , so [F3] gives $∥ C_{A} E_{B} + E_{A} B^{'} ∥ \leq ε_{B} + ε_{A} ∥ B ∥ / α_{B} \leq ε_{A} + ε_{B}$ . Also $∥ A B ∥ \leq ∥ A ∥ ∥ B ∥ \leq α_{A} α_{B}$ by [F3]; the product normalization is positive. The block-encoding definition therefore applies with the claimed error.

Depends on

Used by

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, Chapter 29 (17 April 2025) (standard reference, not scraped)
András Gilyén, Yuan Su, Guang Hao Low, and Nathan Wiebe, Quantum singular value transformation and beyond, Lemma 53 (standard reference, not scraped)