Sparse Stencil Algebra
Exercise LA-020
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
- Finite-dimensional complex matrices; ordinary conjugate transpose
- All declared products have compatible dimensions
- Tensor factors ordered as written; stencil offsets are ordinary integers, not modular wrapping
- Original derivation from inspected local source; no fresh Lean verification
Question
A finite row stencil is a list of offset/coefficient pairs. Its matrix entry at row i and column j is the sum of coefficients of every pair with i+offset=j; no modular wrapping is used. Prove that merging repeated offsets by summing their coefficients leaves every matrix entry unchanged. Use the pairs (1,2),(1,-2),(-1,3) to show why list width and the number of nonzero matrix entries need not agree.
Hint: mathematical route
A finite row stencil is a list of offset/coefficient pairs. Its matrix entry at row i and column j is the sum of coefficients of every pair with i+offset=j; no modular wrapping is used. Prove that merging repeated offsets by summing their coefficients leaves every matrix entry unchanged. Use the pairs (1,2),(1,-2),(-1,3) to show why list width and the number of nonzero matrix entries need not agree.
- For fixed i,j, only pairs with the single matching integer offset contribute.
- Regroup a finite scalar sum by equal offsets to preserve all entries.
- Evaluate the cancellation example and separately check the finite-grid boundary.
Reference solution
Fix i,j. Every pair contributes its coefficient if its offset equals j-i and contributes zero otherwise. Group the finite sum by equal offsets; associativity and commutativity of scalar addition preserve the sum. Replacing each group by a single pair whose coefficient is that group sum therefore gives exactly the same entry for this arbitrary i,j, hence the same matrix. In the example the offset1 coefficient is2-2=0, while the offset-1 coefficient is3. Thus the entry at j=i+1 vanishes and the entry at j=i-1 equals3 if that column lies in the finite grid. The original list has three pairs, its merged list can have two pairs including a zero, and it has at most one nonzero matrix entry in a row; at a left boundary even that entry may disappear because j=i-1 is outside the grid. An access permutation or sparse-oracle cost cannot be inferred solely from the unmerged list length. This proof uses the stated additive matrix semantics, not a claim that arbitrary loaders with collided labels are automatically reversible.
Assessment rubric
- Prove entrywise invariance including repeated offsets (1 weight)
- Compute cancellation and remaining coefficient3 (1 weight)
- Distinguish list count, actual support and boundary truncation without claiming free access (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/RobinMatrix.lean
stencilRowCoeff15-26; buildRobinMatrix50-63
Source SHA-256:e957b6a5961ad2c22cfd154f17cbbec3e7668027b2f526d9f762798eb1c50038· MIT (repository LICENSE)
Contract: bb231c6c4dc551545d97fe1e0fe40342ee76634409cce46979e1ca00e3321185
Item digest: af12f58eabab10496249efa91b5f940edea14c74f6121a7b860ae69e321d3fc6
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.