Linear Algebra
Exercise LA-002
local source supported. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- A is a core emitting one bit of two values with a right-bond index
- R is a real matrix on the right-bond index
- a bit-slice fixes the emitted bit and leaves an ordinary left-by-right matrix
- absorption acts only on the right-bond coordinate
Question
During backward canonicalization of a finite real tensor train, a residual matrix R (left over from factorizing a later core) must be absorbed into the right bond of the preceding core A, where A emits one bit of two possible values and has a right-bond index. The absorption produces a new core whose entry at left index a and composite column (bit, j) is the sum over the old right-bond index b of A at (a, bit, b) times R at (b, j). Explain in matrix-slice terms what this absorption does to each of the two emitted-bit branches of A, and justify why it does not mix the two bit branches together. State the single slice identity that captures this.
Hint: mathematical route
absorb A R contracts R into the right bond of A; absorb_slice shows slice(absorb A R, bit) = slice(A, bit) * R, so absorption is per-bit right multiplication that never mixes emitted-bit branches.
- Absorption of R right-multiplies each fixed-bit slice of A by R.
- Formally, slice(absorb A R, bit) = slice(A, bit) * R for each bit value.
- No bit branch is mixed because the contraction sum ranges only over the right-bond index and the emitted bit passes through unchanged.
Reference solution
View the core A, with the emitted bit fixed to a value, as an ordinary matrix called the bit-slice of A for that bit value: its rows are indexed by the left bond and its columns by the right bond. The absorption of R multiplies each such bit-slice on the right by R: the bit-value-0 slice of the absorbed core is the bit-value-0 slice of A times R, and the bit-value-1 slice of the absorbed core is the bit-value-1 slice of A times R. In other words absorption is just an independent right matrix multiplication performed within each emitted-bit branch. It cannot mix the two branches because the defining sum runs only over the old right-bond index b and carries the emitted bit through unchanged on both sides: the bit label of an output column equals the bit label fed in, and R acts only on the right-bond coordinate, never on the bit coordinate. The single identity that captures this is: the bit-b slice of (absorb A R) equals (the bit-b slice of A) times R, for each bit value b. This is why absorption changes bond dimensions on the right while preserving the bit structure the core emits.
Assessment rubric
- Describes absorption as right-multiplying each fixed-bit slice of A by R. (1 weight)
- States the slice identity: slice(absorb A R, b) = slice(A, b) * R for each bit value b. (1 weight)
- Explains no bit-mixing: the sum is only over the right-bond index and the emitted bit is carried through unchanged. (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 absorb (lines 58-60) and absorb_slice (lines 62-64), with slice (lines 20-21) and Core (line 18)
Source SHA-256:b8d1eb0651708ac2496be306e2d4b6f3025f7ea4d35a8c6907de02b89d1d981f· MIT (repository LICENSE)
Contract: 2201ea71c0c13fc5b258c8f0b308d77e98e6e5202b3e2eb52faf150084f4cf93
Item digest: ca7a9fcd324216a1144307b9d48138420f5a9609c644b95f81d80c8ccc438408
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.