Oracle Composition
Exercise BE-101
local source supported. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- Slot values range over {0,...,7}, so the outer mod 8 never fires
- The loader is XOR with the fixed mask 3
- XOR with a constant mask toggles exactly the bits set in the mask
- The loader is realized by two X gates on the two low wires
Question
A reversible source-loader on three little-endian bits is defined by the rule that maps each slot value s in {0,...,7} to (s XOR 3) mod 8, i.e. it flips the two low-order bits of s. Prove that this loader is its own inverse (an involution) as a permutation of {0,...,7}, and give the explicit image list obtained by applying it to 0,1,2,3,4,5,6,7 in order. Explain why the involution property is exactly what lets the two bit-flip gates that realize it also undo it when applied a second time.
Hint: mathematical route
The three-bit source loader s |-> s XOR 3 is an involution with image list [3,2,1,0,7,6,5,4]; XOR-with-mask self-inversion is the circuit-level undoing of the two bit-flip gates.
- Because every slot value is below 8, (s XOR 3) mod 8 equals s XOR 3.
- XOR with the fixed mask 3 toggles bit 0 and bit 1 and fixes bit 2.
- Self-inverse: (s XOR 3) XOR 3 = s XOR (3 XOR 3) = s, so L is an involution and a bijection.
- Evaluating L on 0..7 yields the ordered image list [3,2,1,0,7,6,5,4].
- The two X gates implementing the mask are each self-inverse and commute, so a second pass applies 3 XOR 3 = 0 and restores every slot.
Reference solution
The loader is L(s) = (s XOR 3) mod 8. Since every s in {0,...,7} is below 8, the outer mod 8 is inert and L(s) = s XOR 3. Bitwise XOR with the fixed mask 3 (binary 011) toggles bit 0 and bit 1 and leaves bit 2 untouched. XOR with a fixed mask is self-inverse because XOR is associative and commutative with x XOR x = 0: L(L(s)) = (s XOR 3) XOR 3 = s XOR (3 XOR 3) = s XOR 0 = s, so L is an involution and in particular a bijection of the 8-element set. Applying L to 0..7 in order gives [3, 2, 1, 0, 7, 6, 5, 4]: 0->3, 1->2, 2->1, 3->0, 4->7, 5->6, 6->5, 7->4. Operationally the loader is implemented by two X (bit-flip) gates on wires 0 and 1; because each X is self-inverse and the two flips commute, running the same two gates again applies 3 XOR 3 = 0, returning every slot to its original value, which is the circuit-level statement of the involution.
Assessment rubric
- State L(s)=s XOR 3 (mod 8 inert for s<8) and that it toggles the two low bits, mask 3 = binary 011 (1 weight)
- Prove the involution L(L(s))=s using x XOR x=0 and associativity/commutativity of XOR, concluding L is a bijection (1 weight)
- Give the exact image list [3,2,1,0,7,6,5,4] and connect the involution to the two X gates undoing themselves on a second pass (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/BandedSparseAccessPrimitive.lean
def primitiveOffset3 (slot : Fin 8) : Fin 8 := ⟨(slot.val ^^^ 3) % 8, Nat.mod_lt _ (by decide)⟩ (lines 29-30); @[simp] theorem primitiveOffset3_table : List.ofFn primitiveOffset3 = [3, 2, 1, 0, 7, 6, 5, 4] := by native_decide (lines 32-34)
Source SHA-256:e4f35bfdd690445de12d5a7e6692b9ab86d1a096b9ed3f4d1a41e07b99181ca7· MIT (repository LICENSE)
Contract: 40e56f9aa65e5d4bbd165e35277a54b73c72e6dd2aa637fa7ee32c995fef3444
Item digest: c121d5a0d54af38e9206a89b7e5c8acbab4eca77fe5c2e3ef5dad9fc0267a2a1
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 5. This is not measured graph distance or model difficulty.