Linear Algebra
Exercise LA-007
local source supported. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- finite complex matrices and vectors
- |left> and |right> are computational-basis states
- basis ket is a Kronecker delta at its index
- matrix-vector action uses the standard finite sum
Question
In a finite complex matrix backend, acting with an operator on a computational-basis state (a vector with a single 1 at one position and 0 elsewhere) returns the corresponding column of the operator. Using only this fact and the linearity of matrix-vector multiplication, prove that acting with an operator A on the two-term superposition a*|left> + b*|right>, where |left> and |right> are two basis states, gives a*(column left of A) + b*(column right of A), and that the amplitude read at output row k equals a*A[k,left] + b*A[k,right]. Explain why this means a block-encoding or state-preparation witness never needs to reconstruct the whole matrix-vector product: only two named columns, or two named entries, are ever required.
Hint: mathematical route
A(a|left>+b|right>) = a*col(left)+b*col(right) and row-k amplitude = a*A[k,left]+b*A[k,right], by linearity of mulVec on basis kets.
- Acting on a single basis ket returns the corresponding matrix column.
- By linearity the action on a two-term superposition is the weighted sum of the two columns.
- Reading row k yields the scalar amplitude a*A[k,left] + b*A[k,right].
Reference solution
Matrix-vector multiplication is linear in the vector argument: for scalars a, b and vectors u, w we have A(a*u + b*w) = a*(A u) + b*(A w), and A(c*u) = c*(A u). Apply this with u = |left> and w = |right>. By the basis-column fact, A|left> is exactly the 'left' column of A and A|right> is exactly the 'right' column of A. Therefore A(a*|left> + b*|right>) = a*(A|left>) + b*(A|right>) = a*(column left of A) + b*(column right of A). Reading the k-th coordinate of both sides and using that the k-th coordinate of the 'j' column of A is the entry A[k,j], the output amplitude at row k is a*A[k,left] + b*A[k,right]. Consequently, to certify what an operator does to any two-term superposition it suffices to inspect the two named columns (vector form) or, for a single output amplitude, just the two named matrix entries (scalar form). No sum over all basis states or full reconstruction of the matrix-vector product is needed; the sparsity of the input collapses the computation to exactly the terms whose input amplitude is nonzero. This is why finite preparation and block-encoding witnesses are stated and checked column-wise or entry-wise rather than by rebuilding a dense product.
Assessment rubric
- States/uses linearity of matrix-vector action in the vector argument (additivity and scalar homogeneity). (1 weight)
- Identifies A on a basis ket with the corresponding column and derives the vector-form result a*col(left)+b*col(right). (1 weight)
- Reads coordinate k to get the scalar amplitude a*A[k,left]+b*A[k,right]. (1 weight)
- Explains the practical consequence: only two columns/entries are needed, no full product reconstruction. (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/ConcreteSemantics.lean
complete declarations applyVec_basisKet (lines 70-74), applyVec_twoBasisSuperposition (lines 79-88), applyVec_twoBasisSuperposition_apply (lines 93-100)
Source SHA-256:454c0c5e215ca197c5883bedf74882f392d259c7afeadc63912230437698ebe5· MIT (repository LICENSE)
Contract: f9e0dbca29830768aac6c3aaf82a28b5b7edaff3d6938ee697b32acfea46faa9
Item digest: f10f3a23733971a2aa0b150a90124936ed6d12d8b403eff4b77380607f85064c
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.