Block Encoding
Exercise BE-009
local source supported. 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
- Rational matrix backend; support map c is a function on columns
- Reconstruction uses amp(col) = target(c(col), col)
- Column-sparse: at most one nonzero per column at the fixed row c(col)
- A zero amplitude column is the degenerate allowed case
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
Retain rational square matrices A indexed by Fin n and a column support function c:Fin n→Fin n, with amp(j)=A(c(j),j) and reconstruction R_c(A)(i,j)=amp(j) if i=c(j), else0. The inherited convention describes support at the FIXED row c(j). State and prove the exact support condition for R_c(A)=A. Then distinguish two claims: (a) for every matrix with at most one nonzero per column there EXISTS a suitable c giving reconstruction; (b) any previously fixed c reconstructs every such matrix. Assess the historical demand to refute claim(a) with a column containing TWO nonzeros: is that a valid counterexample under its premise? Prove or refute each claim in the stated finite square setting, including n0. Give a genuine one-sparse counterexample to claim(b) for a specified c, a separate two-nonzero limitation example, and a correctly reconstructed target with a zero column. State why arithmetic reconstruction alone is not a normalizer-one block-encoding or oracle/circuit certificate.
Hint: mathematical route
The fixed-c reconstruction is equivalent to off-support zero entries; suitable c exists for every finite square one-sparse matrix, while a mismatched fixed c can fail and a two-nonzero column is not a counterexample to the existential premise. Zero columns and correctly located single nonzeros reconstruct exactly, including the empty square case; this entrywise identity does not supply unitary normalization or oracle/circuit resources.
- The fixed-c reconstruction is equivalent to off-support zero entries; suitable c exists for every finite square one-sparse matrix, while a mismatched fixed c can fail and a two-nonzero column is not a counterexample to the existential premise.
- Zero columns and correctly located single nonzeros reconstruct exactly, including the empty square case; this entrywise identity does not supply unitary normalization or oracle/circuit resources.
Reference solution
Write hSupport:forall i,j,i≠c(j) implies A(i,j)=0. At i=c(j), R_c(A)(i,j)=A(c(j),j)=A(i,j); away from that row it is0, so hSupport proves equality. Conversely reconstruction equality forces every off-support entry to be0. Thus the support predicate is necessary and sufficient. The complete oneSparse_from_support proof supplies the forward implication by exactly this case split; oneSparseMatrix_entry_if supplies the formula.
For claim(a), if n>0 and a column has a nonzero entry, choose its unique nonzero row as c(j); uniqueness follows from at-most-one nonzero. If the column is zero, choose any row, say0. Then all off-support entries vanish and the reconstruction is exact. At n0 columns/rows are empty, c is the unique empty function and equality is vacuous. Thus the finite square existential reconstruction statement is TRUE. This is an existence/finite-choice fact, not an efficient method for finding a support oracle.
Claim(b) is false when c is fixed independently of A. Take n2,c(0)=0,c(1)=1 and A=[[0,0],[1,0]]. Each column has at most one nonzero, but A(1,0)=1 lies off c(0)=0. Both sampled amplitudes are0, so R_c(A)=0≠A. This is a genuine counterexample respecting the one-sparse premise; it violates the fixed-map hSupport condition.
The historical example D=[[1,0],[1,0]] has two nonzeros in column0. Whichever c(0) is chosen, one nonzero is off-support, so no map reconstructs D. But D violates the premise of claim(a), hence cannot refute it. It only demonstrates the limitation on non-one-sparse inputs. Finally B=[[0,0],[0,3]], with c0=0,c1=1, has amp0=0,amp1=3 and reconstructs exactly: the entire zero column is allowed. These examples retain rational entries; zero amplitudes need no choice of a distinguished nonzero row.
The reconstructed B has operator norm3, so this arithmetic equality is not a normalizer-one unitary compression. Normalization, unitary completion, reversible location-map implementation, amplitude loading, ancilla cleanup, finite-bit evaluation and resource costs are separate obligations; a support map function need not itself be injective or an already supplied reversible oracle. The empty case does not require selecting a row from an empty carrier because there are also no columns. No invalid two-nonzero refutation or quantum synthesis conclusion is retained.
Assessment rubric
- Proves the exact fixed-c off-support condition and distinguishes existential selection of c from an arbitrary preselected c; correctly handles n0. (1 weight)
- Proves the existential one-sparse reconstruction claim and gives a genuine one-sparse fixed-c failure; explicitly explains why a two-nonzero column violates, rather than refutes, the existential claim's premise. (1 weight)
- Gives the separate two-nonzero limitation and valid zero-column witness, while keeping arithmetic reconstruction separate from normalization/oracle/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 oneSparseMatrix (lines 123-125); theorem oneSparseMatrix_entry_if (lines 127-132); theorem oneSparse_from_support hypothesis 'row != c col -> A row col = 0' (lines 139-147); structure OneSparseCertificate (lines 155-170)
Source SHA-256:94ac6632924df0a49b1ebd99bb5d9ed69b2ea463ec527033f38bd73deeb1346a· MIT (repository LICENSE)
Contract: 2d6d1fc3dd956a6077b7f27dc77ca53cc22333f28a846d18e4782cffc5dd528c
Item digest: e79c6d96942d1f304fa93069a5e4c1a0d5badd81a22ee1381f6bf64c587886e2
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 2. This is not measured graph distance or model difficulty.
Question revision lineage
{ "question_version": 2, "predecessor_key": "qcb-core-be-009", "predecessor_item_digest": "81aa90c475f83c6c482f6e7f35e5c20125c17896170b3c3306ef5600c8c76dcb", "predecessor_contract_hash": "6659d3e45a3aa738998a147809356d44e0b5f688405bbe667a6d174f6f8ba117", "current_contract_hash": "2d6d1fc3dd956a6077b7f27dc77ca53cc22333f28a846d18e4782cffc5dd528c", "changed_contract_fields": [ "question" ], "repair_record": "shared/repairs/be-009-support-quantifiers-question-successor.json", "repair_record_digest": "cfbe91cf8fbd9eb42e104306deadc4eee9b263c0d2e7121bf7bea2122cb79fe7", "review_record": "reports/textbook-v1/repairs/be-009-support-quantifiers-question-successor-review.json", "review_digest": "37bcc63fbb2caf6ae7cfa1687981684e8fd71cf02ebae31306deea8faef2ffaa", "equivalence_to_predecessor_claimed": false, "additional_core_count": 0 }