Linear Algebra
Exercise LA-004
nl bridge from inspected source. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- system register has 2^n states
- a auxiliary qubits are used
- signal/ancilla register is high-order, system register is low-order
- flat index = signal * systemDim + system
Question
A block-encoding unitary represents an operator that acts on the 2^n states of an n-qubit system register, using a auxiliary qubits. (a) What is the dimension of the square matrix representing the full unitary, and why? (b) The full index is a flattened combination of a signal/ancilla register and the system register; state which register is treated as the high-order (most significant) part of the index and which as the low-order part. (c) If one instead keeps the two registers explicit as an ordered pair (signal, system) and reads off the sub-matrix for one fixed value of the signal register, how does that sub-matrix relate to the sub-matrix obtained by projecting the single flattened unitary onto the same signal branch?
Hint: mathematical route
A system-on-n-qubits candidate with a auxiliary qubits has a 2^(n+a) unitary; the signal register is high-order; the explicit product-register branch equals the flattened signal-system block projection.
- A system on n qubits with a auxiliary qubits yields a 2^(n+a)-dimensional unitary.
- The flat index places the signal register high-order and the system register low-order.
- The product-register branch and the flattened block projection are the identical matrix.
Reference solution
(a) The full unitary is a 2^(n+a) by 2^(n+a) matrix. The combined register has n + a qubits (n system qubits plus a auxiliary qubits), and a register of n+a qubits has 2^(n+a) basis states, so the unitary acting on all of them is a square matrix of that size. (b) The signal/ancilla register is the high-order (most significant) part of the flattened index and the system register is the low-order part; equivalently the flat index is signalIndex times (system dimension) plus systemIndex. (c) They are the same matrix. Taking the explicit product-register view of the flat unitary and then extracting the block for one fixed signal value yields exactly the same entries, position by position, as projecting the single flattened unitary onto that signal branch; the two descriptions are definitionally identical, so reasoning done in either view transfers to the other without any change of entries.
Assessment rubric
- States the full dimension is 2^(n+a) and justifies it by the n+a combined qubits. (1 weight)
- Identifies signal/ancilla as high-order and system as low-order in the flattened index. (1 weight)
- States the explicit product-register branch equals the flattened block projection entry-for-entry. (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/BlockEncoding.lean
declaration OperatorBlockEncodingCandidate with the dimension note (lines 97-116)
Source SHA-256:fe06f75a29822e28ccdbfedfb0b0e87f90872620fae7aed359085fad8fae64b4· MIT (repository LICENSE) - QuantumBlockEncoding/ConcreteSemantics.lean
declarations flatToProductRegister (lines 190-198), productRegisterBlockProjection (lines 201-204), productRegisterBlockProjection_flatToProductRegister (lines 210-217)
Source SHA-256:454c0c5e215ca197c5883bedf74882f392d259c7afeadc63912230437698ebe5· MIT (repository LICENSE)
Contract: 4d210c8afd68cbdf3466959eeb2e95763df5353f3d18f73eb39f3e64811e291a
Item digest: 33cc06733514e0836a461f03019dbbcf4881b1b6963dfe5207cb05932deb4106
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.