Reversible Classical
Exercise LA-017
nl bridge from inspected source. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- Finite-dimensional complex Hilbert spaces unless real amplitudes are explicitly specified
- All basis/register permutations are fixed and applied to both input and output
- Column-vector action; Euclidean induced operator norm for norm claims
- Source inspection only; no fresh formal verification
Question
A reversible gate flips a target bit exactly when two control bits are both1. Assume each control wire is distinct from the target, but allow the two control wires to coincide. Prove the gate is its own inverse and explain what it reduces to when the controls coincide.
Hint: mathematical route
A reversible gate flips a target bit exactly when two control bits are both1. Assume each control wire is distinct from the target, but allow the two control wires to coincide. Prove the gate is its own inverse and explain what it reduces to when the controls coincide.
- Separate inactive and active control cases.
- Active control values survive the target flip by wire distinctness.
- Two target flips cancel; coincident controls collapse to a single predicate.
Reference solution
If the control predicate is false, the gate leaves the whole bit string unchanged, so a second application also does nothing. If true, it flips only the target; each control remains1 because neither control is the target. Thus the predicate remains true for the second application, which flips the target back. All other bits stay fixed, proving involution. If the two controls coincide, the condition c=1 and c=1 is just c=1, so the action reduces to one controlled bit flip. Pairwise-distinct controls are required by some instruction encodings but not by this involution argument; control-target distinctness is the load-bearing condition.
Assessment rubric
- Complete two-case inverse argument (1 weight)
- Correct minimal distinctness assumptions (1 weight)
- Identify coincident-control reduction (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/ReversibleClassical.lean
ccxBasisAction24-28; involutive30-50; equivalence52-61
Source SHA-256:01ea24f54500974985702a0f968e28d93b2bd04a1aefaf05da848c9b7fe64711· MIT (repository LICENSE)
Contract: bc1e5664a796f893fd2f033150e6d981c611cbad30267dd96abb0e2bddfa6bff
Item digest: f717b346a68d9dddbefdc009acf698ff6aca04c0531629f56fab06200a6b0999
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.