Stored Cost Refinement
Exercise LA-210
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
- Scalar-boundary chain; the Gram environment is a 1-by-1 stored matrix
- Reading a stored matrix entry is one row read plus one entry read
- The environment is already materialized before the boundary step; counts are exact-real, not finite-bit
- Original derivation from inspected local source; no fresh Lean verification
Question
Given the stored right-to-left Gram-environment computation of a scalar-boundary tensor-train chain (which returns a 1-by-1 stored environment), the stored norm is obtained by reading the single scalar entry of that environment and taking its exact square root. Prove that the norm computation's cost equals the Gram computation's cost plus exactly two reads and one square root on the appropriate counters, and hence that its summed total exceeds the Gram total by exactly three. Then state precisely what mathematical quantity the returned scalar equals and why charging only two reads and one square root is the correct marginal cost of the scalar boundary.
Hint: mathematical route
Prove the stored tensor-train norm costs the Gram cost plus exactly two reads and one square root (total +3), and equals the Euclidean norm of the represented vector.
- The norm reads the single environment entry (two reads) and applies one square root.
- Per counter the norm cost is the Gram cost plus two reads and one square root, so the total grows by exactly three.
- The returned scalar is the Euclidean norm, the square root of total squared contracted mass.
Reference solution
The norm is defined as: run the Gram computation to get the 1-by-1 environment E, read its entry E(0,0), and return the exact square root of that entry. Reading the entry of a stored matrix is a row read followed by an entry read, i.e. two reads; the square root is one square-root call. No other counter is touched. Therefore, counter by counter, the norm cost equals the Gram cost plus two on the read counter and plus one on the square-root counter, and is unchanged on the other six counters. Summing all eight counters, the norm total is the Gram total plus exactly 2 + 1 = 3. The returned scalar equals the square root of the sum over all computational-basis words of the squared contracted amplitude of the chain, i.e. the Euclidean norm of the vector the tensor train represents; equivalently it is the square root of the single top-left Gram entry, since the full Gram environment at the scalar boundary stores exactly that total squared mass. Charging only two reads and one square root is correct because the environment has already been fully materialized by the Gram computation, so the only additional work at the boundary is to look up the stored scalar and apply one exact-real square root; this is an exact-real operation count, not a finite-bit cost, and the heavy contraction work is all accounted inside the Gram stage.
Assessment rubric
- Identify the marginal operations as two reads (row then entry) and one square root (1 weight)
- Conclude the summed total exceeds the Gram total by exactly three (1 weight)
- State the scalar equals the Euclidean norm (square root of total squared mass) and justify the small marginal charge (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/StoredTensorTrainNorm.lean
norm118-121; norm_eq_sum129-131; norm_cost286-290; norm_total_cost_le293-302
Source SHA-256:60fa71fc821f7598f5df739b231f5b25cf1927824d2b028ef723f9ee04074011· MIT (repository LICENSE)
Contract: d088ce771664b3d673463cb525dbe533984f0d811c56545f9d6afe6a7588f429
Item digest: f7b3e31bd2ea7ed164adf59e8ce49b69f7a86494a8f7b0de784805f53bf9efcb
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.