State Preparation
Exercise SP-003
local source supported. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- the train has scalar left and right boundaries (both dimension one) and real cores
- the sole numeric hypothesis is that the sum of squared contracted amplitudes is one
- right-canonical means every individual core has orthonormal rows
- amplitudes are read off by full contraction of the chain for each bit word
Question
A finite real tensor train with scalar (dimension-one) left and right boundaries defines its amplitudes by full contraction over all cores. Suppose the only hypothesis is that the sum of squared contracted amplitudes equals one. After right-canonicalization, what is guaranteed about (a) the new initial boundary vector and (b) each individual target amplitude, and what is deliberately NOT assumed?
Hint: mathematical route
Canonicalization derives a normalized initial boundary and exact amplitude recovery from only the sum-of-squares-one hypothesis, assuming no target-state equality.
- Canonicalization returns a right-canonical train and a residual initial vector while preserving every amplitude by an exact factorization.
- Under the hypothesis that the squared amplitudes sum to one, the residual initial vector is normalized.
- Each original amplitude is recovered as the contraction of the normalized initial vector against the canonical train, with no target-state equality assumed.
Reference solution
Right-canonicalization produces an exactly equivalent right-canonical train D (each core has orthonormal rows) together with a new initial boundary vector u such that: (a) u is normalized, the sum over a of u_a squared equals one; and (b) every original amplitude is recovered exactly by contracting u against D, namely amplitude(x) = sum over a of u_a times contract(D, x)_a. What is deliberately not assumed is any equality to a prescribed target state: the normalization of u and the amplitude-recovery identity are consequences derived solely from the single scalar hypothesis that the squared amplitudes sum to one, together with the exact factorization produced by canonicalization. The terminal bond stays dimension one. In other words, normalization and recovery are provable output promises of the construction, not extra side conditions imposed on the input.
Assessment rubric
- States that canonicalization yields a right-canonical train (orthonormal rows per core) plus a new initial boundary vector u. (1 weight)
- States that u is normalized (its squared entries sum to one). (1 weight)
- States that each original amplitude equals the contraction of u against the canonical train, and that the terminal bond stays dimension one. (1 weight)
- Emphasizes that no equality to a target state is assumed; normalization and recovery are derived from the single hypothesis sum of squared amplitudes = 1. (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 183-195: theorem exists_normalized_state (C : Chain n 1 1) (hC : (sum x : Word n, (contract C x 0 0) ^ 2) = 1) : exists l' u D, RightCanonical D and RankReduced C D and mass u = 1 and for all x, contract C x 0 0 = sum a, u a * contract D x a 0; and lines 172-178 exists_rightCanonical_normalized
Source SHA-256:b8d1eb0651708ac2496be306e2d4b6f3025f7ea4d35a8c6907de02b89d1d981f· MIT (repository LICENSE)
Contract: fe84af982ab601b542660b351a02c568ffa54ab92928cebc6f06e01897d59321
Item digest: c4a49ccae5572ff4bf896d73c30f37c0c0c3b4caa98488b2efd4171679e36f72
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.