State Preparation
Exercise SP-004
local source supported. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- the input train is normalized (chain mass one) with a scalar terminal bond
- canonicalization uses orthonormal-row (right-canonical) cores
- mass is the sum of squared entries of a real boundary vector
- vecMul v R denotes the row-vector action of the residual matrix on the boundary
Question
A normalized finite real tensor train with a scalar terminal bond is right-canonicalized from the terminal end inward, absorbing each residual matrix into the preceding core. After this process, where does the total squared mass of the state reside, and what are the dimensions of the two boundary bonds?
Hint: mathematical route
Right-canonicalization concentrates all squared mass in the residual initial boundary while leaving the terminal bond at dimension one.
- Canonicalization factors the chain as a residual initial matrix times a right-canonical train preserving every amplitude.
- Orthonormal-row cores compose to a mass-preserving map, so the chain mass equals the mass of the boundary pushed through the residual.
- For a normalized input the residual initial boundary is normalized, while the terminal bond stays dimension one.
Reference solution
Canonicalization factors the chain as a residual initial matrix R times a right-canonical train D. Every core of D has orthonormal rows, so D acts as a composition of row isometries that preserve the row-vector squared mass. Consequently the total squared mass of the original state equals the mass of the boundary vector after it is pushed through R: mass(vecMul v R) equals the chain mass. For a normalized input (chain mass one) the residual initial boundary is therefore itself normalized. The terminal bond stays exactly dimension one throughout, and the residual appears as a new initial boundary whose dimension is the reduced left rank. So after canonicalization all of the normalization is concentrated in the single residual initial boundary while the terminal bond is untouched at dimension one.
Assessment rubric
- States the factorization chain = residual initial matrix R times a right-canonical train D. (1 weight)
- Explains that orthonormal-row cores act as row isometries preserving squared mass, so the mass equals mass(vecMul v R). (1 weight)
- Concludes that for a normalized input the residual initial boundary is normalized (all mass concentrated there). (1 weight)
- States the terminal bond stays dimension one and the residual initial boundary has the reduced left-rank dimension. (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
lines 159-178: theorem residual_mass (C D R hD h v) : chainMass C v = mass (Matrix.vecMul v R); and theorem exists_rightCanonical_normalized (C : Chain n l 1) (v) (hv : chainMass C v = 1) : exists l' R D, RightCanonical D and RankReduced C D and (for all x, contract C x = R * contract D x) and mass (Matrix.vecMul v R) = 1
Source SHA-256:b8d1eb0651708ac2496be306e2d4b6f3025f7ea4d35a8c6907de02b89d1d981f· MIT (repository LICENSE)
Contract: cbbc481fefb93aaa840806bffbbaa512e93b8ec8258a274ddc6be7f6db1d9f23
Item digest: 1b31a5d5788641b5b7068c87fc829de70756a84e5d8acb6f2e049f0d12701aed
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.