Oracle Composition
Exercise BE-107
local source supported. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- Each diagonal block B_k is unitary on the shared target space
- The full operator is block-diagonal in the control index
- Off-diagonal blocks of a block-diagonal matrix are zero
- Unitarity means the conjugate transpose times the operator is the identity
Question
A controlled family of operators is placed block-diagonally: for each control value k there is a block B_k acting on the same target space, and the full operator is the block-diagonal matrix whose k-th diagonal block is B_k. Prove that if every block B_k is unitary then the whole block-diagonal operator is unitary, by showing how the conjugate transpose interacts with the block-diagonal structure and that the product collapses block-by-block to the identity.
Hint: mathematical route
A block-diagonal operator built from per-block unitaries is unitary: the conjugate transpose respects the block structure, multiplication is pointwise in the control index, and each block collapses to the identity.
- The conjugate transpose of a block-diagonal matrix is block-diagonal with each block replaced by its conjugate transpose.
- Off-diagonal compound entries vanish on both sides because distinct control values index different blocks.
- The product of two block-diagonal matrices multiplies blocks pointwise in the control index.
- Per-block unitarity gives star(B_k)*B_k = I for every k, so the block family is the constant identity.
- Block-diagonal of the all-identity family is the identity, so star(D)*D = I and D is unitary.
Reference solution
Let D = blockDiagonal(B) be the operator on the product index (target x control) whose (k,k) block is B_k and whose off-diagonal blocks are 0. First, the conjugate transpose commutes with the block-diagonal construction: star(D) is the block-diagonal operator whose k-th block is star(B_k). This is checked entrywise: for two compound indices with control parts kR and kC, if kR != kC the entry is 0 on both sides (a block-diagonal matrix has zero off-diagonal blocks, and so does its conjugate transpose), and if kR = kC the entry is the conjugate-transpose entry of the single block B_k. Hence star(D) = blockDiagonal(k -> star(B_k)). Next, the product of two block-diagonal matrices is block-diagonal with the blocks multiplied pointwise: star(D) * D = blockDiagonal(k -> star(B_k) * B_k). Now use the hypothesis: each B_k is unitary, so star(B_k) * B_k = I for every k. Therefore the family k -> star(B_k) * B_k is the constant identity family, and blockDiagonal of the all-identity family is the identity matrix on the whole product space. Thus star(D) * D = I, which is exactly unitarity of D. The proof uses only (1) that conjugate transpose respects the block structure, (2) that block-diagonal multiplication is pointwise in the control index, and (3) the per-block unitarity hypothesis; no relation between different control values is needed because distinct blocks never interact.
Assessment rubric
- Show the conjugate transpose of a block-diagonal matrix is block-diagonal with each block conjugate-transposed (off-diagonal blocks zero on both sides) (1 weight)
- Show the product of block-diagonal matrices multiplies blocks pointwise in the control index, giving blockDiagonal(k -> star(B_k)*B_k) (1 weight)
- Apply per-block unitarity star(B_k)*B_k = I to conclude the product is the identity, hence D is unitary; note distinct blocks never interact (1 weight)
Graph-grounded prerequisites
These are support/source anchors, not an automatically extracted theorem-dependency proof.
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.
Sources and provenance
- QuantumBlockEncoding/Robin/ComplexLCU.lean
theorem blockDiagonal_unitary {ι κ : Type*} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (blocks : κ → _root_.Matrix ι ι ℂ) (unitary : ∀ k, blocks k ∈ _root_.Matrix.unitaryGroup ι ℂ) : _root_.Matrix.blockDiagonal blocks ∈ _root_.Matrix.unitaryGroup (ι × κ) ℂ (lines 122-145)
Source SHA-256:aa51d33a6ca788b17879e1d88030b525f4f035c97d74588636ccf25f8c04b843· MIT (repository LICENSE)
Contract: c9d2d5f292003faafbed817adf2ef01df15a6ee701fbd771d1a0a100fa0934a4
Item digest: 1b36266ef6c6f4eed5fc5fd43aada972b13c343a97ddce568581c553671be494
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 5. This is not measured graph distance or model difficulty.