Exercise BE-102

Clean work guarantees the correct sum, unchanged row and return to zero. This concrete reversible circuit preserves row and entering work even on dirty inputs, whose arithmetic sum can—but need not—be wrong.

1. The clean-action theorem certifies the three-property output conjunction when the entering carry-scratch bit is zero; its converse is not a dirty-input failure theorem.
2. The certified clean-branch address equals (loader(address)+row) mod8.
3. The row is unchanged on the clean branch; direct gate-target inspection gives the stronger all-input row preservation for this witness.
4. The paired scratch toggles restore the entering work bit on all basis inputs, so a clean input returns zero and a dirty input returns one.
5. Dirty address3,row0,work1 retains a correct sum while dirty address1,row0,work1 produces6 instead of2; neither returns a known-zero work bit, and the full map is still reversible.

The clean-branch contract specifies three different properties of the same output: the address is overwritten by (loader(address)+row) mod 8, the row is unchanged, and the work bit ends at zero. The hypothesis work=0 is needed to guarantee that conjunction for every allowed input; it does not mean that every individual property must fail whenever work=1. In particular, the existing named clean-action theorem supplies only a sufficient clean-input contract. What actually happens outside it must be read from the program, not inferred by negating the hypothesis.

For this fixed circuit there is a stronger direct source-level fact: the row bits and the entering work bit are preserved on every basis input, clean or dirty. The loader flips only address bits 0 and 1. The first and third adder gates both toggle work bit 6 by the same product of row bit 3 and loaded address bit 0; between them only address bit 2 is changed, so these two work toggles cancel. No later gate targets work. No gate targets row wires 3,4,5 at all. Thus a dirty work bit returns as 1, not as 0: restoration to the stipulated clean state fails, but restoration to its entering value holds. Reversible borrowed-bit preservation and the known-zero clean-work promise are different interfaces.

Let v be loaded address bit 1 and d the entering work bit. Relative to the clean-input computation on the same address and row, the dirty-input trace differs by an extra toggle of address bit 2 precisely when d=1 and v=1. The second adder gate uses the scratch bit before the third gate restores it. All subsequent address updates have controls independent of address bit 2, so this extra toggle persists to the output. Consequently the arithmetic sum can be wrong, but need not be wrong on every dirty input.

Two exact basis examples distinguish the claims. Start with address3, row0, work1. The XOR3 loader produces address0; the dirty-work high-bit control has v=0, and the output is address0,row0,work1. The required sum is correct while the return-to-zero promise fails. Start instead with address1,row0,work1. The loader produces address2, whose bit1 is1; the output address is6 rather than the required2, with row0 and work1 unchanged. Thus dirty inputs can lose arithmetic correctness and always fail this known-zero restoration promise, while row preservation survives. The whole seven-wire map remains a reversible permutation on all basis inputs. With a known clean quantum input, linear extension of the clean-action map returns a factored |0> work register; preservation of basis labels alone must not be rephrased as a no-entanglement guarantee for arbitrary unknown dirty quantum inputs. These claims concern this finite witness, not an arbitrary-width adder or a new resource bound.

1. Identifies the carry-scratch use of work and the exact clean-input conjunction. Does not infer universal dirty-input failure merely from the clean theorem's missing hypothesis. (1 weight)
2. Separates correct address sum, unchanged row and known-zero work restoration. Derives unconditional row/input-work preservation for this actual circuit from its targets and paired work toggles. (1 weight)
3. Shows what can fail and what still holds for work=1, using a dirty input with correct sum and a dirty input with incorrect sum. Keeps borrowed-value preservation, return-to-zero, reversibility and arbitrary-input entanglement distinct. (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/BandedSparseAccessPrimitive.lean

  theorem primitiveAccess3_cleanAction (state : PrimitiveBasis 7) (workClean : state 6 = 0) : let output := primitiveAccess3BasisEquiv state; primitiveWord3 output 0 1 2 = ⟨((primitiveOffset3 (primitiveWord3 state 0 1 2)).val + (primitiveWord3 state 3 4 5).val) % 8, Nat.mod_lt _ (by decide)⟩ ∧ primitiveWord3 output 3 4 5 = primitiveWord3 state 3 4 5 ∧ output 6 = 0 (lines 48-57); theorem primitiveAccess3_preserves_row ... (lines 60-64); theorem primitiveAccess3_workspaceClean ... (lines 67-70)

  Source SHA-256: e4f35bfdd690445de12d5a7e6692b9ab86d1a096b9ed3f4d1a41e07b99181ca7 · MIT (repository LICENSE)

Contract: 17816324abe115e9fc8c77de7e26b26e39203b5466d8bf455c841cef553f71b9

Item digest: ae8623f2384d5350708cbe0dba53b4b300a965e6f3eb80d4bfde18e331df7839

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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

{ "predecessor_item_digest": "ccce000279db59f25b24bf92dc5768b74e732a097f2cb4da9eb98c4851df6165", "predecessor_key": "qcb-core-be-102", "repair_record": "shared/repairs/be-102-dirty-work-boundary-repair.json", "repair_record_digest": "e2392b76510772802787bd9cfa7f7d814a04db9173e58655f4fccf2c7a789238", "review_record": "reports/textbook-v1/repairs/be-102-dirty-work-boundary-repair-review.json", "review_digest": "1be83d6da782444784c317644691597b54806047ece8ae56702a35ff5544143b" }