Pipeline-generated

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.

✓ 2 results · all verified · 2 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 2 also cleared it.

Block Encodings — Examples

1 · Prerequisites

2 · Summary

The examples calculate a two-term LCU with unequal component normalizations and a complex coefficient phase, then evaluate a two-factor normalized product-error bound on explicit diagonal matrices. Each compressed block is realized by a finite unitary dilation, and the query and implementation costs remain attached to the supplied PREPARE, SELECT and component calls.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Product block error in a two-factor instance

Example

Let $A = diag (1 / 2, 0)$ and $B = diag (1, 0)$ , with $α_{A} = 1$ , $α_{B} = 2$ , $ε_{A} = 1 / 10$ , and $ε_{B} = 1 / 5$ . Use the compressed blocks $C_{A} = diag (3 / 5, 0)$ and $C_{B} = diag (7 / 10, 0)$ . The example evaluates both the normalized product-error formula and its unnormalized version.

Facts & Assumptions

Given: The matrices and compressed blocks in the Example section, and the normalized product theorem Product block-encoding error bound.

[F1]

Product block-encoding error bound: the normalized two-factor product error is bounded by $ε_{A} ∥ B ∥ / α_{B} + ε_{B} ∥ A ∥ / α_{A} + ε_{A} ε_{B}$ .

[F2]

The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||: the operator norm of a diagonal matrix on the standard inner product space is its maximum action on a unit vector.

[F3]

The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ : $⟨ T x, y ⟩ = ⟨ x, T^{*} y ⟩$ .

[F4]

Linear isometries, and orthogonal or unitary operators on finite-dimensional inner product spaces: a unitary is an invertible linear isometry.

Verification

1.1givenF2F3F4constructalgebra

The errors are $E_{A} = C_{A} - A / α_{A} = diag (1 / 10, 0)$ and $E_{B} = C_{B} - B / α_{B} = diag (1 / 5, 0)$ . For a diagonal $D = diag (d_{1}, d_{2})$ , $∥ D x ∥^{2} = ∣ d_{1} ∣^{2} ∣ x_{1} ∣^{2} + ∣ d_{2} ∣^{2} ∣ x_{2} ∣^{2}$ , so the maximum on unit vectors is $\max (∣ d_{1} ∣, ∣ d_{2} ∣)$ , attained at the corresponding basis vector. Hence $∥ E_{A} ∥ = 1 / 10$ , $∥ E_{B} ∥ = 1 / 5$ , $∥ A ∥_{o p} = 1 / 2$ , and $∥ B ∥_{o p} = 1$ . For each of $C_{A}, C_{B}$ , put $S = \sqrt{I - C^{2}}$ and $D (C) = (\begin{array}{cc} C & S \\ S & - C \end{array})$ . The diagonal matrices $C, S$ commute and satisfy $C^{2} + S^{2} = I$ , so block multiplication gives $D (C)^{*} = D (C)$ and $D (C)^{2} = I$ . Then [F3] gives $∥ D (C) x ∥^{2} = ⟨ x, D (C)^{*} D (C) x ⟩ = ∥ x ∥^{2}$ , and [F4] makes $D (C)$ unitary; its top-left block is $C$ . Thus both chosen compressed blocks have exact unitary dilations.

2.1F1F2step 1.1algebra

The theorem's normalized bound is $(1 / 10) (1 / 2) + (1 / 5) (1 / 2) + (1 / 10) (1 / 5) = 17 / 100$ . The actual product block is $C_{A} C_{B} = diag (21 / 50, 0)$ , whereas $A B / (α_{A} α_{B}) = diag (1 / 4, 0)$ ; their difference has norm $21 / 50 - 1 / 4 = 17 / 100$ , so this instance attains that bound.

3.1F1step 2.1algebra∎

Multiplying the normalized error by $α_{A} α_{B} = 2$ gives unnormalized error $17 / 50$ . The looser universal normalized estimate is $ε_{A} + ε_{B} + ε_{A} ε_{B} = 8 / 25$ ; after scaling by $2$ , its unnormalized counterpart is $16 / 25$ . Neither bound is tight here.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Two-term LCU normalization and access count

Example

Take $A_{0} = diag (1, 0)$ , $A_{1} = diag (0, 1)$ , $α_{0} = 1$ , $α_{1} = 2$ , and coefficients $β_{0} = 1$ , $β_{1} = i$ . Use the exact one-ancilla block encodings constructed below. The example computes the LCU normalization, coefficient amplitudes, projected block, and charged access calls.

Facts & Assumptions

Given: The finite matrices and scalar values in the Example section, and the procedure and cost convention of LCU block-encoding construction and Block-encoding normalization, error, and cost accounting.

[F1]

LCU block-encoding construction: the coefficient weights are $∣ β_{j} ∣ α_{j} / Λ$ and SELECT applies phase $β_{j} / ∣ β_{j} ∣$ in branch $j$ .

[F2]

LCU projected-block correctness: the all-zero block is $\sum_{j} β_{j} A_{j} / Λ$ .

[F3]

Block-encoding normalization, error, and cost accounting: one LCU use invokes PREPARE, SELECT, and PREPARE $^{†}$ once each, with all primitive and synthesis costs kept explicit.

[F4]

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

[F5]

The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ : $⟨ T x, y ⟩ = ⟨ x, T^{*} y ⟩$ .

[F6]

Linear isometries, and orthogonal or unitary operators on finite-dimensional inner product spaces: a unitary is an invertible linear isometry.

Verification

1.1givenF4F5F6constructalgebra

The coordinate formulas give $∥ A_{0} ∥_{o p} = ∥ A_{1} ∥_{o p} = 1$ , so the chosen $α_{j}$ satisfy the normalization promises. For a positive diagonal contraction $C$ , put $S : = \sqrt{I - C^{2}}$ and $D (C) : = (\begin{array}{cc} C & S \\ S & - C \end{array})$ . Since $C$ and $S$ are commuting self-adjoint diagonal matrices and $C^{2} + S^{2} = I$ , direct block multiplication gives $D (C)^{*} = D (C)$ and $D (C)^{2} = I$ , hence $D (C)^{*} D (C) = I$ . The adjoint identity [F5] shows $∥ D (C) x ∥^{2} = ⟨ x, D (C)^{*} D (C) x ⟩ = ∥ x ∥^{2}$ , and $D (C)^{2} = I$ makes it invertible, so [F6] makes it unitary. Its top-left block is $C$ . Thus $D (A_{0} / α_{0})$ and $D (A_{1} / α_{1})$ are exact unitary block encodings with one component ancilla each.

1.2F1F2algebra

Here $Λ = ∣ 1 ∣ \cdot 1 + ∣ i ∣ \cdot 2 = 3$ , so $∣ χ ⟩ = \sqrt{1 / 3} ∣ 0 ⟩ + \sqrt{2 / 3} ∣ 1 ⟩$ . By [F1] and [F2], the projected block is $\frac{1}{3} A_{0} + \frac{2}{3} i (A_{1} / 2) = (A_{0} + i A_{1}) / 3 = diag (1 / 3, i / 3)$ ; the normalization is $3$ and the error is zero.

2.1F3givenalgebra∎

With PREPARE, SELECT, and PREPARE $^{†}$ separately supplied, the construction uses one call to each. If SELECT is assembled from component calls, its declaration must include one controlled call for each component branch and the relative phase operation; if those circuits are compiled from matrices, their data access and gate costs are added separately.

Block Encodings — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

Product block error in a two-factor instance

Example

Facts & Assumptions

Verification

Two-term LCU normalization and access count

Example

Facts & Assumptions

Verification

Sources