Exercise BE-119

The ten named oracle-call labels fix exact printed order and length but are not interpreted matrices. No matrix, inverse/cleanup, unitarity or block-correctness assertion follows from the transcript or its length theorem. SWAP is a string label here; a separate executable object requires its own semantics/composition bridge. Visible backend total13 and effective projection10=declared9+visible padded0+trailing1 differ from the full internal-oracle pure-workspace budget6; an expanded physical footprint is not certified by these bookkeeping facts.

1. The ten named oracle-call labels fix exact printed order and length but are not interpreted matrices.
2. No matrix, inverse/cleanup, unitarity or block-correctness assertion follows from the transcript or its length theorem.
3. SWAP is a string label here; a separate executable object requires its own semantics/composition bridge.
4. Visible backend total13 and effective projection10=declared9+visible padded0+trailing1 differ from the full internal-oracle pure-workspace budget6; an expanded physical footprint is not certified by these bookkeeping facts.

The exact source-ordered list is [H_W^(kappa),U_indic,O_DT^S,Ry_boundary,O_DT^BS,U_indic^dagger,O_f,SWAP(two n-qubit registers; paper label only),(O_D^BS)^dagger,(H_W^(kappa))^dagger]. The list definition and length theorem fix these identities/order and length10 only. Every item is Gate.oracleCall with a string, not an interpreted matrix/primitive program. A dagger-looking label does not establish inverse semantics; the transcript alone proves neither unitarity, cleanup, a projected target block nor an oracle resource implementation.

The SWAP label is especially explicit: naming a swap between two registers does not execute its wire action here. A separate SourceBaseline module supplies a three-pair logical swap fragment [(0,3),(1,4),(2,5)] and associated definitions, but that separate object is not imported as matrix correctness of this string transcript by its name. Replacing the label with a physical circuit, composing its matrices and proving the full ten-block action require separate bridges; one must not infer them from the transcript's list equality.

The visible partition sums to5+1+3+0+3+1=13. Removing the3 system wires leaves10 non-system backend wires for the clean projection. The layout's declared signal count is9=5+1+3, and effective10=declared9+paddedOD0+trailing1. This matches the source's complete effective-signal layout bridge. It is dimension/bookkeeping arithmetic, not a proof that the non-system outputs are clean after execution or that their projection encodes the desired block.

Visible pure ancillas in this partition are paddedOD0+trailing1=1. The theorem-level layout/resource field is2n=6 at n3. Source documentation explicitly says that full pure-ancilla budget also includes internal sparse-access/oracle workspace, unlike the narrower visible ket partition. Thus the three facts 'visible13', 'declared signal9/effective10' and 'theorem pure budget6' refer to different scopes. The historical phrase 'total13 physical qubits' is unsupported if meant to include all internal implementation workspace; the exact theorem establishes the visible backend total, not that expanded physical upper bound. This is a scope obstruction, not a proof that an optimized physical implementation necessarily needs more than13 wires.

No exact fully expanded footprint follows from these fields alone. One cannot simply add system3+signal9+pure6 as disjoint simultaneously live registers, nor declare6-1=5 additional physical wires or add that to13 without overlap/lifetime/subcircuit allocation evidence. A budget is not a tight minimality theorem. Uninterpreted oracle labels can stand for implementations with different workspace; even padding a hidden implementation would leave this list unchanged. Cleanup and reuse would need actual semantic proofs, and a zero visible padded register does not make internal oracle work free. Conversely the arithmetic bridge does not assert a success probability, normalizer, finite-bit gate cost or circuit-resource certification. The initial assumption that SWAP semantics live elsewhere remains intact, but those semantics and the whole source-paper resource theorem are not freshly verified here.

1. Gives the exact ten-label order/length and separates strings from matrices, inverse/cleanup/unitarity/block correctness and resources. (1 weight)
2. Explains label-only SWAP and why a separate executable fragment needs a semantic/composition bridge rather than transfer by name. (1 weight)
3. Computes visible13, declared9 and effective10=9+0+1; distinguishes visible pure1 from theorem full2n=6 budget and explicitly assesses the old unqualified physical-total claim. (1 weight)
4. Does not manufacture a fully expanded total by adding/subtracting different-scope budget fields; leaves internal allocation, cleanup, normalization and gate/finite-bit resources as separate obligations. (1 weight)

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.

Read the Lean track and existing diagnostic warmups

• QuantumBlockEncoding/RobinEvolution.lean

  def warmRobinSourceCircuit : Circuit := [ Gate.oracleCall "H_W^(kappa)" , Gate.oracleCall "U_indic" , ... , Gate.oracleCall "SWAP(two n-qubit registers; paper label only)" , ... ] (lines 108-119); theorem warmRobinSourceLayout_spec : systemQubits = 3 ∧ signalQubits = 9 ∧ pureAncillas = 6 (lines 152-156); theorem warmRobinEffectiveSignalQubits_eq : GHL2025.effectiveRobinSignalQubits warmRobinParameters = 10 (lines 174-177)

  Source SHA-256: 8673572458ff260cf35d6cfce60ffcc52b5b2be721671b3171919e32d0b73a37 · MIT (repository LICENSE)

Contract: 73c770b750b75e2d669bcff4625dd1d3827fffe3a6532d704fab0a3c072a115a

Item digest: 9b0481fca1bab9937c5b104f59ffe062811391ebf1f4d70e20a2d46b5d3554f9

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

Authored support steps: 4. This is not measured graph distance or model difficulty.

{ "question_version": 2, "predecessor_key": "qcb-core-be-119", "predecessor_item_digest": "9861d3807794ab3a410205c3d90e220174973ab60491d738ba200ce0de215506", "predecessor_contract_hash": "4d00d5fa56caf609041bdfb2399f6cba6567cbd92c4e5d42725303b60e962807", "current_contract_hash": "73c770b750b75e2d669bcff4625dd1d3827fffe3a6532d704fab0a3c072a115a", "changed_contract_fields": [ "question" ], "repair_record": "shared/repairs/be-119-visible-workspace-question-successor.json", "repair_record_digest": "84404045bdb48551016b30c2f17988781d1137b5c9f1b8ace89c5879a3d3c861", "review_record": "reports/textbook-v1/repairs/be-119-visible-workspace-question-successor-review.json", "review_digest": "b26d9632075945d70f62d9891e06e315f17ed837eb754f59257a1e918f5bcfd6", "equivalence_to_predecessor_claimed": false, "additional_core_count": 0 }