Oracle Composition

Exercise BE-109

intermediate · proof · dev

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

Assumptions and conventions

PREPARE is unitary on the selector register alone
The lift tensors identities on the coefficient and system registers

The identity matrix is a unitary on any register
star of a Kronecker product is the Kronecker product of the stars

Question

A state-preparation unitary acts only on a selector register, but inside a composite machine it is applied on the full product register coefficient x (selector x system) as identity-on-coefficient tensor (PREPARE tensor identity-on-system). Prove that if PREPARE is unitary on the selector register alone then this tensor-lifted operator is unitary on the whole product register, and explain the physical reading: tensoring a gate with 'do nothing' on untouched registers never spoils unitarity.

Hint: mathematical route

Lifting a selector PREPARE to the full register as I ⊗ (PREPARE ⊗ I) preserves unitarity by applying the Kronecker-product-of-unitaries law twice; identities on untouched registers are inert unitaries.

The lifted operator is the Kronecker product I_c ⊗ (PREPARE ⊗ I_s) on coefficient x (selector x system).
The Kronecker product of two unitaries is unitary because star(M⊗N)=star(M)⊗star(N) and (star(M)⊗star(N))(M⊗N)=I⊗I.
Inner step: PREPARE is unitary and I_s is unitary, so PREPARE ⊗ I_s is unitary.
Outer step: I_c is unitary, so I_c ⊗ (PREPARE ⊗ I_s) is unitary on the whole register.
Physically, identities represent inert untouched registers, and the unitarity check factorizes per subsystem, so tensoring with them never spoils unitarity.

Reference solution

The lifted operator is L = I_c ⊗ (PREPARE ⊗ I_s), a Kronecker product acting on the compound index coefficient x (selector x system). The governing fact is that the Kronecker product of two unitaries is unitary: if M and N are unitary on their respective factors then M ⊗ N is unitary on the product, because star(M ⊗ N) = star(M) ⊗ star(N) and (star(M) ⊗ star(N))(M ⊗ N) = (star(M) M) ⊗ (star(N) N) = I ⊗ I = I. Apply this twice. Inner step: PREPARE is unitary by hypothesis and I_s (the identity on the system) is unitary (its conjugate transpose is itself and the product is the identity), so PREPARE ⊗ I_s is unitary on selector x system. Outer step: I_c (identity on coefficient) is unitary, and PREPARE ⊗ I_s is unitary from the inner step, so I_c ⊗ (PREPARE ⊗ I_s) is unitary on the whole register. The physical reading: 'do nothing' on a register is represented by the identity, which is a trivial unitary; tensoring any unitary with identities on registers it does not touch leaves it unitary because the Kronecker factorization of the unitarity check splits into independent per-factor identities. A unitary gate that physically touches only one subsystem therefore remains a legitimate reversible operation on the enlarged machine, with the untouched registers carried along inertly.

Assessment rubric

State the lift as I_c ⊗ (PREPARE ⊗ I_s) and invoke that the Kronecker product of unitaries is unitary via star(M⊗N)=star(M)⊗star(N) (1 weight)
Apply the Kronecker fact twice: PREPARE ⊗ I_s unitary (inner), then I_c ⊗ (that) unitary (outer), using that identities are unitary (1 weight)
Give the physical reading: tensoring a gate with identity on untouched registers preserves unitarity because the check factorizes per subsystem (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/ComplexLCU.lean
def selectorLift (prepare : _root_.Matrix selector selector ℂ) : ... := (1 : _root_.Matrix coefficient coefficient ℂ) ⊗ₖ (prepare ⊗ₖ (1 : _root_.Matrix system system ℂ)) (lines 254-264); theorem selectorLift_unitary ... := by apply _root_.Matrix.kronecker_mem_unitary ... (lines 267-281)
Source SHA-256: aa51d33a6ca788b17879e1d88030b525f4f035c97d74588636ccf25f8c04b843 · MIT (repository LICENSE)

Contract: 9cb3520780bf5e7915ba05e2048371cb7c177068ffbe824cbb0370bbc9a4bc48

Item digest: 76cc51c2e49f3f7062d8732b280e44f07723d2cfe3a72ceb5bf003e71965a5ff

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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