Reversible Classical
Exercise LA-018
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
On a two-bit string(c,t), consider the update that flips c itself when c=t=1 and otherwise does nothing. Does the familiar self-inverse proof for a two-control target flip remain valid when one control is also the target? Give a concrete collision and explain the lost hypothesis.
Hint: mathematical route
On a two-bit string(c,t), consider the update that flips c itself when c=t=1 and otherwise does nothing. Does the familiar self-inverse proof for a two-control target flip remain valid when one control is also the target? Give a concrete collision and explain the lost hypothesis.
- Evaluate active input(1,1) to(0,1).
- Evaluate inactive input(0,1) to itself, exposing collision.
- Identify failed preservation premise of the inverse proof.
Reference solution
No. The input(1,1) is sent to(0,1), while(0,1) already fails the activation predicate and is left at(0,1). Two distinct inputs therefore collide, so this map is not injective and cannot be reversible or unitary on basis states. Applying it twice to(1,1) does not return the original state: after the first flip the control predicate became false. The usual involution proof uses that flipping the target preserves all control bits, which fails exactly when a control coincides with the target. This is a mathematical counterexample, not a compiler rejection.
Assessment rubric
- Explicit collision of two inputs (1 weight)
- Explain activation predicate changes (1 weight)
- Conclude noninjective not just unsupported API (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
basis action24-28; control-target hypotheses and preserved controls30-49
Source SHA-256:01ea24f54500974985702a0f968e28d93b2bd04a1aefaf05da848c9b7fe64711· MIT (repository LICENSE)
Contract: 3fcf3e1d288ee1c23c341e11ce35c3e8e3e85965508a1af714b1ccd68bf21213
Item digest: c6d32bc846decf5ac3703d8ef0c1d92984d3bd2cacfb16960bdb04a891b21afd
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.