State Preparation
Exercise SP-011
nl bridge from inspected source. 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 physical bond register is padded strictly larger than the active bond, with active dimension greater than two
- the full terminal stage is required to be unitary
- terminal core sends inputs to a single clean output bond label carrying a 2-row emitted-bit block
- active columns are the occupied input bond labels; inactive columns are free completion data
Question
In the sequential bond construction with a padded physical bond register larger than the active bond, a tempting simplification is to demand that the terminal cleanup stage send EVERY padded input column (not just the active ones) into the single clean output label. Show by a dimension/orthogonality argument that for an active bond dimension greater than two this demand is incompatible with the stage being unitary, and state the correct restricted condition the library uses instead.
Hint: mathematical route
Terminal cleanup confines constrained columns to a two-dimensional clean-output span. Padded dimension greater than two forbids an all-column unitary condition, and active dimension greater than two forbids even its active-only variant; the library's supported factorization theorem is conditional, not a unitary-existence result.
- Each terminal-action column lies in the two-dimensional output span indexed by emitted bit and the clean bond label.
- Unitary columns are orthonormal, so requiring this action on more than two padded or active input columns is impossible.
- Active-only terminal equality plus zero inactive support yields a conditional clean state-action factorization. It does not prove unitarity or its feasibility, and cannot yield a unitary in the question's active-dimension-greater-than-two case.
Reference solution
Write D for the padded input bond dimension and k for the number of active input bond basis labels. The fresh input bit is zero, so the constrained columns of the stage U are indexed by (0,a). Requiring terminal cleanup confines each such column to the output subspace H spanned by (0,clean) and (1,clean), which has dimension two. If U is unitary, these columns must be orthonormal. Therefore no more than two columns can satisfy this action. An all-padded-column requirement is impossible whenever D > 2. In the question k > 2 and D > k, so this obstruction certainly applies. The library's step_terminalCore_of_supported instead assumes (1) v(p,a)=0 for every inactive label a and every prefix p, and (2) U(bit,b)(0,a)=terminalCore(clean,T)(bit,b)(a) only for active a. The inactive summands then vanish in step_apply, yielding step(U,v)(x,b)=0 when b differs from clean and sum_a T(lastBit(x),a)*v(prefix(x),a) when b=clean. This is a conditional state-action identity; it does not assume or prove that U is unitary or construct such a U. Crucially, under the stated k > 2 assumption, even the active-only condition is incompatible with unitarity: it still forces k > 2 orthonormal columns into H. Thus active-only restriction is not a feasible unitary remedy for this question's setting. A physically feasible terminal step of this form must also have k <= 2 and orthonormal prescribed active columns (equivalently the active columns of T have Gram identity); then those finitely many columns can be completed to a unitary on the full finite-dimensional stage space. This last linear-algebra existence observation is not a circuit synthesis or resource theorem. Without changing the stated k > 2 setting there is no such unitary terminal cleanup, and a correct answer must say so rather than claiming the support condition solves the dimension obstruction.
Assessment rubric
- Uses distinct symbols D and k for padded and active input dimensions and identifies the two-dimensional output span (bit,clean). The columns in question are the fresh-input-bit-zero columns (0,a). (1 weight)
- Uses unitarity to force column orthonormality and proves all-padded cleanup impossible for D > 2. (1 weight)
- States exactly the active-only column identity plus zero inactive-support condition, and derives clean output factorization as a conditional state-action result, not a unitary-existence result. (1 weight)
- Explicitly recognizes that k > 2 also makes active-only unitary cleanup impossible. Does not claim a feasible remedy under the unchanged assumptions; any discussion of feasible alternatives must disclose k <= 2 and the Gram/isometry condition, without a circuit-cost claim. (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 201-222: comment 'Requiring this terminal action on all padded input columns would be incompatible with unitarity for bond dimension greater than two.'; theorem step_terminalCore_of_supported (support : for all p a, not active a -> v (p,a) = 0) (cleanColumns : for all bit b a, active a -> U (bit,b) (0,a) = terminalCore clean T (bit,b) a) : step U v (x,b) = if b = clean then sum a, T (x (Fin.last n)) a * v (Fin.init x, a) else 0
Source SHA-256:ad4542b108d44f196f2a02f78e59b58f43d45b1e890709cf4c22e1222805d5c5· MIT (repository LICENSE)
Contract: ccf6c506bc06c94a4aba979176d9cab93c866f1a7a5173a60d7c5d5e74047cb7
Item digest: 3dc8ebd018ba2a658d973683c272426bb6cf72ff07f489e20ed26fdb8a249818
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.
Answer revision lineage
{ "predecessor_item_digest": "8e29ce90772af81328f7d4b8e817f6183b46c52d96801e394ac4287c4be24a6f", "predecessor_key": "qcb-core-sp-011", "repair_record": "shared/repairs/sp-011-terminal-feasibility-repair.json", "repair_record_digest": "dbc81770f93ebf540ba98fa159e7b3552d4722fa04143ffd78163c75aa64457d", "review_record": "reports/textbook-v1/repairs/sp-011-terminal-feasibility-repair-review.json", "review_digest": "26456a1e859051ac81eaa8a067abf7e48f04d6c643527c237aa7023d01423710" }