Block Encoding

Exercise BE-006

advanced · proof · train

local source supported. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.

Assumptions and conventions

Input and output pinned to the clean coefficient and clean selector
rotation(j,systemColumn) is a coefficient-register unitary; only its clean diagonal entry survives

SELECT uses the controlled system equivalence; matching condition is permutation(j)(systemColumn) = systemRow
PREPARE amplitude is prepare(j, cleanSelector); UNPREPARE contributes its complex conjugate

Question

For the logical unprepare-select-amplitude-prepare LCU matrix on registers coefficient x (selector x system), derive the exact clean projected entry between clean input (clean coefficient, clean selector, systemColumn) and clean output (clean coefficient, clean selector, systemRow). Show that it is a finite sum over selector indices, that each surviving term carries the SELECT matching condition on the system permutation, and that each term's weight is the conjugate of a PREPARE amplitude times the controlled coefficient rotation diagonal entry times the PREPARE amplitude. Explain concretely why the selector weight appears as conjugate-times-itself and what this means physically.

Hint: mathematical route

Derives the exact clean projected entry of the logical LCU matrix as a selector sum with SELECT matching indicator and conjugate-times-itself PREPARE weights, explaining the |prepare|^2 selection probability and the shared selector register.

The clean PREPARE-dagger bra turns the matrix product into a selector sum weighted by conj(prepare(j,cleanSelector)).
SELECT after AMPLITUDE after PREPARE on a clean column yields the permutation indicator times the clean coefficient rotation diagonal times prepare(j,cleanSelector).
Combining gives the exact clean entry with weight conj(prepare)*rotation-diagonal*prepare, i.e. |prepare|^2 when the diagonal is 1.

Reference solution

Project the logical matrix onto the clean coefficient and clean selector on both sides, leaving system indices systemRow (output) and systemColumn (input). The clean entry equals the finite sum over all selector indices j of: [if permutation(j) applied to systemColumn equals systemRow then conj(prepare(j, cleanSelector)) * rotation(j, systemColumn)(cleanCoefficient, cleanCoefficient) * prepare(j, cleanSelector) else 0]. Derivation: UNPREPARE = PREPARE-dagger lifted on the selector contributes the clean bra, which turns the matrix product into a selector sum against conj(prepare(j, cleanSelector)) and forces the coefficient and system row labels; AMPLITUDE contributes the controlled coefficient-register entry rotation(j, systemColumn)(cleanCoefficient, cleanCoefficient) on the clean coefficient diagonal; SELECT contributes the indicator that the controlled system permutation for selector j maps the input systemColumn to the output systemRow; PREPARE contributes the ket amplitude prepare(j, cleanSelector). The selector weight is conj(prepare(j,cleanSelector)) * (...) * prepare(j,cleanSelector): the factor prepare(j,cleanSelector) comes from PREPARE loading the selector superposition from the clean selector, and the factor conj(prepare(j,cleanSelector)) comes from UNPREPARE = PREPARE-dagger projecting back onto the clean selector. Physically this is why PREPARE and UNPREPARE must be the SAME gate up to adjoint acting on the SAME selector register: the clean amplitude of each term is weighted by |prepare(j,cleanSelector)|^2 when the coefficient rotation diagonal is 1, i.e. by the probability of selecting term j, so the clean block is the probability-weighted (and coefficient-weighted) combination of the per-term system permutations. If prepare and unprepare were independent, the two factors would not form conj(x)*x and the clean weights would not be the intended squared selection amplitudes.

Assessment rubric

State the exact clean entry as a selector sum with the SELECT matching indicator permutation(j)(systemColumn)=systemRow and zero otherwise (1 weight)
Identify the three nonzero factors per term: conj(prepare(j,cleanSelector)) from UNPREPARE, the clean coefficient rotation diagonal from AMPLITUDE, and prepare(j,cleanSelector) from PREPARE (1 weight)
Explain the conjugate-times-itself weight as |prepare(j,cleanSelector)|^2 (selection probability) arising because UNPREPARE is PREPARE-dagger on the same selector register, and note it fails for independent gates (1 weight)

Graph-grounded prerequisites

These are support/source anchors, not an automatically extracted theorem-dependency proof.

Download the shared core registry

Lean view and evidence boundary

No aligned Lean view has been admitted for this native core in this textbook checkpoint. This is not a claim that the underlying mathematics lacks a formal proof. Contributions must preserve this exact target contract and split.

Read the Lean track and existing diagnostic warmups

Sources and provenance

QuantumBlockEncoding/Robin/ComplexLCUProjection.lean
theorem prepareAmplitudeSelectUnprepare_cleanEntry giving the selector sum 'if permutation selectorIndex systemColumn = systemRow then star (prepare ...) * rotation ... * prepare ... else 0' (lines 171-220); star_selectorLift_mul_clean (lines 147-169); selectLift_mul_amplitudeLift_mul_selectorLift_clean (lines 112-144)
Source SHA-256: fa0b84ce5c819184f190b81b4d259e12f725e6196cd37147984fab76fe4ec340 · MIT (repository LICENSE)
QuantumBlockEncoding/Robin/ComplexLCU.lean
def prepareAmplitudeSelectUnprepare (lines 351-367)
Source SHA-256: aa51d33a6ca788b17879e1d88030b525f4f035c97d74588636ccf25f8c04b843 · MIT (repository LICENSE)

Contract: 0de3c24a0ef81d66cc0335a09491db3c65b2a30b7af82dc6a6fc933d8a4efd69

Item digest: 5e2925c035693a4f8034296aa2d0448e56e059aac0db6f66de4b45cc440f9fb2

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

Authored support steps: 3. This is not measured graph distance or model difficulty.