Exercise BE-004

The defined LCU stages have precise target/control registers and P† supplies the conjugate selector clean row. This architectural adjoint is sufficient, not uniquely forced by projected correctness; neither the clean block nor global unitarity implies deterministic auxiliary cleanup.

1. On coefficient×(selector×system), selectorLift targets the selector, amplitudeLift targets coefficient under selector/system controls, and selectLift preserves coefficient/selector labels while permuting the system; chronological order is PREPARE then AMPLITUDE then SELECT then the final selector stage.
2. The chosen final stage is P† on the same selector, yielding conjugate selector amplitudes in the clean projected block. A distinct Q=D P† fixing the clean bra gives the same block, while the H/controlled-X example leaves a nonzero dirty selector branch; projection is not deterministic cleanup.

Write basis states as |c,s,x>, with ordinary operator action on column states and the rightmost matrix factor acting first. The register grouping is C×(S×H), not an unspecified interchangeable set of ancillas. P_lift=I_C tensor(P tensor I_H) acts as |c,s,x> -> sum_t P[t,s]|c,t,x>. It changes selector amplitudes while preserving the coefficient and system basis labels. AMPLITUDE acts as |c,s,x> -> sum_d R_{s,x}[d,c]|d,s,x>; it targets the coefficient register, controlled by the existing selector and system labels. Its preserving those basis labels does not assert an absence of entanglement or an unchanged reduced quantum state. SELECT acts as |c,s,x> -> |c,s,p_s(x)>; it preserves coefficient and selector labels and permutes the system conditionally on selector. UNPREPARE in the defined architecture is P_lift†, acting on the SAME selector register and leaving coefficient/system labels as such unchanged. Chronologically the stages are P_lift, AMPLITUDE, SELECT, P_lift†, not the left-to-right written matrix order.

Fix clean labels c0 and s0 and put v_s=P[s,s0]. Since P is unitary, sum_s |v_s|^2=1, but P's unitarity alone does not specify any desired numerical weight distribution. On |c0,s0,y>, after the first three stages the state is sum_{s,c} v_s R_{s,y}[c,c0]|c,s,p_s(y)>. The clean output bra after P† supplies conjugate(v_s). Therefore, for J|y>=|c0,s0,y>, the projected system matrix K=J†WJ has entries K[x,y]=sum_{s:p_s(y)=x} conjugate(v_s) R_{s,y}[c0,c0] v_s. Equivalently this is the squared selector weight |v_s|^2 times each controlled coefficient clean entry, with the indicated system permutation constraint. This is the source's exact clean-entry structure. P† is a canonical sufficient choice: it pairs the prepared selector column with its conjugate bra. Complex coefficients/phases can reside in the coefficient-block clean entries; selector probabilities alone are not arbitrary signed/complex coefficients.

The final selector gate is NOT uniquely forced by this projected block. If the selector has dimension at least two, take a nonidentity selector unitary D with <s0|D=<s0|, for example D=diag(1,-1) with s0=0 on a qubit. Let Q=D P†. Then Q is unitary, Q differs from P†, and <s0|Q=<s0|P†. Thus replacing the final selector gate by Q leaves EVERY clean projected entry above unchanged, for the same intervening stages. In full-register notation W_Q=D_lift W and J†D_lift=J†, so J†W_QJ=J†WJ. The particularly simple P=I, AMPLITUDE=I, SELECT=I example gives W=I and W_Q=D_lift: distinct global unitaries with the identical clean system block I. A one-dimensional selector has no such nontrivial D, which does not restore a general uniqueness theorem. By contrast, demanding QP=I on the ENTIRE selector space uniquely forces Q=P† by multiplication by P† on the right. Equality of one clean row/projected action is strictly weaker than that full inverse requirement. An arbitrary independent gate need not give the desired weights; that lack of a blanket guarantee is not a proof that no different suitable gate can work.

Nor does the chosen P† generically clean the selector deterministically. Take a singleton coefficient register, selector and system qubits, P=H=(1/sqrt(2))[[1,1],[1,-1]], AMPLITUDE=I, and SELECT choosing p_0=I and p_1=X. From |s=0,x=0>, the states after PREPARE and SELECT are (|0,0>+|1,0>)/sqrt(2) and (|0,0>+|1,1>)/sqrt(2). Applying P†=H on the selector gives (|0,0>+|1,0>+|0,1>-|1,1>)/2. The selector-one branch has squared norm1/2. Here K=(I+X)/2, and K|0>=(|0>+|1>)/2 is the unnormalized selector-zero branch with success probability1/2, not the whole state. Normalizing that accepted branch gives |+>; the other selector sector has not vanished. All local unitary/permutation requirements and the source architecture are satisfied.

The auxiliary subsystem designated by J is BOTH coefficient and selector at c0,s0 (usually their zero labels), not the system data register. Clean projection fixes those labels on the accepted branch; it does not assert all outputs have those labels. In general coefficient leakage may occur as well, since an amplitude rotation need not return its target coefficient to c0. A genuine deterministic cleanup claim would require an additional theorem that (I-JJ†)WJ=0, which this architecture does not supply merely from P† and local unitarity. These are exact logical matrix/register semantics, not an elementary-gate compilation, finite-bit resource bound or a guaranteed successful state-preparation procedure.

1. Assigns PREPARE/UNPREPARE to the same selector, AMPLITUDE to the coefficient controlled by selector/system, and SELECT to the controlled system permutation; gives basis actions and correct chronological versus matrix-factor order. (1 weight)
2. Derives or explains the conjugate PREPARE clean row and the projected weighted-entry structure with both coefficient and selector fixed at designated clean values. Treats P† as the architecture's sufficient adjoint choice, not a unique final gate. (1 weight)
3. Separates exact inverse uniqueness on the entire selector from clean-row equality: supplies a valid nontrivial D fixing the clean bra and Q=D P† with the same projected block. Refutes deterministic cleanup using the fully evaluated H/controlled-X example and distinguishes unnormalized accepted branch/probability from the complete output. (1 weight)

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

• QuantumBlockEncoding/Robin/ComplexLCU.lean

  def selectorLift (lines 253-264); def amplitudeLift (lines 283-294); def selectLift (lines 329-337); def prepareAmplitudeSelectUnprepare 'star (selectorLift ... prepare) * (selectLift ... * (amplitudeLift rotation * selectorLift ... prepare))' (lines 351-367)

  Source SHA-256: aa51d33a6ca788b17879e1d88030b525f4f035c97d74588636ccf25f8c04b843 · MIT (repository LICENSE)

Contract: 112521b12612f1c530e7fffe4738eab90f97fd054cc6f06e90a5a93ecbb57666

Item digest: ff8d58144358000f0819569e29e66c610374b36355831065ff543f2ebc9f37c6

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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

{ "question_version": 2, "predecessor_key": "qcb-core-be-004", "predecessor_item_digest": "69ef913513b5551fc106df171152b284d3ab8de62ca563ee680e1e751cfaa977", "predecessor_contract_hash": "de212863300e2df799356b50dc2ec077f1b268a6e82e0b2442ab95029905e0e7", "current_contract_hash": "112521b12612f1c530e7fffe4738eab90f97fd054cc6f06e90a5a93ecbb57666", "changed_contract_fields": [ "question" ], "repair_record": "shared/repairs/be-004-stage-role-projection-question-successor.json", "repair_record_digest": "f6754efc28a9919eb73ccebc5187deec5f58648be6080113e9887eaf583ccda2", "review_record": "reports/textbook-v1/repairs/be-004-stage-role-projection-question-successor-review.json", "review_digest": "769144ed58c5fcaf0669a7a3ab57df57fcea583c36bb523cf8a3355ca8143016", "equivalence_to_predecessor_claimed": false, "additional_core_count": 0 }