Linear Algebra
Exercise LA-012
local source supported. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- canonicalization follows the backward min(l, 2*m') recurrence
- the terminal bond of a scalar-boundary chain is dimension one
- each core emits one bit of dimension 2
- bond dimensions are the dependent inner indices, not padded
Question
A finite real tensor train is right-canonicalized by sweeping from the terminal bond backward, replacing each core by one with orthonormal rows while absorbing a residual into the preceding core. The active left bond dimension produced at each core obeys the exact backward recurrence: the new left bond is the minimum of (the current left bond) and (twice the next active bond). Using only this recurrence and the fact that the sweep never enlarges any bond, prove two boundary facts: (a) after canonicalization every core's left bond is at most its original left bond AND at most twice its next active bond; and (b) for a scalar-boundary chain whose terminal bond is forced to dimension one, the active bond immediately before the terminal bond is at most two. Explain where the factor of two comes from.
Hint: mathematical route
The backward recurrence new left bond = min(l, 2m') gives head_bound (l' <= l and l' <= 2m') and last_bond_le_two (penultimate bond <= 2 when the terminal bond is 1).
- The new left bond equals min(original left bond, twice the next active bond), from reshaping the emitted bit with the right bond and factorizing.
- Therefore the new left bond is at most the original left bond and at most twice the next active bond simultaneously.
- For a length-one scalar-boundary chain the bond before the dimension-one terminal bond is at most two.
Reference solution
The factor of two comes from the physical bit each core emits: a core carries an emitted bit of dimension 2 together with its right bond, so when it is reshaped and factorized the inner (new left) dimension cannot exceed the number of columns of the reshaped bit/right-bond block, which is 2 times the right (next active) bond. The factorization also cannot increase the row count, so the new left bond cannot exceed the original left bond either. Hence the new left bond is at most the minimum of the original left bond and twice the next active bond, which is exactly the stated recurrence. (a) Reading the recurrence directly: new left bond = min(original left bond, 2 * next active bond) <= original left bond, and <= 2 * next active bond. Both inequalities hold simultaneously because the minimum of two quantities is at most each of them. So every canonicalized core's left bond is bounded by both its original left bound and twice its next active bond. (b) Consider a chain of length one over a scalar (dimension-one) terminal boundary: the single core's right/next active bond is the terminal bond, which is forced to be dimension one. Apply the bound from (a) to this core: its left bond is at most 2 times its next active bond = 2 * 1 = 2. Therefore the active bond immediately preceding a dimension-one terminal bond is at most two. Intuitively, once the chain has been squeezed down to a scalar output, the preceding bond can retain at most the two values the final emitted bit can distinguish, so its dimension cannot exceed two.
Assessment rubric
- Explains the factor of two as the emitted bit of dimension 2 multiplying the right/next-active bond (reshape column count). (1 weight)
- Derives (a): new left bond = min(original, 2*next) is at most each of the two quantities. (1 weight)
- Derives (b): for a length-one chain with terminal bond 1 the preceding bond is at most 2*1 = 2. (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 RankReduced (lines 51-55), exists_core_lq (lines 67-80), RankReduced.head_bound (lines 104-110), RankReduced.last_bond_le_two (lines 113-117), RankReduced.maxBond_le (lines 203-207)
Source SHA-256:b8d1eb0651708ac2496be306e2d4b6f3025f7ea4d35a8c6907de02b89d1d981f· MIT (repository LICENSE)
Contract: 80e75adc1df2a536fbaa3a2467e7a82f9e5bff05a0b15ce3874e93cdf6736123
Item digest: b53e888a9d2bde591363f2eb202ee553d7d833c9cfc4f8c52e0ce21427338a09
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.