State Preparation
Exercise SP-002
local source supported. Additive answer successor with distinct content-bound review; historical rejected answer retained only for audit. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- the stage is a genuine matrix-vector action on the fresh-bit-and-bond register, followed only by basis regrouping
- no claim is made that the stage's clean columns implement any particular tensor core
- the fresh output bit is appended at the highest wire; already-emitted bits are passive
- amplitude mass is the sum of star(amplitude) times amplitude over all basis labels
Question
A sequential bond-dimension construction prepares a state one output bit at a time: each stage acts on a freshly introduced bit set to zero together with the current bond register, appending the new bit at the highest wire while previously emitted bits stay passive. (i) Which input columns of a stage's local matrix can actually influence an emitted amplitude, and (ii) does introducing the fresh zero bit amount to a postselection or measurement?
Hint: mathematical route
Only clean fresh-bit-zero columns drive the emitted state, and introducing the fresh zero bit is norm-preserving rather than a postselection.
- The fresh bit starts in zero, so after padding only the fresh-bit-input-zero columns of the stage multiply nonzero prior amplitudes.
- The emitted amplitude collapses to a sum over the prior bond label of clean-column entries times prior amplitudes; other columns never contribute.
- Adding the zero bit leaves the total squared-modulus mass unchanged, so it is not a postselection or measurement.
Reference solution
(i) Let x denote the full emitted bit string after this stage, let c be its newly appended highest-wire bit, let p be the previous prefix obtained by removing that last bit, let b be the output bond label, and let a range over the prior input bond labels. The emitted amplitude is step(U,v)(x,b) = sum_a U((c,b),(0,a)) * v(p,a). The fresh input bit is fixed to zero, so the fresh-bit-input-1 columns multiply zero and cannot affect this clean-input action. The output bond b is free; only the prior bond a is summed. These unused columns are completion data not determined by the clean-input action, but they are not arbitrary if an additional admissibility condition such as unitarity is imposed. (ii) For the padding operation alone, freshZero(v)(p,(c,a)) is v(p,a) when c=0 and zero when c=1. Summing conjugate(amplitude) times amplitude over p,c,a therefore gives exactly the prior sum over p,a. This introduces a fresh zero register deterministically, with no measurement, discarded outcome weight, postselection or renormalization. Norm preservation of this padding does not by itself assert norm preservation of an arbitrary full stage matrix U; the latter requires an appropriate condition such as unitarity.
Assessment rubric
- Identifies that only fresh-bit-input-0 columns affect the clean-input action; fresh-bit-input-1 columns are irrelevant to that action, not unconstrained under additional matrix admissibility requirements. (1 weight)
- States the collapsed amplitude with free output bond b and summed input bond a: sum_a U((c,b),(0,a))*v(p,a), with p the old prefix and c the newly appended highest-wire bit. (1 weight)
- Shows that fresh-zero padding preserves total squared-modulus mass by the fresh-bit 0/1 sum; does not claim arbitrary U is norm preserving. (1 weight)
- Concludes the padding is deterministic register enlargement, not postselection or measurement, with no discarded weight or renormalization. (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/SequentialBondPreparation.lean
lines 39-68: def freshZero v := fun x => if x.2.1 = 0 then v (x.1, x.2.2) else 0; noncomputable def step U v := fun x => ((liftStage n U).mulVec (freshZero v)) (Fin.init x.1, (x.1 (Fin.last n), x.2)); theorem step_apply : step U v (x, b) = sum a, U (x (Fin.last n), b) (0, a) * v (Fin.init x, a); and lines 302-306 theorem amplitudeMass_freshZero : amplitudeMass (freshZero v) = amplitudeMass v
Source SHA-256:ad4542b108d44f196f2a02f78e59b58f43d45b1e890709cf4c22e1222805d5c5· MIT (repository LICENSE)
Contract: dbada4a38d51afaacc05de7b54b9b3d1a802bd1c1f642f2e072d10ded5d7c2e2
Item digest: 913146f35e58a18dbdca2df520ed09bfef9b31fc3bddfaf331881d33a6cb06bf
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.
Answer revision lineage
{ "predecessor_item_digest": "7f1b2a1988e00771f6ae01653a655d04982f664f22fab24482075424eb8cbed5", "predecessor_key": "qcb-core-sp-002", "repair_record": "shared/repairs/sp-002-index-repair.json", "repair_record_digest": "427b454740badec4b182fabaef2468f74c2a27c2779f396d2541a520136453aa", "review_record": "reports/textbook-v1/repairs/sp-002-index-repair-review.json", "review_digest": "86ea63ca682f4098c9fd71863a65a6f6f3f957c28e20d3d5fa9ded1f06195b61" }