Block Encoding
Exercise BE-003
nl bridge from inspected source. Explicit question version 2 with distinct contract-change review; the predecessor question is not equivalent current gold. Core, family and split are retained. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- Real orthogonal 2x2 matrices; target in (0,1) so s = sqrt(1-x^2) > 0 and the two witnesses are genuinely distinct
- Clean block is the single embedded entry U(0,0)
- cleanBlockBy embed U (row,col) = U(embed row, embed col); here embed sends the system index to total index 0
- Garbage/failure branch = entries off the clean embedding
This question explicitly revises its historical contract. A Lean companion must bind the current contract hash, not the predecessor hash. This is one reserved core, not two exercises.
Question
Keep total dimension2, the single system index embedded at total index0, and real orthogonal matrices. The inherited explicit assumption is 0<x<1. The historical question instead wrote 0<|x|<1: identify this range discrepancy rather than silently replacing the inherited assumption. Under the standing positive range, refute the claim that target clean entry U(0,0)=x plus orthogonality determines U uniquely: exhibit and verify two distinct orthogonal2x2 completions. As a separately identified extension, assess whether the SAME formulas also work for negative x satisfying0<|x|<1, without calling those x admissible under the inherited positive premise. Specify which entries a clean-block certificate fixes, how orthogonality couples the remaining entries, and why reading only CLEAN outputs of every clean-basis input is equivalent information. Distinguish this projected action from specifying the full output vector. State precisely what nonuniqueness does and does not imply about completion families or implementation costs.
Hint: mathematical route
The inherited domain is0<x<1; the historical0<|x|<1 phrase is explicitly assessed, and the clean compression fixes U00 only. Rotation/reflection witnesses share U00=x and satisfy both Gram identities; they are distinct for s>0, with any negative-x extension explicitly outside the retained positive premise. Projected clean-basis action carries the same information as the clean block, not the full output vector; off-block completions and implementation resources are not uniquely determined.
- The inherited domain is0<x<1; the historical0<|x|<1 phrase is explicitly assessed, and the clean compression fixes U00 only.
- Rotation/reflection witnesses share U00=x and satisfy both Gram identities; they are distinct for s>0, with any negative-x extension explicitly outside the retained positive premise.
- Projected clean-basis action carries the same information as the clean block, not the full output vector; off-block completions and implementation resources are not uniquely determined.
Reference solution
Under the actual standing assumption0<x<1 let s=sqrt(1-x²)>0. Take U_rot=[[x,-s],[s,x]] and U_ref=[[x,s],[s,-x]]. Their clean entry is x. Each pair of columns has squared norms x²+s²=1 and cross product0: for U_rot it is -xs+sx; for U_ref it is xs-sx. Hence U_rot^T U_rot=U_ref^T U_ref=I2; square finite matrices with orthonormal columns are orthogonal, and direct row calculations also give U_rot U_rot^T=U_ref U_ref^T=I2. They differ at(0,1), since s>0; their determinants are+1 and-1. This refutes uniqueness under the inherited positive range.
The historical positive assumption and broader absolute-value wording are not identical domains. The displayed construction in fact depends only on|x|<1, so it separately extends to every negative x with0<|x|<1, using the positive real square root of1-x². This extension is not an override of the frozen positive assumption. At x0 the same two matrices are still distinct; at|x|1 the s-based off-diagonal distinctness argument degenerates and must not be used, though other completions may remain. These boundary observations do not change the requested interior domain.
The exact embedded compression fixes only U00=x. It fixes neither all of row0 nor all of column0, and off-clean entries are NOT independent arbitrary numbers: row/column norms and mutual orthogonality constrain them. In these witnesses the full first column even happens to coincide, while the second column can still have either orthogonal sign. In real dimension2 the completion set for a fixed interior x is finite (indeed the sign choices give four completions), so two witnesses do not prove an infinite family in this fixed setting. Larger spaces can have continuous freedoms, but no universal infinite-family statement is needed.
The source cleanBasisActionAmplitude applies U to an embedded basis input and reads only an embedded CLEAN output. Each such amplitude is exactly one clean-block entry; quantifying over all clean inputs/outputs is therefore equivalent to the projected block equality, as the complete bridge proof shows. It is not a certificate specifying the entire clean-input output vector or its leakage, nor is it intrinsically stronger information. Full-output action data would be a different contract.
A alone thus does not select a unique U, circuit, depth, ancilla layout or resource count. Different completions need not have proven different optimal costs, and even one fixed U can have artificially padded implementations. The abstract candidate records store resource/verification fields separately; their presence is not a new unitarity/circuit theorem. Real square-root witnesses above are mathematical real matrices, not claims that the rational scalar backend or a finite gate compiler implements them exactly for arbitrary x. No normalization, cleanup, success probability or resource synthesis follows from this nonuniqueness example.
Assessment rubric
- Uses the inherited positive range explicitly and diagnoses the historical absolute-value mismatch; verifies two distinct orthogonal completions and separately identifies the negative-x extension without overriding assumptions. (1 weight)
- Identifies U00 as the fixed compressed entry, with coupled rather than independently free off-block data; does not claim a continuous family for fixed real dimension2. (1 weight)
- Explains the clean-output-only action/block equivalence versus full-output data, and separates nonuniqueness from unproved cost, ancilla or circuit claims. (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/BlockEncodingClassics.lean
def cleanBlockBy 'U (embed row) (embed col)' (lines 38-42)
Source SHA-256:94ac6632924df0a49b1ebd99bb5d9ed69b2ea463ec527033f38bd73deeb1346a· MIT (repository LICENSE) - QuantumBlockEncoding/ConcreteSemantics.lean
theorem pointwiseProjection_iff_cleanBasisAction with comment 'any normalized orthogonal failure branch is additional unitarity evidence, not a different block-encoding contract' (lines 271-294)
Source SHA-256:454c0c5e215ca197c5883bedf74882f392d259c7afeadc63912230437698ebe5· MIT (repository LICENSE) - QuantumBlockEncoding/BlockEncoding.lean
structure OperatorBlockEncodingCandidate (lines 103-116); structure VerifiedOperatorBlockEncoding (lines 130-134)
Source SHA-256:fe06f75a29822e28ccdbfedfb0b0e87f90872620fae7aed359085fad8fae64b4· MIT (repository LICENSE)
Contract: baadc3b2b59d3b6326e8925e735674b8eccaca0961f4c46e6ae19e584febf7d9
Item digest: 8c485ecf49d7c1b766a12871fd960795482772086f9b9ee641a0ccc4bc7a51dc
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.
Question revision lineage
{ "question_version": 2, "predecessor_key": "qcb-core-be-003", "predecessor_item_digest": "a757beddff8a7a05762348e416f2e50a373efa53005468c33f43d4ea53b61de8", "predecessor_contract_hash": "44e0c8e158d38e93a29891a143cf773aecbf6f7aada292309b5f9c96e67ba1a8", "current_contract_hash": "baadc3b2b59d3b6326e8925e735674b8eccaca0961f4c46e6ae19e584febf7d9", "changed_contract_fields": [ "question" ], "repair_record": "shared/repairs/be-003-range-completion-question-successor.json", "repair_record_digest": "1abe381992540e8837f66bb19dd323b051b983b28595f23fd71ce10bcb1d09f3", "review_record": "reports/textbook-v1/repairs/be-003-range-completion-question-successor-review.json", "review_digest": "5bfffa84b0b4c2f0e4b59fcd87a71b1069fdfc18d1d7d16529800743c016036d", "equivalence_to_predecessor_claimed": false, "additional_core_count": 0 }