Linear Algebra
Exercise LA-010
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
- the original core is right-canonical (orthonormal rows before padding)
- padding appends zero outputs beyond the active rank
- active clean-input columns are indexed by the original ranks
- column orthonormality is the conjugate-transpose-times-matrix Gram identity
Question
When embedding a right-canonical tensor-train core into a larger fixed physical register by zero-padding its outputs, one claims the active clean-input columns remain orthonormal and that right-multiplication of the boundary stays mass-preserving. A reviewer argues: 'the padded core still satisfies core times core-transpose equals the identity on the physical register, so its rows are orthonormal and nothing changes'. Show by an explicit small example that the reviewer's blanket claim is false: padding generally destroys the ROW orthonormality relation even though it preserves the COLUMN orthonormality of the active clean-input columns. State precisely which relation survives padding and which does not, and why only the surviving one is used.
Hint: mathematical route
Zero-padding a right-canonical core preserves active clean-input column orthonormality (paddedCore_active_isometry) but destroys physical-register row orthonormality, since padded rows are zero (paddedCore_inactive_output).
- Padding appends identically-zero output rows beyond the active rank.
- A matrix with a zero row cannot satisfy row-orthonormality (matrix*transpose = I).
- The active clean-input columns still form an orthonormal (identity Gram) family after padding.
Reference solution
Take the simplest nontrivial case: a core whose matrix, after fixing the emitted bit, acts as the 1-by-1 identity (its single active row/column is the scalar 1), and pad its output into a physical register of dimension 2 by appending a zero output row. Writing the padded clean-input column as the 2-component vector (1, 0): the column relation (conjugate-transpose times itself) gives (1,0).(1,0) = 1, so the single active clean-input column is still a unit column orthonormal to the (absent) others. But the row relation (matrix times its own transpose on the physical register) now has rows (1,0) and (0,0): the second row is the zero vector, so the matrix-times-transpose is diag(1,0), NOT the 2-by-2 identity. Hence padding breaks 'rows orthonormal' (core*core-transpose = I fails) while keeping 'active clean-input columns orthonormal' (the column Gram matrix on active indices stays the identity). This is a general phenomenon: zero-padding adds all-zero output rows, and a matrix with a zero row can never satisfy matrix*matrix-transpose = I (that identity forces every row to have unit norm). What survives is the column isometry restricted to the active clean-input labels, because the extra padded output rows are identically zero and contribute nothing to the column inner products. The library therefore states the preserved property as orthonormality of the active clean-input columns after embedding, and uses only that; the naive 'rows stay orthonormal on the physical register' claim is false and is correctly avoided.
Assessment rubric
- Gives a concrete small padded example (e.g. active block = [1], padded column (1,0) in a size-2 register). (1 weight)
- Shows the row relation fails: a zero padded row makes core*core-transpose = diag(1,0) != I. (1 weight)
- Shows the active-column relation survives: the clean-input column Gram matrix is still the identity. (1 weight)
- States the general reason (a zero row cannot satisfy row-orthonormality) and that only the active-column isometry is used. (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/TensorTrainCanonical.lean
complete declarations paddedCore (lines 255-258), paddedCore_inactive_output (lines 260-262), complexCore_isometry (lines 215-226), paddedCore_active_isometry (lines 295-315)
Source SHA-256:b8d1eb0651708ac2496be306e2d4b6f3025f7ea4d35a8c6907de02b89d1d981f· MIT (repository LICENSE)
Contract: 6961857bbd9bce35efff6bde34f2f53f947d50b32aee022526fac75b195c149c
Item digest: 492aef4134070695970d651e98c5bf482a5c7d14719d34b8b92091a7a6178ff5
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.