Linear Algebra
Exercise LA-001
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 core is a real matrix with composite column index (bit of 2 values, right bond of r values)
- a thin factorization with orthonormal rows exists in flat coordinates
- columns reshaped by a fixed finite-product bijection of size 2r
- orthonormal rows means Q*Q-transpose = identity
Question
A single core of a finite real tensor train is a real matrix whose rows are indexed by the left bond and whose columns are indexed by a composite label: an ordered pair of an emitted bit (two values) and a right-bond index (r values). To factorize this core, one reshapes that composite column label into a single flat column label and then performs a thin factorization in the flat coordinates. Explain (a) why the reshaping is a genuine bijection and what the flat label's size is, (b) why performing the factorization in flat coordinates and then relabeling the result back by the inverse reshaping produces valid factors of the original core, and (c) why the row-orthonormality of the orthonormal factor is unaffected by the relabeling. State the resulting inner (new left-bond) dimension.
Hint: mathematical route
exists_core_lq reshapes a core's (Fin 2 x Fin r) column index to a flat Fin (2r) index via a bijection, applies thin LQ, and reindexes back; A = R*Q and Q*Q-transpose = 1 hold with inner dimension min(l, 2r).
- The composite (bit, right-bond) column label is bijective with a flat label of size 2r.
- Factorizing in flat coordinates and relabeling back reproduces the original core because column relabeling preserves entries and products.
- Row-orthonormality is preserved because the per-row-pair column sum is invariant under bijective reindexing; inner dimension is min(left bond, 2*right bond).
Reference solution
(a) The composite column label ranges over all ordered pairs (bit, right-bond index) with the bit taking 2 values and the right-bond index taking r values. The set of such pairs has exactly 2 times r elements, and there is a fixed bijection between it and the flat label set {0,...,2r-1}; reshaping is simply applying this bijection, so no column is lost, duplicated, or merged. The flat label therefore has size 2r. (b) A thin factorization in flat coordinates writes the reshaped core as R times Q where Q has orthonormal rows. Relabeling the columns of Q back by the inverse bijection permutes/renames columns without changing any entry, so the matrix product R times (relabeled Q) reproduces the original core entry by entry: for each original column (bit, j) the entry equals the flat-coordinate entry at the image label, which the factorization already matches. Hence R and the relabeled Q are valid factors of the original core. (c) Row-orthonormality is the statement that Q times Q-transpose equals the identity, i.e. each pair of rows has the prescribed inner product summed over columns. Relabeling columns by a bijection only reorders the terms of that per-row-pair sum, and a finite sum is invariant under reindexing by a bijection, so the row-Gram matrix is unchanged; the relabeled Q still has orthonormal rows. The inner (new left-bond) dimension is the minimum of the original left bond and 2r, i.e. min(left bond, 2 * right bond).
Assessment rubric
- States the composite (bit, right-bond) label is in bijection with a flat label of size 2r (2 bit-values times r right indices). (1 weight)
- Explains that relabeling columns by the inverse bijection leaves entries unchanged, so R times the relabeled factor reproduces the original core. (1 weight)
- Explains row-orthonormality survives because a finite column sum is invariant under bijective reindexing; states inner dimension min(left bond, 2*right bond). (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 declaration exists_core_lq (lines 67-80) with Core (line 18) and slice (lines 20-21); the reshaping uses a finite-product bijection and sum-reindexing to recover A = R*Q and Q*Q-transpose = 1 with inner dimension min l (2*r)
Source SHA-256:b8d1eb0651708ac2496be306e2d4b6f3025f7ea4d35a8c6907de02b89d1d981f· MIT (repository LICENSE)
Contract: df0cde7e7f68e52d59b1e2539d365af3e79e65d6524f557c541f4fc39d7653c2
Item digest: f871c32a18b71fb5ea483f94e2941d10f0b34a1ea600577f1e392fdb2d0412c3
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.