Exercise BE-112

The chosen PREPARE† SELECT AMPLITUDE PREPARE matrix is unitary by tensor/block/permutation, adjoint and product closure. Neither global unitarity nor a fixed clean projected block forces a unique final adjoint or deterministic auxiliary cleanup; full inverse uniqueness is a separate stronger requirement.

1. P_lift is unitary as the tensor lift of the stipulated selector PREPARE; its role is chronologically first despite being the rightmost written factor.
2. P_lift† is unitary by adjoint closure of the unitary group, giving one certified final factor for the chosen architecture.
3. A_lift is unitary as a block-diagonal family of coefficient unitaries, and S_lift is unitary as the controlled basis permutation.
4. All four fixed-register factors are unitary, so their product is unitary by group closure (equivalently the explicit adjoint-product cancellations). No deterministic cleanup follows from that conclusion.
5. The architecture chooses P† and full inverse QP=I uniquely requires it, but global unitarity admits other certified final gates; a clean-row-fixing D also preserves the projected block, while the H/controlled-X example refutes automatic selector cleanup after intervening stages.

Use column-vector operator convention. The written product W=P_lift† S_lift A_lift P_lift acts chronologically as PREPARE, AMPLITUDE, SELECT, then PREPARE†. It does not apply the leftmost dagger first. All factors act on the same C×(S×H) register, so the products are typed; no clean input or postselection premise is needed for the GLOBAL unitarity proof.

(1) P_lift=I_C tensor(P tensor I_H) is unitary because tensor products of unitary matrices are unitary, and the two identities and selector P are unitary. (2) P_lift† is unitary by adjoint closure of the unitary group. (3) A_lift is block diagonal over contexts (s,x), with coefficient block R_{s,x}; its adjoint product is block diagonal with blocks R_{s,x}†R_{s,x}=I_C, so it is unitary. S_lift is a basis-permutation matrix: each basis column is sent bijectively to |c,s,p_s(x)>, so its columns are orthonormal and it is unitary. (4) Closure under multiplication on the fixed total register now makes W a product of four unitaries. Explicitly, W†W=P_lift† A_lift† S_lift† P_lift P_lift† S_lift A_lift P_lift =P_lift† A_lift† A_lift P_lift=I; the intervening cancellations use P_lift P_lift†=I, S_lift†S_lift=I and A_lift†A_lift=I. The reverse product is I as well. This argument is valid also for empty finite index sets; auxiliary clean labels are used only where they actually exist for a projected block or the examples below.

(5) P† is the defined, sufficient adjoint/inverse choice, but global unitarity does NOT force that choice. Replacing the final selector factor by ANY unitary Q gives Q_lift S_lift A_lift P_lift, again unitary by the same product rule. In particular Q=I uses the known unitary identity and no additional unknown certificate; Q=P inherits unitarity from the existing PREPARE certificate. Thus the old claim that a different final gate cannot be guaranteed unitary from those facts is false. Its clean projected block generally changes: take singleton coefficient/system registers, P=H on a qubit selector, and A=S=I. The chosen W=H†H=I has clean scalar1; the unitary replacement Q=I gives W_Q=H with clean scalar1/sqrt(2). This is a precise distinction between global unitarity and intended LCU clean-entry correctness.

A complete inverse requirement is stronger and does single out the adjoint: if QP=I on the ENTIRE selector space and P is unitary, multiply on the right by P† to get Q=P†. With nontrivial amplitude/SELECT in between, however, the final P† is not adjacent to the original P. Inverting P alone does not invert S_lift A_lift, and global product unitarity says nothing about deterministic auxiliary cleanup.

Preserving only the clean projected block is weaker still. Let clean selector be0, D=diag(1,-1) on a qubit selector, and Q=D P†. Then Q is a distinct unitary with <0|Q=<0|P†. For clean injection J|x>=|c0,0,x>, the full replacement W_Q=D_lift W satisfies J†W_QJ=J†WJ, independently of the particular intervening A,S. This is a shared clean-row LCU subproof with the linked BE004 repair, not a separate new mathematical core. Requiring a particular projected entry/row does not uniquely specify all unitary columns or a full inverse. With singleton coefficient/system and P=I,A=S=I, W=I and W_Q=D already give an explicit distinct pair with the same clean scalar1.

For a direct failure of deterministic cleanup within the CHOSEN architecture itself, take singleton coefficient, selector/system qubits, P=H, amplitude I, and p_0=I,p_1=X for SELECT. On |0,0>, PREPARE then SELECT gives (|0,0>+|1,1>)/sqrt(2). The final P†=H gives (|0,0>+|1,0>+|0,1>-|1,1>)/2 in selector/system notation. Selector1 has probability1/2, despite all three local certificates. The clean projected block is (I+X)/2, not a deterministic normalized system action. In general coefficient leakage can occur too, since its amplitude gates need not fix the chosen clean coefficient label. A deterministic cleanup theorem would require the additional condition (I-JJ†)WJ=0; global unitarity alone does not imply it. This H/controlled-X witness is the same elementary boundary subproof used in the linked BE004 repair; the present core's main task remains assembling global unitarity rather than assigning stage roles.

The source therefore proves a sufficient product-unitarity theorem for its explicit adjoint architecture. It does not prove unique-final-gate necessity or a full-output cleanup property. No gate compilation, state-preparation success guarantee, query count or finite-bit resource theorem follows merely from this logical group-closure calculation.

1. Identifies the four written matrix factors and correct chronological action; derives lifted PREPARE, amplitude-family and SELECT unitarity from tensor, block-diagonal and permutation facts respectively. (1 weight)
2. Uses adjoint closure and multiplication closure (or equivalent explicit dagger-product cancellations) to prove the entire chosen product unitary without inserting a clean-input or cleanup hypothesis. (1 weight)
3. Distinguishes architectural P†/unique full inverse from a necessary condition for global unitarity: gives a certified alternative final gate such as I, shows its projected block can change, and also gives a distinct Q=D P† with the same clean row/block. (1 weight)
4. Refutes deterministic auxiliary cleanup after intervening operations using the fully evaluated H/controlled-X example; keeps projected unnormalized action, accepted labels and extra full-output cleanup condition separate. Does not turn group membership into a success/resource or uniqueness theorem. (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

  noncomputable def prepareAmplitudeSelectUnprepare (prepare ...) (rotation ...) (permutation ...) := star (selectorLift ... prepare) * (selectLift ... permutation * (amplitudeLift rotation * selectorLift ... prepare)) (lines 352-367); theorem prepareAmplitudeSelectUnprepare_unitary ... (lines 370-399)

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

Contract: f0d61f87e50ec90e5811ab7333684aaae090d01347814e037b5ed6c241ae9e61

Item digest: b8e9794f7bb8d12f2bbfb63c310d9e29cd2fde308eab5dd83320a05a743f9736

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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

{ "question_version": 2, "predecessor_key": "qcb-core-be-112", "predecessor_item_digest": "c9008a445032f5ece7e8068ed7a580c1a74eda9188a36cdaac48888b6da4cc19", "predecessor_contract_hash": "f64837f9c986dd70c8674308b444a2520ddf8f79805e5f7866e5b114aefb2b7d", "current_contract_hash": "f0d61f87e50ec90e5811ab7333684aaae090d01347814e037b5ed6c241ae9e61", "changed_contract_fields": [ "question" ], "repair_record": "shared/repairs/be-112-unitarity-versus-adjoint-question-successor.json", "repair_record_digest": "f351324a881cf91ba38563bd9f1040457e2ec256284146c040c43bcbda21c0ab", "review_record": "reports/textbook-v1/repairs/be-112-unitarity-versus-adjoint-question-successor-review.json", "review_digest": "a074a89cff4dd2cd56d3cf57cc78fceb917640fe006d14b299ad8790d082bd49", "equivalence_to_predecessor_claimed": false, "additional_core_count": 0 }