A dirty scratch wire can be fully restored
On this page · Permalink · Source line 104
Consider the four-wire oracle in the Lean examples. First compute \(ab\) into scratch \(s\), copy \(s\) into the target, and uncompute \(s\):
The displayed final expression specializes to the required oracle when the boundary scratch is zero. On the positive input \(a=b=1\), the scratch is dirty between the first and last gates.
The two panels check both initial targets. The final target is toggled, the logical inputs are unchanged, and scratch returns to zero. A proof that used an intermediate clean-workspace assumption would fail to cover this explicit legal fixture.
This circuit uses two Toffolis. It is a useful restoration witness, not the optimal two-input AND oracle: the direct gate \(T(a,b;y)\) computes that oracle with one Toffoli and no scratch. The guide distinguishes an exact example from an optimization claim.
Exact new trace assertion imported from the source gate semantics; the same fixture is formalized by Examples.andOracle_restores.